The nonzero variation class over Γ_R, #H²(Γ_R, 𝔽₂) = 2, and Lemma 8.6

The Γ_R twin of GQ2/HalfTorsorGammaA.lean, and the delivery point of two SourceData leaves for the Roe candidate:

• exists_nonzero_varCoc_gammaR — assembling the Γ_R ledger identity with the prop_5_15_R self-duality: from NoDescent, there is a crossed T-cocycle u whose variation class [varCoc u] ∈ H²(Γ_R, 𝔽₂) is nonzero (the hvar input to CentralObstruction.half_count);
• card_H2_gammaR_eq_two — #H²(Γ_R, 𝔽₂) = 2: WordCoh2R.obsH2_R_injective gives ≤ 2, the nonzero variation class gives surjectivity;
• card_H2_gammaR — the same unconditionally, over the packaged GammaR with its canonical trivial action. The NoDescent hypothesis is discharged against the source-free D₈ witness CardH2GammaA.datum/datum_noDescent, reused verbatim (RadicalCoverData carries no Γ); only the surjection Γ_R ↠ 𝔽₂²/⟨s̄⟩ is rebuilt, by descending CardH2GammaA.qmark through Marking.descendR. This is the SourceData.cardH2 leaf — the hcard_R residue that RStageGammaR.stageR136_gammaR_of_hcard and hsep_hom_gammaR thread;
• half_torsor_gammaR / lemma_8_6_gammaR — the SourceData.lem86 leaf (obligation ii.4): with a nonzero radical edge, exactly half of the unrestricted M-lifts of a lower epimorphism ρ : Γ_R ↠ B/M satisfy the central relation.

The two examples at the end are stated in the verbatim field types of GQ2.SourceData specialised at Γ := GammaR (the RStage/GammaR.lean spelling discipline), so that any drift between these declarations and the structure is caught here rather than in R32's sourceR.

