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

The existing LedgerGammaA.card_H2_gammaA_eq_two (the Γ_A half-torsor proof) proves #H²(Γ_A, 𝔽₂) = 2 but takes a NoDescent radical-cover datum as input (the nonzero variation class is built from a nonzero radical edge). The R-stage assembly of the Prop. 8.9 assembly needs the bare cardinality with no cover data in scope (the "zero-edge" regime), so this file discharges the NoDescent hypothesis once and for all against a concrete witness:

the central extension 𝔽₂ → D₈ → 𝔽₂² with T = M = ⟨s̄⟩ and q ≡ 0.

T lies in the (whole) radical of the zero form, and the cover has no descent: the two lifts sr 0, sr 2 = (sr 0)·z of the generator of T are swapped by conjugation by r 1, so neither 𝔽₂-line complementing ⟨z⟩ in p⁻¹(T) is normal. Feeding this into card_H2_gammaA_eq_two (via any surjection Γ_A ↠ 𝔽₂²/⟨s̄⟩, built here by descending an order-2 marking) yields the unconditional

card_H2_gammaA_unit : Nat.card (H2 GA (ZMod 2)) = 2.

Wired into the R-stage: stageR136_gammaA (the hypothesis-free (136) identity for the candidate source) drops the hcard_A argument of RStageGammaA.stageR136_gammaA_of_hcard.

All finite-group facts are decided; every declaration is std-3 (no B-axioms — the candidate duality route is axiom-free, and the witness is elementary group theory).

The concrete witness 𝔽₂ → D₈ → 𝔽₂²

@[reducible, inline]

abbrev GQ2.CardH2GammaA.Base : Type

The base group 𝔽₂² = Klein four = DihedralGroup 2.

Equations

• GQ2.CardH2GammaA.Base = DihedralGroup 2

@[reducible, inline]

abbrev GQ2.CardH2GammaA.Cov : Type

The cover D₈ = DihedralGroup 4.

Equations

• GQ2.CardH2GammaA.Cov = DihedralGroup 4

@[implicit_reducible]

def GQ2.CardH2GammaA.instTopologicalSpaceBase : TopologicalSpace Base

Equations

• GQ2.CardH2GammaA.instTopologicalSpaceBase = ⊥

theorem GQ2.CardH2GammaA.instDiscreteTopologyBase : DiscreteTopology Base

@[implicit_reducible]

def GQ2.CardH2GammaA.instTopologicalSpaceCov : TopologicalSpace Cov

Equations

• GQ2.CardH2GammaA.instTopologicalSpaceCov = ⊥

theorem GQ2.CardH2GammaA.instDiscreteTopologyCov : DiscreteTopology Cov

def GQ2.CardH2GammaA.φ₀ : Base →* Multiplicative (ZMod 2)

The "index parity" character 𝔽₂² → 𝔽₂, whose kernel is T = M = ⟨s̄⟩.

Equations

• One or more equations did not get rendered due to their size.

def GQ2.CardH2GammaA.Mlayer : Subgroup Base

M = T = ⟨s̄⟩ = ker φ₀ = {1, sr 0} — the radical layer.

Equations

• GQ2.CardH2GammaA.Mlayer = GQ2.CardH2GammaA.φ₀.ker

@[implicit_reducible]

instance GQ2.CardH2GammaA.instDecidablePredBaseMemSubgroupMlayer : DecidablePred fun (x : Base) => x ∈ Mlayer

Equations

• GQ2.CardH2GammaA.instDecidablePredBaseMemSubgroupMlayer x✝ = decidable_of_iff (GQ2.CardH2GammaA.φ₀ x✝ = 1) ⋯

instance GQ2.CardH2GammaA.instNormalBaseMlayer : Mlayer.Normal

def GQ2.CardH2GammaA.cover_p : Cov →* Base

The cover projection D₈ → 𝔽₂², reducing the rotation index ZMod 4 → ZMod 2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GQ2.CardH2GammaA.cover : SectionEight.CentralCover Base

The central double cover D₈ ↠ 𝔽₂² with kernel ⟨z⟩, z = r 2.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.CardH2GammaA.cover_sq (x : Cov) (hx : cover_p x ∈ Mlayer) : x * x = 1

Squares of cover elements over M land in ⟨z⟩ — here trivially = 1, since q ≡ 0 (sr i are involutions and r 0, r 2 square to 1).

noncomputable def GQ2.CardH2GammaA.datum : SectionEight.RadicalCoverData Base

