The Γ_A-side M-stage multiplicity count (hmultA)

The M-stage lane of thm_4_2 (GQ2/SectionNine.lean, the R = ⊥ branch) applies mStage_partition at both sources with multiplicity mult = |M_B|²; the G_ℚ₂ count is RecursionFrame.liftsOver_card_local (GQ2/MStageCount.lean). This file supplies the Γ_A count #LiftsOver_{Γ_A}(ρ) = |M_B|² (hmultA).

The proof mirrors liftsOver_card_local (the #H² = 1 torsor bridge at the descended module M_B), with the two Γ_A-specific substitutions of the Prop. 8.9 assembly RStageGammaA playbook:

• the Z¹ count — there is no local Euler characteristic for Γ_A; the candidate duality supplies it instead. z1Equiv (WordCohBridge, the Γ_A half-torsor proof) identifies Z¹_cont(Γ_A, M_B) with the Fox–Heisenberg word cocycles Z¹_word(markC ρ), and prop_5_15 clause 2 (IsSelfDual) counts those as |M_B|² · #fixedPts_C(M_B^∨). This is exactly the hZcount_gammaA route at module M_B instead of R. #fixedPts = 1 is the source-independent lemma_7_1_dual bridge, extracted once as card_fixedPts_MB_dual (the same argument as liftsOver_card_local's hfix) inside the shared M_B module pack consumed by both twins.
• nonemptiness — Γ_A has no degree-2 word↔continuous bridge, so the #H² = 1 ⟹ coboundary route of the local proof is unavailable. Instead liftsOver_nonempty_gammaA ports the hsep_hom_gammaA + L5-descent argument (RStageGammaA) from (π_B, R) to (π_BC, M_B): a set-lift marking's relator values land in M_B, the trace-span duality forces their correction (since (M_B^∨)^C = 0), and the corrected marking descends.

Axioms (target at close): ⊆ std-3 + B6 + B7 (as liftsOver_card_local / hZcount_gammaA).

The shared M_B module pack

Both twins below run the same M_B-module setup: M_B ⊴ Y_B is elementary abelian (2-torsion by MB_elem), carries the Y_C-conjugation action through a set-section of π_{BC}, and has no nonzero Y_C-invariant 𝔽₂-functional (lemma_7_1_dual). The pack is extracted here once; the twins install it by letI/have and diverge only at their coboundary/torsor tails.

theorem GQ2.SectionEight.RecursionFrame.liftsOver_nonempty_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Nonempty (RF.LiftsOver b F ρ)

Nonemptiness of the Γ_A B-lift fibre (the §9 induction, the M-stage residue): every lower boundary lift ρ : Γ_A ↠ C lifts to a continuous homomorphism Γ_A → B through π_{BC}.

Ported from RStageGammaA.hsep_hom_gammaA (which lifts through π_B : Y ↠ B) to π_{BC} : B ↠ C (kernel M_B, 2-torsion by MB_elem): a set-lift marking of ρ has relator values in M_B, and since (M_B^∨)^C = 0 (lemma_7_1_dual, the hfix group theory) the trace-span duality forces those values to be correctable, whence the corrected marking descends (L5).

theorem GQ2.SectionEight.RecursionFrame.liftsOver_card_gammaA_of_nonempty {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) (hne : Nonempty (RF.LiftsOver b F ρ)) : Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2

hmultA for Γ_A, assuming the fibre is nonempty: #LiftsOver(ρ) = |M_B|². The Z¹-torsor bridge (liftsOver_card_local's Step 2) is source-generic once a base lift exists; the Z¹ count is the candidate-duality route (z1Equiv + prop_5_15 clause 2), and hfix = 1 is the lemma_7_1_dual bridge, both mirroring the local proof.

theorem GQ2.SectionEight.RecursionFrame.liftsOver_card_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : ↑GammaA.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2

hmultA for Γ_A: #LiftsOver(ρ) = |M_B|² over every lower boundary lift.