The Γ_R relator-correction calculus

The Roe-candidate twin of the correction layer of GQ2/RStage/GammaA.lean (sections WildCorrection, PushDescent, WordLiftMul) — the per-cover algebra the Γ_R (136)-stage separation argument (ticket R31e) and the Γ_R base-change/obstruction layers (R31f/R31g) run on.

Two independent pieces:

• Relator death along any continuous hom from Γ_R (no surjectivity, unlike markC_admissible_R): push_tameRelR / push_wildRelR, from tameRelator_mem_NR / wildRelatorR_mem_NR.

• The correction ledger of the Roe word. Correcting a marking's four generators by central involutions r⃗ (the shape of the kernel R/l ≅ 𝔽₂ at an L4 cover) shifts the Roe wild relator value by exactly the τ-correction:

  wildValueR_correction : (corrMark t r₀ r₁ r₂ r₃).wildValueR = r₁ * t.wildValueR

  — the same conclusion shape as Γ_A's RStageGammaA.wildValue_correction, so every downstream statement keeps its exact form. The ledger, however, is computed by a different (and shorter) chain, because Γ_A's nine auxiliary words u₀,u₁,g₀,z₀,d₀,c₀,dg,h_c,h₀ do not occur in r_R = (x₀^σ)⁻¹ · a · x₁² · c (note eq. (1.2) ⟦eq:relators⟧). The four Roe factors carry:

  factor	correction	why
  (x₀^σ)⁻¹	r₂	conjP_central_correction (r₀ cancels), then r₂⁻¹ = r₂
  a = (x₀⁻³τ)^ω₂	r₂r₁	corrMark_aR (r₂³ = r₂) + powOmega2_central_involution
  x₁²	none	corrMark_x1_sq (r₃² = 1)
  c = [x₁,y₁]	none	corrMark_cR via commP_central_correction

  and r₂ · r₂r₁ = r₁ is the whole ledger.

Finally the general (non-central) correction and base change at the Roe word: liftMarking_wildValueR_g, corrected_wildValueR (stated at d1FunR), and d1FunR_base_change.

Reused verbatim from GQ2/RStage/GammaA.lean, never cloned

powOmega2_central_involution, tameValue_correction (the tame relator is shared with Γ_A), conjP_central_correction, commP_central_correction, conjP_central_left, the corrMark definition itself together with corrMark_sigma2 (σ₂ is shared), marking_ext, and the WordLift multiplication calculus projW / mulW / baseW / liftMarking_map_projW / liftMarking_tameValue_g / corrected_tameValue / d1Fun_base_change. Only the two private helpers central_mul_comm / central_mul_sq are re-stated here (they are inaccessible across modules); central_pair is not needed for the Roe word.

Namespace. GQ2.RStageGammaR, mirroring GQ2.RStageGammaA, so that ticket R31e's port of hsep_hom_gammaA reads name-for-name against the Γ_A original.

Relator death along any continuous hom from Γ_R (L4)

theorem GQ2.RStageGammaR.push_tameRelR {G' : Type} [Group G'] [TopologicalSpace G'] (f : WordCohBridgeR.GR →ₜ* G') : (Marking.pushR f).TameRel

Relators die along any continuous hom from Γ_R, tame (Γ_R twin of RStageGammaA.push_tameRel; NO surjectivity, unlike markC_admissible_R): the pushed marking of any f : Γ_R →ₜ* G' satisfies the tame relation, because the tame relator word — shared with Γ_A — lies in N_R (tameRelator_mem_NR).

theorem GQ2.RStageGammaR.push_wildRelR {G' : Type} [Group G'] [TopologicalSpace G'] [DiscreteTopology G'] [Finite G'] (f : WordCohBridgeR.GR →ₜ* G') : (Marking.pushR f).WildRelR

Relators die along any continuous hom from Γ_R, wild — the Roe wild relator word lies in N_R (wildRelatorR_mem_NR, GQ2/Roe/AdmissibleLimit.lean). Γ_R twin of RStageGammaA.push_wildRel.

L1-wild for the Roe word — the correction chain at central involutions