The radical-cover datum of the witness: M = T = ⟨s̄⟩, q ≡ 0.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.CardH2GammaA.datum_noDescent : datum.NoDescent

The witness has no descent: p⁻¹(T) = {r0, r2, sr0, sr2} is elementary abelian, but the two 𝔽₂-lines ⟨sr 0⟩, ⟨sr 2⟩ complementing ⟨z⟩ = ⟨r 2⟩ are swapped by conjugation by r 1 (r 1 · sr 0 · r 1⁻¹ = sr 2), so neither is normal — and sr 0 · sr 2 = r 2 = z.

A surjection Γ_A ↠ 𝔽₂²/⟨s̄⟩ and the unconditional cardinality

@[implicit_reducible]

instance GQ2.CardH2GammaA.instDecidableEqQuotientBaseSubgroupMlayer : DecidableEq (Base ⧸ Mlayer)

Equations

• GQ2.CardH2GammaA.instDecidableEqQuotientBaseSubgroupMlayer = Quotient.decidableEq

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

def GQ2.CardH2GammaA.qmark : Marking (Base ⧸ Mlayer)

The order-2 marking of 𝔽₂²/⟨s̄⟩ sending σ ↦ [r̄] (the nonzero class) and the rest to 1 — trivial wild generators, so admissibility is elementary.

Equations

• GQ2.CardH2GammaA.qmark = { σ := ↑(DihedralGroup.r 1), τ := 1, x₀ := 1, x₁ := 1 }

theorem GQ2.CardH2GammaA.quotient_cases (b : Base) : ↑b = 1 ∨ ↑b = ↑(DihedralGroup.r 1)

Every class in 𝔽₂²/⟨s̄⟩ is 1 or [r̄] (the quotient has order 2).

noncomputable def GQ2.CardH2GammaA.rho : WordCohBridge.GA →ₜ* Base ⧸ Mlayer

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

Equations

• GQ2.CardH2GammaA.rho = GQ2.CardH2GammaA.qmark.descend GQ2.CardH2GammaA.qmark_admissible✝

theorem GQ2.CardH2GammaA.rho_surjective : Function.Surjective ⇑rho

theorem GQ2.CardH2GammaA.card_H2_gammaA_unit [DistribMulAction WordCohBridge.GA (ZMod 2)] [ContinuousSMul WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x • m = m) : Nat.card (ContCoh.H2 WordCohBridge.GA (ZMod 2)) = 2

#H²(Γ_A, 𝔽₂) = 2, unconditionally (the Prop. 8.9 assembly, over the raw quotient GA). The NoDescent hypothesis of LedgerGammaA.card_H2_gammaA_eq_two is discharged by the concrete witness datum/datum_noDescent; ρ = rho is any surjection onto 𝔽₂²/⟨s̄⟩.

The GammaA-facing forms and the hypothesis-free (136) for the candidate source

theorem GQ2.CardH2GammaA.card_H2_gammaA : Nat.card (ContCoh.H2 (↑GammaA.toProfinite.toTop) (ZMod 2)) = 2

#H²(Γ_A, 𝔽₂) = 2 over the packaged GammaA, with its canonical trivial action (RStageGammaA.instDistribMulActionGammaA). This is the exact hcard_A residue that RStageGammaA.stageR136_gammaA_of_hcard threads — supplied here unconditionally (the Prop. 8.9 assembly), bridging the raw-quotient GA result across the GA ≡ GammaA defeq.

theorem GQ2.CardH2GammaA.stageR136_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (hE2 : ∀ (e : E), e ^ 2 = 1) (hRK : ∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) (hR2 : ∀ r ∈ Blk.frattiniK, r * r = 1) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) : ↑(Nat.card (blockFrameImpl T Blk hE2).DR) * ↑(exactImageCount b F T) = ↑(blockFrameImpl T Blk hE2).zR * ∑ᶠ (l : (blockFrameImpl T Blk hE2).DR), (2 * ↑((blockFrameImpl T Blk hE2).mB b F l) - ↑(exactImageCount b F (blockFrameImpl T Blk hE2).TB))

(136) for the block frame at the candidate source, hypothesis-free (the Prop. 8.9 assembly): drops the hcard_A argument of RStageGammaA.stageR136_gammaA_of_hcard by supplying card_H2_gammaA. The remaining hRK/hR2 are the lemma_7_2 structural facts of the block; hfg is discharged internally (gammaA_topologicallyFinitelyGenerated). This is the stageR136 field of the candidate RecursionInputs bundle (the Prop. 8.9 assembly), verbatim.