The (136) R-stage for Γ = Γ_R

The instance prerequisite of the Γ_R source-data supply (ticket R31, discovered by the R30 SourceData recon): the (136)/(140)/Gauss-Z layers are all stated at an ambient DistribMulAction Γ (ZMod 2), and GQ2.SourceData carries that action as the three fields smulZmod2 / contSMulZmod2 / htriv. On the Γ_A side these are the global instances registered in GQ2/RStage/GammaA.lean:53-69; this file registers their Γ_R mirrors so that R32's sourceR can fill the three fields with inferInstance, inferInstance, RStageGammaR.htriv_gammaR — exactly as BoundaryMaps.sourceA does (GQ2/SourceData.lean:316-318).

On top of that instance layer this file carries the whole Γ_R (136) chain — the twin of GQ2/RStage/GammaA.lean, name-for-name (ticket R31e, obligation ii.5):

• hZcount_gammaR — #RCocycle = z_R, via the Roe word bridge z1EquivR (GQ2/WordCohBridgeR.lean) + prop_5_15_R clause 2 + the frame-generic blockRChar_card;
• wTrace_R / sep_word_R — the (2,0)-trace-span package on H²_{R,word}, driven by prop_5_8_right_R and IsSelfDual_R clause 1 (no H²(Γ_R, R));
• hsep_hom_gammaR — the (R^∨)^C-separation, on the shared L4/L5 cover-lift kernel GQ2/Roe/CoverLiftR.lean;
• stageR136_gammaR_of_hcard — the (136) identity, threading hcard_R hypothesis-side exactly as stageR136_gammaA_of_hcard threads hcard_A (so ii.5 is decoupled from the card_H2 obligation, which is owned elsewhere).

Since Aut(𝔽₂) = 1, every action of any group on ZMod 2 is the trivial one, so the content here is nil: the instance is defined by smul _ m := m and htriv_gammaR is rfl. What matters is that the action is registered globally at the ProfiniteGrp-bundled carrier GammaR, the carrier spelling the SourceData fields use (↥Γ at Γ := GammaR) — a DistribMulAction registered at the raw quotient F₄ ⧸ N_R would not cross-resolve, exactly the GammaA/GA instance-diamond documented in the GQ2/RStage/GammaA.lean standing plumbing note.

Module-system note. Plain import (non-module), like its siblings GQ2/Roe/Supply.lean and GQ2/Roe/Prop23.lean: it imports the non-module GQ2.RStage.GammaA, and module-style files cannot import plain ones. Importing the module file GQ2.Roe.GammaR from here is fine — the restriction is one-directional.

Axioms: none introduced (htriv_gammaR is rfl; the instances are definitional).

