Foundations for the Γ_R phase-140 residues

The Roe-candidate twin of GQ2/Phase140/GammaA/Foundation.lean: the candidate-side counts and the T-stage descent of covering markings.

See GQ2.Phase140.GammaR for the paper-facing overview and architectural notes.

What is reused, never cloned. The per-character 𝔽₂-cover layer of Γ_A's Foundation (Phase140GammaA.charKer/charCover/charCoverMap/charCover_p_comp/charCoverMap_coe_eq_zpow/ exists_lift_charCover, Foundation.lean:181–441) is abstract in Γ — it takes the source as a section variable with [DistribMulAction Γ (ZMod 2)] plus htriv — so Γ_R imports and applies it at GR rather than re-deriving it. Likewise the L5 kernel is the shared RStageGammaR.lift_of_relatorFree_markingR (GQ2/Roe/CoverLiftR.lean), which is more general than the Γ_A original precisely so that this file's non-surjective T-stage can feed it a corestricted Pro2Core certificate instead of cloning the descent.

theorem GQ2.Phase140GammaR.hZcard_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 : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : RF.YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : RF.YC) (v : En.Vmod), g • v ≠ v) (ρ : BoundaryLifts b F RF.TC) : Nat.card (SectionEight.AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card En.Vmod * Nat.card En.Vmod

hZcard for Γ_R — #Z¹_{Γ_R,ρ'}(V) = #V². Mirror of Phase140GammaA.hZcard_gammaA with the Roe word complex: the VCocycle ≃ Z¹_cont(Γ_R, V) bridge (structurally Γ-generic), then z1EquivR + prop_5_15_R clause 2 (#Z1wR = #V²·#fixedPts) instead of card_Z1_eq, and the #fixedPts = 1 factor from the simple nontrivial Y_C-action (card_fixedPts_elemDual_eq_one_of_nontrivial).

hnt (the nontrivial Y_C-action) is REQUIRED — in the #V = 2 ∧ Y_C = 1 corner #(V^∨)^{Y_C} = 2 ≠ 1 and the identity is false; it is discharged at the capstone from the block's chief-factor structure (same amendment as on the Γ_A and local sides).

theorem GQ2.Phase140GammaR.tcocycle_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 : SectionEight.RecursionFrame T Blk} (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) : Nat.card (SectionEight.CentralObstruction.TCocycle (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card (Additive ↥(En.radData l h).T) ^ 2 * Nat.card ↑(FoxH.fixedPts (RF.YB ⧸ (En.radData l h).M) (FoxH.ElemDual (Additive ↥(En.radData l h).T)))

hμ for Γ_R — the T-cocycle count #Z¹_{Γ_R,ρ'}(T) = #T²·#(T^∨)^{Y_B/M} in the muZero closed form (Phase140GammaA.tcocycle_card_gammaA's twin). Same module setup (the global RadicalEdgeGammaA.cActT conjugation action, which is Γ-free over RadicalCoverData) and the same TCocycle ≃ Z¹_cont(GR, Additive T) bridge; the count is z1EquivR + prop_5_15_R clause 2. The #fixedPts factor is NOT reduced: it is part of the shared μ₀ value (the twin dualities produce the same closed form, which is the source-independence prop_8_9 needs).

L5 descent at the T-stage: a relator-free covering marking of B descends from Γ_R

The T-stage consumer of the shared Γ_R L5 kernel (GQ2/Roe/CoverLiftR.lean), with the one twist the Γ_A side also had to absorb: the covered map g_Q : Γ_R → B/T is not surjective (its image is the graph-like subgroup of a V-cocycle), so Marking.pushR_admissible does not apply to it directly and no Pro2Core certificate is available downstairs.

The Γ_A file solved this by cloning the whole descent (Phase140GammaA.mlift_of_relatorFree_marking, 221 ln). Here the kernel was deliberately generalised — lift_of_relatorFree_markingR takes an abstract π and the Pro2Core input directly rather than through surjectivity of g_B — so the fix is just a corestriction: the four B/T-generator images generate J̄, the F₄-hom classified by the J̄-marking kills N_R, so it descends to a surjective ḡ : Γ_R ↠ J̄, whose pushed marking is R-admissible and supplies hcoreB. Nothing of the kernel is cloned.

theorem GQ2.Phase140GammaR.mlift_of_relatorFree_markingR {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] {D : SectionEight.RadicalCoverData Bg} (gQ : WordCohBridgeR.GR →ₜ* Bg ⧸ D.T) (tHat : Marking Bg) (hproj : Marking.map (QuotientGroup.mk' D.T) tHat = Marking.pushR gQ) (htame : tHat.TameRel) (hwild : tHat.WildRelR) : ∃ (f : ↑GammaR.toProfinite.toTop →ₜ* Bg), ∀ (γ : ↑GammaR.toProfinite.toTop), (QuotientGroup.mk' D.T) (f γ) = gQ γ

The T-stage descent (hsep_gammaR L5): a marking of B that covers g_Q's marking through π_T and kills both Γ_R relators descends to a continuous f : Γ_R → B with π_T ∘ f = g_Q. Γ_R twin of Phase140GammaA.mlift_of_relatorFree_marking, but assembled from the shared kernel RStageGammaR.lift_of_relatorFree_markingR at the corestricted projection qJ' : J → J̄ instead of re-deriving the descent.

SourceData field-type smoke tests (R31 spelling discipline)

Each residue is restated in the verbatim GQ2.SourceData field type at Γ := GammaR and discharged by the plain lambda BoundaryMaps.sourceA uses for its _gammaA twin (GQ2/SourceData.lean:325–330), so sourceR (R32) is a copy-paste.