The Γ_R-side M-stage multiplicity count (obligation ii.3)

The Γ_R twin of GQ2/MStageCountGammaA.lean: the M-stage lane of thm_4_2 applies mStage_partition with multiplicity mult = |M_B|², and this file supplies the Γ_R count #LiftsOver_{Γ_R}(ρ) = |M_B|² — the SourceData.liftsOver_card field at Γ := Γ_R (recon row ii.3), whose Γ_A occupant is RecursionFrame.liftsOver_card_gammaA.

The port is line-for-line against the Γ_A original, with the Roe wild word substituted throughout (GA → GR, markC → markC_R, Marking.push → Marking.pushR, WildRel → WildRelR, Marking.descend → Marking.descendR, Admissible → AdmissibleR, prop_5_15 → prop_5_15_R, z1Equiv → z1EquivR, d1Fun/d1/H2w → d1FunR/d1R/H2wR). The two places where the Roe candidate duality actually enters are exactly the two prop_5_15_R calls, both immediately after markC_admissible_R θ hθs:

• the Z¹ count (liftsOver_card_gammaR_of_nonempty, clause .2.1) — there is no local Euler characteristic for Γ_R either, so z1EquivR (GQ2/WordCohBridgeR.lean, R31b) identifies Z¹_cont(Γ_R, M_B) with the Roe word cocycles Z¹_{word,R}(markC_R ρ) and prop_5_15_R clause 2 counts those as |M_B|² · #fixedPts_C(M_B^∨);
• nonemptiness (liftsOver_nonempty_gammaR, clause .1) — #H²_{word,R} = #fixedPts = 1 puts the Roe relator pair (v₁, v₂) in range (d¹_R (markC_R θ)), so the set-lift marking's relator values are correctable (RStageGammaA.corrected_tameValue for the shared tame row, RStageGammaR.corrected_wildValueR for the Roe wild row, both transported by RStageGammaR.d1FunR_base_change) and the corrected marking descends through Marking.descendR (descend_piBC_R, the π_{BC} port of the Roe L5 descent).

#fixedPts = 1 is the source-independent lemma_7_1_dual bridge: it lives in the shared M_B module pack (MB_mul_comm/MB_conj_eq/MB_add_self/mbCommGroup/mbSec/mbConjActC/ card_fixedPts_MB_dual), which is private in both GQ2/MStageCount.lean and GQ2/MStageCountGammaA.lean and is therefore carried here as a third private copy — source-free in all three, and unchanged from the Γ_A text.

Axioms (target at close): ⊆ std-3 + B6 + B7 (as liftsOver_card_gammaA; B6/B7 enter through prop_5_15_R's duality assembly, exactly as they do through prop_5_15).

Module-system note. Plain import (non-module), like its Γ_A original: it imports the non-module files GQ2.MStageCountGammaA / GQ2.Roe.CorrectionR / GQ2.Roe.Prop23 / GQ2.SourceData. Importing the module file GQ2.Roe.DualityAssembly from here is fine — the restriction is one-directional.

The shared M_B module pack (third private copy)

Verbatim from GQ2/MStageCountGammaA.lean:164-361 (itself a copy of GQ2/MStageCount.lean's): 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). Every declaration here is source-free — no marking word appears — so the Roe port changes nothing; the copy exists only because the originals are private to their modules. The twins install the pack by letI/have and diverge at their coboundary/torsor tails.

theorem GQ2.SectionEight.RecursionFrame.liftsOver_nonempty_gammaR {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 : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Nonempty (RF.LiftsOver b F ρ)

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

The Γ_R port of RecursionFrame.liftsOver_nonempty_gammaA: a set-lift marking of ρ has both relator values in M_B (push_tameRelR/push_wildRelR, no surjectivity needed), and since (M_B^∨)^C = 0 (lemma_7_1_dual, via card_fixedPts_MB_dual) the Roe candidate duality prop_5_15_R clause 1 gives #H²_{word,R} = 1, forcing the relator pair to be a d¹_R-image; the corrected marking (shared tame row corrected_tameValue, Roe wild row corrected_wildValueR, transported by d1FunR_base_change) then descends by descend_piBC_R.

theorem GQ2.SectionEight.RecursionFrame.liftsOver_card_gammaR_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 : ↑GammaR.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

hmultR for Γ_R, 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 Roe candidate-duality route (z1EquivR + prop_5_15_R clause 2), and hfix = 1 is the lemma_7_1_dual bridge, both mirroring the Γ_A twin.

theorem GQ2.SectionEight.RecursionFrame.liftsOver_card_gammaR {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 : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2

hmultR for Γ_R (obligation ii.3, the SourceData.liftsOver_card field at Γ := Γ_R): #LiftsOver(ρ) = |M_B|² over every lower boundary lift.

SourceData field-type smoke test (R31 spelling discipline)

The example below is stated in the verbatim field type of GQ2.SourceData.liftsOver_card (GQ2/SourceData.lean:137-143) specialised at Γ := GammaR, and is filled by exactly the fun RF b F ρ => … partial application that BoundaryMaps.sourceA uses for the Γ_A occupant (GQ2/SourceData.lean:322). Any future drift between liftsOver_card_gammaR and the structure field is caught here rather than in R32's sourceR.

Paper-tag ledger (paper §8/§9 + Roe note paper/roe-presentation-verification.tex;

hand-maintained)

• Proposition 5.15 = ⟦prop:duality⟧ — the Roe candidate deformation duality (prop_5_15_R), entering at the two marked spots (#Z¹_R count, #H²_R = 1 nonemptiness).
• Lemma 7.1 (dual form) — card_fixedPts_MB_dual, the source-free (M_B^∨)^{Y_C} = 0 input.