theorem GQ2.RStageGammaR.gammaR_eq_quotient : ↑GammaR.toProfinite.toTop = (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

Γ_R's underlying type is the raw quotient F₄ ⧸ N_R against which the Roe marking machinery (markC_R, Z1wR, prop_5_15_R) is stated — the Γ_R mirror of RStageGammaA.gammaA_eq_GA, and the bridge every Γ_R word-machinery call transports across.

The canonical trivial Γ_R-action on 𝔽₂

@[implicit_reducible]

instance GQ2.RStageGammaR.instDistribMulActionGammaR : DistribMulAction (↑GammaR.toProfinite.toTop) (ZMod 2)

The trivial Γ_R-action on 𝔽₂ (Aut(𝔽₂) = 1, so every action is this one). Mirror of RStageGammaA.instDistribMulActionGammaA.

Equations

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

instance GQ2.RStageGammaR.instContinuousSMulCarrierToTopTotallyDisconnectedSpaceToProfiniteGammaRZModOfNatNat : ContinuousSMul (↑GammaR.toProfinite.toTop) (ZMod 2)

theorem GQ2.RStageGammaR.htriv_gammaR (γ : ↑GammaR.toProfinite.toTop) (m : ZMod 2) : γ • m = m

The Γ_R-action on 𝔽₂ is trivial — the htriv field of Γ_R's SourceData (GQ2/SourceData.lean:123), mirror of RStageGammaA.htriv_gammaA. Definitional, from the registered trivial action.

Sanity lemmas

theorem GQ2.RStageGammaR.smul_eq_of_gammaR (γ δ : ↑GammaR.toProfinite.toTop) (m : ZMod 2) : γ • m = δ • m

Sanity 1. The registered action is the trivial one on the nose: scalar multiplication is the second projection, so it is constant in the group argument.

theorem GQ2.RStageGammaR.htriv_gammaR_and_gammaA (γ : ↑GammaR.toProfinite.toTop) (α : ↑GammaA.toProfinite.toTop) (m : ZMod 2) : γ • m = m ∧ α • m = m

Sanity 2. The Γ_R action agrees with the Γ_A one under any map of underlying elements — both are the unique (trivial) action, so the two sources present 𝔽₂ identically to the (136)/(140) layers.

theorem GQ2.RStageGammaR.gammaR_smul_add (γ : ↑GammaR.toProfinite.toTop) (m n : ZMod 2) : γ • (m + n) = γ • m + γ • n

Sanity 3. The action is by additive-group automorphisms and fixes everything, so the fixed-point set is all of 𝔽₂ — the degenerate input the (140) layer's fixedPts factors reduce through.

SourceData field-type smoke tests (R31 spelling discipline)

Each example below is stated in the verbatim field type of GQ2.SourceData (GQ2/SourceData.lean:119-123) specialised at Γ := GammaR, so that any future drift between these declarations and the structure is caught here rather than in R32's sourceR. (The fields are mutually dependent — contSMulZmod2/htriv are stated under letI := smulZmod2 — so the letI is discharged here by the registered global instances, which is precisely the inferInstance route BoundaryMaps.sourceA takes.)

Shared C = Y/K-module helpers (used by hZcount and hsep_hom)

Third copies of the RStageLocal pack (GQ2/RStage/Local.lean:148/162/195, already cloned once in GQ2/RStage/GammaA.lean:75/89/122): all three are private at both sites, hence inaccessible across modules. The statements and proofs are entirely source-free — the marking word never enters — so these are verbatim transcriptions, carrying the R suffix only to keep the Γ_R namespace readable.

hZcount: the z_R torsor count at the Roe source

The Γ_R mirror of hZcount_gammaA: RCocycle ≃ Z¹(Γ_R, R_{f₀}) (identical conjugation-action setup, reusing RStageLocal's ConjAction section), then the count via z1EquivR + prop_5_15_R clause 2 (#Z1wR = #R²·#fixedPts C (R^∨)), and the same frame-generic fixedPts ≃ RCharSub bridge + blockRChar_card.

theorem GQ2.RStageGammaR.hZcount_gammaR {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 : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (f₀ : BoundaryLifts b F T) : Nat.card (SectionEight.RCocycle (blockFrameImpl T Blk hE2) ↑↑f₀) = (blockFrameImpl T Blk hE2).zR

L3 — the trace-span package: (R^∨)^C perfectly pairs H2wR

Statement-for-statement port of RStageGammaA's TraceSpan section onto the Roe word complex H2wR t = (A × A) ⧸ (d1R t).range. Only three inputs change: prop_5_8_right_R (for well-definedness), IsSelfDual_R clause 1 and H2w_two_torsion_R (for the count). H0w and H0w_eq_fixedPts are reused verbatim — the Roe H0wR is the very same object (H0wR_eq_H0w is rfl, GQ2/Roe/FoxBasic.lean:159), since d⁰ never sees the relator.

noncomputable def GQ2.RStageGammaR.wTrace_R {C : Type} [Group C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (lam : FoxH.ElemDual A) (hlam : (FoxH.d0 t) lam = 0) : FoxH.H2wR t →+ ZMod 2

The trace functional for the Roe word Φ_λ : H2wR(A) →+ 𝔽₂, [v] ↦ λ(v.1 + v.2) — Γ_R twin of RStageGammaA.wTrace. Well-defined on the quotient H2wR = (A×A) ⧸ im d¹_R because for an invariant λ (d⁰λ = 0), prop_5_8_right_R gives λ((d¹_R x).1 + (d¹_R x).2) = mixedB_R t x (d⁰λ) = mixedB_R t x 0 = 0. This is the (2,0)-pairing that IsSelfDual_R omits — supplied by Prop. 5.8 directly.

Equations

• GQ2.RStageGammaR.wTrace_R t ht hw lam hlam = QuotientAddGroup.lift (GQ2.FoxH.d1R t).range (AddMonoidHom.comp lam (AddMonoidHom.fst A A + AddMonoidHom.snd A A)) ⋯

theorem GQ2.RStageGammaR.wTrace_R_injective {C : Type} [Group C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (lam lam' : FoxH.ElemDual A) (hlam : (FoxH.d0 t) lam = 0) (hlam' : (FoxH.d0 t) lam' = 0) (h : wTrace_R t ht hw lam hlam = wTrace_R t ht hw lam' hlam') : lam = lam'

λ ↦ Φ_λ is injective — Φ_λ at [⟨a,0⟩] is λ a, so the functional determines λ.

theorem GQ2.RStageGammaR.wTrace_R_surjective {C : Type} [Group C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hsd : FoxH.IsSelfDual_R t A) (hA₂ : ∀ (a : A), a + a = 0) (Ψ : FoxH.H2wR t →+ ZMod 2) : ∃ (lam : FoxH.ElemDual A) (hlam : (FoxH.d0 t) lam = 0), wTrace_R t ht hw lam hlam = Ψ

λ ↦ Φ_λ is surjective onto H2wR →+ 𝔽₂ — the counting half of the perfect (2,0)-pairing. The invariant characters, #H2wR, and #(H2wR →+ 𝔽₂) are all equinumerous: #{λ : d⁰λ = 0} = #fixedPts C (A^∨) = #H2wR = #(H2wR →+ 𝔽₂) — by H0w_eq_fixedPts (needs Generates; H0wR is H0w), IsSelfDual_R clause 1, and card_addHom_zmod2 at H2w_two_torsion_R. A finite injection (wTrace_R_injective) between equinumerous finite sets is bijective, hence surjective.

theorem GQ2.RStageGammaR.sep_word_R {C : Type} [Group C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (hgen : t.Generates) (hsd : FoxH.IsSelfDual_R t A) (hA₂ : ∀ (a : A), a + a = 0) (v : A × A) (hv : ∀ (lam : FoxH.ElemDual A), (FoxH.d0 t) lam = 0 → lam (v.1 + v.2) = 0) : v ∈ (FoxH.d1R t).range

sep_word_R — the separation for the Roe word. If v.1 + v.2 is killed by every invariant character λ (d⁰λ = 0), then v ∈ im d¹_R. Proof: if [v] ≠ 0 in H2wR, then exists_addHom_ne_zero (finite 𝔽₂-space) produces a functional Ψ with Ψ [v] ≠ 0; by wTrace_R_surjective, Ψ = Φ_λ for some invariant λ, and Φ_λ [v] = λ(v.1 + v.2) = 0 by hypothesis — contradiction. Γ_R twin of RStageGammaA.sep_word.

hsep_hom: the (R^∨)^C separation at the Roe source (L1–L5)

theorem GQ2.RStageGammaR.hsep_hom_gammaR {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) (hcard_R : Nat.card (ContCoh.H2 (↑GammaR.toProfinite.toTop) (ZMod 2)) = 2) (b : ↑GammaR.toProfinite.toTop →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (g : BoundaryLifts b F (blockFrameImpl T Blk hE2).TB) (hg : SectionEight.obs (blockFrameImpl T Blk hE2) (blockRObstructionData T Blk hE2) htriv_gammaR hcard_R ↑↑g = 0) : ∃ (φ : ↑GammaR.toProfinite.toTop →ₜ* Y), ∀ (γ : ↑GammaR.toProfinite.toTop), (blockFrameImpl T Blk hE2).piB (φ γ) = ↑↑g γ

The (R^∨)^C-separation at Γ_R: if the obstruction functional of a boundary lift g vanishes, g lifts to a continuous homomorphism into Y. Route, step for step the Γ_A one: obs g = 0 gives, per invariant character, a concrete lift through the scalar cover (obs_zero_iff_lifts); the relator-value corrections of a set-lift are d1FunR rows (corrected_tameValue — the tame row is shared — and corrected_wildValueR); the trace-span package (sep_word_R, on prop_5_8_right_R + prop_5_15_R) forces full word-solvability; the corrected marking descends by lift_of_relatorFree_markingR. hcard_R is threaded (proof-irrelevant Prop), so this is decoupled from the card_H2 leaf.

stageR136: the (136) identity, assembled

theorem GQ2.RStageGammaR.stageR136_gammaR_of_hcard {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) (hcard_R : Nat.card (ContCoh.H2 (↑GammaR.toProfinite.toTop) (ZMod 2)) = 2) (b : ↑GammaR.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 Roe source, threading hcard_R: htriv/hZcount/ hsep_hom are the residues discharged here; hcard_R and the lemma_7_2 structural facts hRK/hR2 thread hypothesis-side. hfg is gammaR_topologicallyFinitelyGenerated (GQ2/Roe/Supply.lean). The conclusion is the stageR136 field of GQ2.SourceData verbatim, at Γ := GammaR — mirror of RStageGammaA.stageR136_gammaA_of_hcard, so that the Γ_R twin of CardH2GammaA.stageR136_gammaA is a one-line splice once the card_H2 leaf lands.

Capstone shape tests (R31 spelling discipline)

The two capstones are stated in their verbatim consumption shapes: the hZcount argument of blockStageR136 (GQ2/Block/RStage.lean:352) and the stageR136 field of GQ2.SourceData (GQ2/SourceData.lean:154) specialised at Γ := GammaR. Any future drift between these declarations and their consumers is caught here rather than in R32's sourceR.

The cardH2 leaf is deliberately not discharged in this file, so the field-shape test carries the same hcard_R hypothesis the chain threads — exactly the Γ_A split between RStageGammaA.stageR136_gammaA_of_hcard (hypothesis-side) and CardH2GammaA.stageR136_gammaA (leaf discharged), which is what BoundaryMaps.sourceA finally binds.