theorem GQ2.RStageGammaR.corrMark_aR {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr1 : ∀ (z : Y'), Commute r1 z) (hr2 : ∀ (z : Y'), Commute r2 z) (hr1sq : r1 ^ 2 = 1) (hr2sq : r2 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).aR = r2 * r1 * t.aR

a = (x₀⁻³τ)^ω₂ picks up r₂r₁. The x₀-correction survives the odd power x₀⁻³ (r₂³ = r₂) and combines centrally with the τ-correction, then powOmega2_central_involution pushes the joint central involution r₂r₁ out of the ω₂-power. Replaces Γ_A's dead corrMark_u0/corrMark_u1.

theorem GQ2.RStageGammaR.corrMark_y1R {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr0 : ∀ (z : Y'), Commute r0 z) (hr3 : ∀ (z : Y'), Commute r3 z) (hr0sq : r0 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).y1R = r3 * t.y1R

y₁ = x₁^{σ₂} picks up r₃ (the conjugating σ₂-correction r₀ cancels) — the Roe counterpart of Γ_A's dead corrMark_z0, via the reused conjP_central_correction and the reused corrMark_sigma2 (σ₂ is shared with Γ_A).

theorem GQ2.RStageGammaR.corrMark_cR {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr0 : ∀ (z : Y'), Commute r0 z) (hr3 : ∀ (z : Y'), Commute r3 z) (hr0sq : r0 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).cR = t.cR

c = [x₁, y₁] is correction-free — both entries carry the same correction r₃, and commP kills central corrections (commP_central_correction). Roe counterpart of Γ_A's dead corrMark_c0/corrMark_hc.

