The Γ_R cover-lift kernel (L4) and relator-free descent (L5)

The Roe-candidate twin of the CoverLift/Descend sections of GQ2/RStage/GammaA.lean (:726–954) — the two lemmas the Γ_R separation arguments run on. Both are stated free of any (136)-frame context (no H/E/T/Blk/RecursionFrame), because they have two independent consumers: the (136) R-stage (GQ2/RStage/GammaR.lean, ticket R31e) and the (140) T-stage (ticket R31f), whose Γ_A originals instantiate the shared Y at the section variable and at the frame field RF.YB respectively.

L4 — redValues_eq_of_coverLift_R

If a boundary map g_B : Γ_R → B₀ lifts through a central double cover Q, then any set-lift marking t_Y of g_B has equal tame and Roe-wild relator values after reduction along red : Y → Q.cover. Both t_Y.map red and the lift's pushed marking cover g_B's marking, so they differ by corrections in the central 2-torsion kernel ⟨z⟩; the correction ledger (tameValue_correction, shared with Γ_A, and wildValueR_correction, GQ2/Roe/CorrectionR.lean) evaluates both reduced relator values to the same r̄₁ — this is exactly why the two Roe rows had to shift by the same central involution.

Statement shape is binder-for-binder the Γ_A original RStageGammaA.redValues_eq_of_coverLift, with Marking.push → Marking.pushR, gammaGen → gammaGenR, GA → GR, wildValue → wildValueR; the instance context is even weaker (no TopologicalSpace/DiscreteTopology on Y or B₀).

L5 — the relator-free descent, factored

The Γ_A original (RStage/GammaA.lean:829) is private and hard-wired to the block frame (blockFrameImpl T Blk hE2, Blk.frattiniK), which is precisely why GQ2/Phase140/GammaA/ could not reuse it and re-proved a generalised variant (mlift_of_relatorFree_marking, Foundation.lean:461). To avoid repeating that split on the Roe side, the descent is factored here into three public pieces:

• exists_pushR_eq_of_relatorFree — the frame-free core: a marking of Y that kills both Γ_R relators and has a pro-2 wild core is the pushforward of a continuous φ : Γ_R → Y. No π, no B₀, no surjectivity: the cleanest form of "Γ_R classifies relator-free markings".
• isPGroup_wildCore_of_proj — the Pro2Core transfer: an upstairs pro-2 certificate from a downstairs one plus 2-torsion of ker π (the hcoreJ chase of the Γ_A original, restated in Y so it can be reused independently).
• lift_of_relatorFree_markingR — the consumer-facing splice of the two, over an abstract π : Y →* B₀. Strictly more general than the Γ_A original: π is arbitrary (not blockFrameImpl.piB), the kernel torsion is a hypothesis (not hR2 + ker_piB), and the Pro2Core input is taken directly rather than through Function.Surjective g_B — so the non-surjective T-stage of R31f can supply it after its corestriction, instead of cloning.

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

corrMark, marking_ext, tameValue_correction (the tame relator is shared with Γ_A). The Roe-specific inputs are RStageGammaR.push_tameRelR / push_wildRelR / wildValueR_correction (GQ2/Roe/CorrectionR.lean), Marking.pushR / Marking.descendR / Marking.pushR_descendR (GQ2/Roe/Prop23.lean) and gammaGenR (GQ2/WordCohBridgeR.lean).

Module-system note. Plain import (non-module), like its import GQ2.Roe.CorrectionR and that file's own import GQ2.RStage.GammaA: module-style files cannot import plain ones.

Axioms: none introduced (std-3 only).

L4 core: a cover lift forces equal reduced relator values

theorem GQ2.RStageGammaR.redValues_eq_of_coverLift_R {Y : Type} [Group Y] [Finite Y] {B0 : Type} [Group B0] [Finite B0] [TopologicalSpace B0] (Q : SectionEight.CentralCover B0) (piB : Y →* B0) (red : Y →* Q.cover) (hred_p : Q.p.comp red = piB) (gB : WordCohBridgeR.GR →ₜ* B0) (gc : WordCohBridgeR.GR →ₜ* Q.cover) (hgc : ∀ (γ : WordCohBridgeR.GR), Q.p (gc γ) = gB γ) (tY : Marking Y) (hproj : Marking.map piB tY = Marking.pushR gB) : red tY.tameValue = red tY.wildValueR