theorem GQ2.SectionEight.LedgerGammaR.exists_nonzero_varCoc_gammaR {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : CentralObstruction.TComplement D) (hedge : D.NoDescent) (ρ : WordCohBridgeR.GR →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) [DistribMulAction WordCohBridgeR.GR (ZMod 2)] [ContinuousSMul WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : ∃ (u : CentralObstruction.TCocycle D ρ), (ContCoh.H2mk WordCohBridgeR.GR (ZMod 2)) ⟨CentralObstruction.varCoc D ρ S u, ⋯⟩ ≠ 0

The nonzero variation class over Γ_R (the Γ_R half-torsor proof). For a lower epimorphism ρ : Γ_R ↠ B/M with nonzero radical edge (NoDescent), there is a crossed T-cocycle u whose variation class is a nonzero element of H²(Γ_R, 𝔽₂).

theorem GQ2.SectionEight.LedgerGammaR.card_H2_gammaR_eq_two {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : CentralObstruction.TComplement D) (hedge : D.NoDescent) (ρ : WordCohBridgeR.GR →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) [DistribMulAction WordCohBridgeR.GR (ZMod 2)] [ContinuousSMul WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : Nat.card (ContCoh.H2 WordCohBridgeR.GR (ZMod 2)) = 2

#H²(Γ_R, 𝔽₂) = 2 (the Γ_R half-torsor proof hcard). The obstruction injection obsH2_R : H² ↪ 𝔽₂ (c2) gives ≤ 2; the nonzero variation class makes it surjective, hence a bijection.

theorem GQ2.SectionEight.LedgerGammaR.half_torsor_gammaR {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (hedge : D.NoDescent) (ρ : ↑GammaR.toProfinite.toTop →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6, Γ_R source (the Γ_R half-torsor proof): with a nonzero radical edge, exactly half of the unrestricted M-lifts of a lower epimorphism ρ : Γ_R ↠ B/M satisfy the central relation. The abstract half-count CentralObstruction.half_count fed by the nonzero variation class (exists_nonzero_varCoc_gammaR) and #H² = 2 (card_H2_gammaR_eq_two); the counted set is finite because Γ_R is topologically finitely generated.

theorem GQ2.SectionEight.LedgerGammaR.lemma_8_6_gammaR {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (hedge : D.NoDescent) (ρ : ↑GammaR.toProfinite.toTop →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6, Γ_R source ⟦lem-radicaledge⟧ — the SourceData.lem86 leaf (obligation ii.4). Γ_R twin of SectionEight.lemma_8_6_gammaA (GQ2/SectionEight/Partition.lean), stated over the packaged GammaR; the content is half_torsor_gammaR.

#H²(Γ_R, 𝔽₂) = 2, unconditionally

The NoDescent hypothesis of card_H2_gammaR_eq_two is discharged exactly as on the Γ_A side (GQ2/CardH2GammaA.lean), against the same concrete witness 𝔽₂ → D₈ → 𝔽₂² with T = M = ⟨s̄⟩ and q ≡ 0. That witness is source-free — RadicalCoverData Bg binds only [Group Bg] [Finite Bg], no Γ — so CardH2GammaA.datum and CardH2GammaA.datum_noDescent are reused verbatim. Only the surjection onto 𝔽₂²/⟨s̄⟩ is Γ-specific and rebuilt here: the same order-2 marking CardH2GammaA.qmark, now shown AdmissibleR (its Roe wild relation is automatic — both wild generators are trivial, Marking.wildRelR_of_trivial_wild) and descended through Marking.descendR.

@[implicit_reducible]

def GQ2.SectionEight.LedgerGammaR.instTopologicalSpaceBase : TopologicalSpace CardH2GammaA.Base

Equations

• GQ2.SectionEight.LedgerGammaR.instTopologicalSpaceBase = ⊥

theorem GQ2.SectionEight.LedgerGammaR.instDiscreteTopologyBase : DiscreteTopology CardH2GammaA.Base

theorem GQ2.SectionEight.LedgerGammaR.instDiscreteTopologyQuotientBaseSubgroupMlayer : DiscreteTopology (CardH2GammaA.Base ⧸ CardH2GammaA.Mlayer)

noncomputable def GQ2.SectionEight.LedgerGammaR.rhoR : WordCohBridgeR.GR →ₜ* CardH2GammaA.Base ⧸ CardH2GammaA.Mlayer

The chosen surjection ρ_R : Γ_R ↠ 𝔽₂²/⟨s̄⟩, by descending qmark through Marking.descendR.

Equations

• GQ2.SectionEight.LedgerGammaR.rhoR = GQ2.CardH2GammaA.qmark.descendR GQ2.SectionEight.LedgerGammaR.qmark_admissibleR✝

theorem GQ2.SectionEight.LedgerGammaR.rhoR_surjective : Function.Surjective ⇑rhoR

theorem GQ2.SectionEight.LedgerGammaR.card_H2_gammaR_unit [DistribMulAction WordCohBridgeR.GR (ZMod 2)] [ContinuousSMul WordCohBridgeR.GR (ZMod 2)] (htriv : ∀ (x : WordCohBridgeR.GR) (m : ZMod 2), x • m = m) : Nat.card (ContCoh.H2 WordCohBridgeR.GR (ZMod 2)) = 2

#H²(Γ_R, 𝔽₂) = 2, unconditionally, over the raw quotient GR.

theorem GQ2.SectionEight.LedgerGammaR.card_H2_gammaR : Nat.card (ContCoh.H2 (↑GammaR.toProfinite.toTop) (ZMod 2)) = 2

#H²(Γ_R, 𝔽₂) = 2 over the packaged GammaR, with its canonical trivial action (RStageGammaR.instDistribMulActionGammaR) — the SourceData.cardH2 leaf, and the exact hcard_R residue threaded by RStageGammaR.hsep_hom_gammaR and RStageGammaR.stageR136_gammaR_of_hcard. Bridges card_H2_gammaR_unit across the GR ≡ GammaR defeq, mirroring CardH2GammaA.card_H2_gammaA.

SourceData field-type smoke tests (R31 spelling discipline)

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• Lemma 8.6 = ⟦lem-radicaledge⟧ — lemma_8_6_gammaR, over Γ_R.
• Definition 1.1 = ⟦def:GammaR⟧ — Marking.descendR/AdmissibleR, in rhoR.