theorem GQ2.RStageGammaR.corrMark_x1_sq {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} (hr3 : ∀ (z : Y'), Commute r3 z) (hr3sq : r3 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).x₁ ^ 2 = t.x₁ ^ 2

x₁² is correction-free (r₃² = 1) — the third Roe factor.

theorem GQ2.RStageGammaR.wildValueR_correction {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr0 : ∀ (z : Y'), Commute r0 z) (hr1 : ∀ (z : Y'), Commute r1 z) (hr2 : ∀ (z : Y'), Commute r2 z) (hr3 : ∀ (z : Y'), Commute r3 z) (hr0sq : r0 ^ 2 = 1) (hr1sq : r1 ^ 2 = 1) (hr2sq : r2 ^ 2 = 1) (hr3sq : r3 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).wildValueR = r1 * t.wildValueR

L1 wild row for the Roe word, central 2-torsion: the Roe wild relator value shifts by exactly the τ-correction r₁ —

wildValueR (r⃗ · ŷ) = r₁ · wildValueR ŷ,

the identical conclusion shape to Γ_A's RStageGammaA.wildValue_correction, reached by a different ledger: (x₀^σ)⁻¹ contributes r₂ (its r₀ cancels, and r₂⁻¹ = r₂), a contributes r₂r₁, and x₁², c are correction-free; the two r₂'s annihilate. Matches d1FunR_wild's x 1 slot.

theorem GQ2.RStageGammaR.corrMark_tameValue {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} (hr0 : ∀ (z : Y'), Commute r0 z) (hr1 : ∀ (z : Y'), Commute r1 z) (hr1sq : r1 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).tameValue = r1 * t.tameValue

The tame row at a corrMark correction, from the reused tameValue_correction (the tame relator is shared with Γ_A, and it does not read x₀/x₁, so the r₂/r₃ corrections are invisible to it).

theorem GQ2.RStageGammaR.corrMark_relator_correction {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr0 : ∀ (z : Y'), Commute r0 z) (hr1 : ∀ (z : Y'), Commute r1 z) (hr2 : ∀ (z : Y'), Commute r2 z) (hr3 : ∀ (z : Y'), Commute r3 z) (hr0sq : r0 ^ 2 = 1) (hr1sq : r1 ^ 2 = 1) (hr2sq : r2 ^ 2 = 1) (hr3sq : r3 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).tameValue = r1 * t.tameValue ∧ (RStageGammaA.corrMark t r0 r1 r2 r3).wildValueR = r1 * t.wildValueR

Stress test (consumption shape). Both Γ_R relator rows shift by the same central involution r₁ — the fact the (136)-stage separation argument (ticket R31e) consumes, and exactly the Γ_A pairing tameValue_correction/wildValue_correction. Pins that the Roe wild ledger did not acquire a stray r₀/r₂/r₃.

theorem GQ2.RStageGammaR.wildValueR_correction_tau_only {Y' : Type u_1} [Group Y'] {t : Marking Y'} {r0 r1 r2 r3 : Y'} [Finite Y'] (hr0 : ∀ (z : Y'), Commute r0 z) (hr1 : ∀ (z : Y'), Commute r1 z) (hr2 : ∀ (z : Y'), Commute r2 z) (hr3 : ∀ (z : Y'), Commute r3 z) (hr0sq : r0 ^ 2 = 1) (hr1sq : r1 ^ 2 = 1) (hr2sq : r2 ^ 2 = 1) (hr3sq : r3 ^ 2 = 1) : (RStageGammaA.corrMark t r0 r1 r2 r3).wildValueR = (RStageGammaA.corrMark t 1 r1 1 1).wildValueR

Stress test (only the τ-correction survives). The corrected Roe wild relator value is unchanged if r₀, r₂, r₃ are replaced by 1 — an independent pin on the ledger's cancellation (r₂ against r₂, r₃ against nothing since x₁² and c are correction-free).

The general (non-central) correction and base change at the Roe word

The WordLift multiplication calculus projW/mulW/baseW is relator-independent and reused from RStageGammaA; only the three statements that mention wildValueR/d1FunR are re-derived.

theorem GQ2.RStageGammaR.liftMarking_wildValueR_g {G : Type u_1} [Group G] {A : Type u_2} [AddCommGroup A] [DistribMulAction G A] [Finite G] [Finite A] (t : Marking G) (x : Fin 4 → A) : (FoxH.liftMarking t x).wildValueR.g = t.wildValueR

The base coordinate of the evaluated Roe wild relator is the base Roe wild relator value (finite: the ω₂-push). Γ_R twin of RStageGammaA.liftMarking_wildValue_g.

theorem GQ2.RStageGammaR.corrected_wildValueR {G : Type u_1} [Group G] {A : Type u_2} [AddCommGroup A] [DistribMulAction G A] [Finite G] [Finite A] (j : A → G) (hjmul : ∀ (a b : A), j (a + b) = j a * j b) (hjconj : ∀ (g : G) (a : A), j (g • a) = g * j a * g⁻¹) (t : Marking G) (x : Fin 4 → A) : { σ := j (x 0) * t.σ, τ := j (x 1) * t.τ, x₀ := j (x 2) * t.x₀, x₁ := j (x 3) * t.x₁ }.wildValueR = j (FoxH.d1FunR t x).2 * t.wildValueR

The general relator correction, Roe wild row: left-multiplying a marking's generators by the j-realizations of coefficients x multiplies the Roe wild relator value by j of the wild d¹_R-row. (Evaluate r_R in A ⋊ G and push through mulW.) Γ_R twin of RStageGammaA.corrected_wildValue, stated at d1FunR.

theorem GQ2.RStageGammaR.d1FunR_base_change {G : Type u_1} [Group G] {A : Type u_2} [AddCommGroup A] [DistribMulAction G A] [Finite G] [Finite A] {C : Type u_3} [Group C] [DistribMulAction C A] (f : G →* C) (hcompat : ∀ (g : G) (a : A), g • a = f g • a) (t : Marking G) (x : Fin 4 → A) : FoxH.d1FunR (Marking.map f t) x = FoxH.d1FunR t x

d¹_R base change: the Roe word differential only sees the action, so it is computed by the pushed marking — d1FunR (t.map f) x = d1FunR t x when the G-action is pulled back along f. Γ_R twin of RStageGammaA.d1Fun_base_change; the tame slot is free because the tame row is shared (d1FunR_fst), only the wild slot is re-derived.

Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained)

• eq. (1.1) = ⟦eq:defwords⟧ — the auxiliary words a, y₁, c whose corrections are computed here (corrMark_aR, corrMark_y1R, corrMark_cR).
• eq. (1.2) = ⟦eq:relators⟧ — the Roe relator whose correction ledger is wildValueR_correction.