The per-cover L4 core for Γ_R, abstractly over a bare central cover: if g_B lifts through Q (via gc), then any set-lift marking tY of g_B has equal tame and Roe-wild relator values after reduction along red. Both tY.map red and the lift's pushed marking cover g_B's marking, so they differ by corrections in the central 2-torsion kernel (CentralCover.central/z_sq); the correction calculus (tameValue_correction, shared with Γ_A, and wildValueR_correction) evaluates both reduced relator values to the same r̄₁.

Γ_R twin of RStageGammaA.redValues_eq_of_coverLift, binder-for-binder. Deliberately free of frame context so that both the (136) R-stage (R31e) and the (140) T-stage (R31f) can instantiate Y at their own carriers.

L5 descent: a relator-free covering marking of Y descends from Γ_R

theorem GQ2.RStageGammaR.exists_pushR_eq_of_relatorFree {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (tHat : Marking Y) (htame : tHat.TameRel) (hwild : tHat.WildRelR) (hcore : IsPGroup 2 ↥(Subgroup.normalClosure {tHat.x₀, tHat.x₁})) : ∃ (φ : WordCohBridgeR.GR →ₜ* Y), Marking.pushR φ = tHat

L5 core, frame-free: a marking of Y that kills both Γ_R relators and whose wild core is pro-2 is the pushforward of a continuous φ : Γ_R → Y. The marking generates a subgroup J ≤ Y on which it is R-admissible (Generates by construction; TameRel/WildRelR by subtype injectivity; Pro2Core by pulling the Y-certificate back along the injective J.subtype), hence Marking.descendR applies and Marking.pushR_descendR returns the marking.

This is the honest content of the Γ_A original lift_of_relatorFree_marking, stripped of the block frame — the π/g_B projection statement is the corollary lift_of_relatorFree_markingR below.

theorem GQ2.RStageGammaR.isPGroup_wildCore_of_proj {Y : Type} [Group Y] {B0 : Type} [Group B0] [TopologicalSpace B0] (π : Y →* B0) (hker2 : ∀ y ∈ π.ker, y * y = 1) (gB : WordCohBridgeR.GR →ₜ* B0) (hcoreB : (Marking.pushR gB).Pro2Core) (tHat : Marking Y) (hproj : Marking.map π tHat = Marking.pushR gB) : IsPGroup 2 ↥(Subgroup.normalClosure {tHat.x₀, tHat.x₁})

The Pro2Core transfer. If t_Y covers g_B's marking through π and the elements of ker π are involutions, then a pro-2 wild core downstairs gives one upstairs: an element of the normal closure of {x₀, x₁} in Y maps into the normal closure downstairs, so some 2^k-th power lands in ker π, and one more squaring kills it.

This is the hcoreJ chase of RStageGammaA.lift_of_relatorFree_marking (:877–916), restated in Y and detached from blockFrameImpl/Blk.frattiniK so that both Γ_R stages can feed it their own kernel-torsion certificate.

theorem GQ2.RStageGammaR.lift_of_relatorFree_markingR {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {B0 : Type} [Group B0] [TopologicalSpace B0] [DiscreteTopology B0] [Finite B0] (π : Y →* B0) (hker2 : ∀ y ∈ π.ker, y * y = 1) (gB : WordCohBridgeR.GR →ₜ* B0) (hcoreB : (Marking.pushR gB).Pro2Core) (tHat : Marking Y) (hproj : Marking.map π tHat = Marking.pushR gB) (htame : tHat.TameRel) (hwild : tHat.WildRelR) : ∃ (φ : ↑GammaR.toProfinite.toTop →ₜ* Y), ∀ (γ : ↑GammaR.toProfinite.toTop), π (φ γ) = gB γ

L5, the descent (consumer-facing form): a marking of Y that covers g_B's marking through an arbitrary π : Y →* B₀ and kills both Γ_R relators descends to a continuous φ : Γ_R → Y with π ∘ φ = g_B. The projection identity holds because two F₄-classified homs with equal pushed markings agree (Marking.toHom_hom_univMarking_map).

Γ_R twin of the private RStageGammaA.lift_of_relatorFree_marking, and strictly more general: π is abstract, the kernel torsion is a hypothesis, and Pro2Core is taken directly instead of via Function.Surjective g_B — which is exactly what the non-surjective (140) T-stage needs (cf. GQ2/Phase140/GammaA/Foundation.lean:461, where the Γ_A side had to clone).

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

• eq. (1.2) = ⟦eq:relators⟧ — the Roe wild relator whose central-involution correction ledger (wildValueR_correction) makes the two reduced relator values coincide in L4.
• Definition 1.1 = ⟦def:GammaR⟧ — N_R/AdmissibleR, via Marking.descendR in L5.