Γ_R and the Roe-candidate marked quotient (Roe note §1, Definition 1.1 ⟦def:GammaR⟧)

The Roe-candidate group, defined by the same marked-quotient construction as Γ_A (GQ2/GammaA.lean, paper §2.1 eq. (7)): let F₄ be the free profinite group on σ, τ, x₀, x₁; call a finite quotient φ : F₄ ⟶ G R-admissible if the pushed marking generates G, satisfies the tame relation τ^σ = τ² and the Roe wild relation r_R = 1 (note eq. (1.2) ⟦eq:relators⟧, verbatim \rR=(x_0^\sigma)^{-1}a\,x_1^2c), and the normal closure of the images of x₀, x₁ is a 2-group; then

N_R = ⋂ {ker φ | φ R-admissible}, Γ_R = F₄ ⧸ N_R.

Only the wild relation differs from Γ_A: the tame relation, the pro-2 condition, and the whole marked-quotient scaffolding (univMarking, Marking.toHom, surjective_of_map_generates) are reused verbatim from GQ2/GammaA.lean.

This file provides the Roe relation r_R in its profinite reading: the note's auxiliary words of eq. (1.1) ⟦eq:defwords⟧ with genuine ω₂ ∈ ℤ̂ exponents (Marking.aRHat, Marking.y1RHat, Marking.cRHat, Marking.wildRelatorR, via ^ᶻ omega2 from GQ2/Zhat.lean; the σ₂ = σ^{ω₂} letter reuses the shared Marking.sigma2Hat of Γ_A). The fidelity bridge Marking.map_wildRelatorR / Marking.map_wildRelatorR_eq_one_iff proves that pushing the profinite word wildRelatorR through a finite quotient computes exactly Marking.wildValueR of GQ2/Roe/Words.lean — so killing the profinite relator is the same condition as the finite Roe wild relation WildRelR, and the R-admissibility used in N_R is exactly the note's.

Alongside Γ_R this file supplies Marking.map_admissibleR (R-admissibility pushes forward along surjective quotient maps — the Roe counterpart of Marking.map_admissible, GQ2/Subdirect.lean) and the certificate NR_le_ker (every R-admissible continuous hom to a finite group has N_R in its kernel). The limit facts about Γ_R itself (relators die, admissible-opens characterization, pro-2 wild core) are GQ2/Roe/AdmissibleLimit.lean.

The Roe auxiliary words with genuine profinite ω₂-exponents (note eq. (1.1))

noncomputable def GQ2.Marking.aRHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (t : Marking G) : G

a = (x₀⁻³ τ)^{ω₂} (note eq. (1.1) ⟦eq:defwords⟧, verbatim a=(x_0^{-3}\tau)^{\omegaTwo}), profinite reading with the genuine profinite exponent ω₂ ∈ ℤ̂. The finite counterpart is Marking.aR (GQ2/Roe/Words.lean).

Equations

• t.aRHat = GQ2.zpowHat ((t.x₀ ^ 3)⁻¹ * t.τ) GQ2.omega2

noncomputable def GQ2.Marking.y1RHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (t : Marking G) : G

y₁ = x₁^{σ₂} (note eq. (1.1) ⟦eq:defwords⟧, verbatim y_1=x_1^{\sigma_2}), profinite reading, reusing the shared σ₂ = σ^{ω₂} = Marking.sigma2Hat of Γ_A. Finite counterpart Marking.y1R.

Equations

• t.y1RHat = GQ2.conjP t.x₁ t.sigma2Hat

noncomputable def GQ2.Marking.cRHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (t : Marking G) : G

c = [x₁, y₁] (note eq. (1.1) ⟦eq:defwords⟧, verbatim c=[x_1,y_1]), profinite reading. Finite counterpart Marking.cR.

Equations

• t.cRHat = GQ2.commP t.x₁ t.y1RHat

noncomputable def GQ2.Marking.wildRelatorR {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (t : Marking G) : G

The Roe wild relator word r_R = (x₀^σ)⁻¹ · a · x₁² · c (note eq. (1.2) ⟦eq:relators⟧, verbatim \rR=(x_0^\sigma)^{-1}a\,x_1^2c), in the profinite reading — its ω₂-letters (inside aRHat and inside cRHat's sigma2Hat) use the genuine profinite exponents above. The Γ_A analogue is Marking.wildRelator; the finite value is Marking.wildValueR (GQ2/Roe/Words.lean).

Equations

• t.wildRelatorR = (GQ2.conjP t.x₀ t.σ)⁻¹ * t.aRHat * t.x₁ ^ 2 * t.cRHat

Faithfulness bridge: the profinite Roe word evaluates to the finite Roe word

Through any continuous homomorphism to a finite group, the ^ᶻ omega2-ledger of wildRelatorR computes the powOmega2-ledger wildValueR of GQ2/Roe/Words.lean — via the profinite- exponentiation headline map_zpowHat_omega2, pushed through the three Roe letters. In particular the Roe relation read profinitely (relator dies) and finitely (WildRelR of the pushed marking) are the same condition (map_wildRelatorR_eq_one_iff) — the fidelity-critical lemma, exactly mirroring GQ2.Marking.map_wildRelator_eq_one_iff.

theorem GQ2.Marking.map_wildRelatorR {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Type} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P] (f : G →ₜ* P) (t : Marking G) : f.toMonoidHom t.wildRelatorR = (map f.toMonoidHom t).wildValueR

Word-for-word fidelity: the profinite Roe wild relator evaluates, through any finite quotient, to the finite Roe wild relator value Marking.wildValueR of the pushed marking — the content underlying map_wildRelatorR_eq_one_iff. (The Γ_A monolithic analogue is folded into GQ2.Marking.map_wildRelator_eq_one_iff; here it is exposed separately as a stress test.)

theorem GQ2.Marking.map_wildRelatorR_eq_one_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Type} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P] (f : G →ₜ* P) (t : Marking G) : f.toMonoidHom t.wildRelatorR = 1 ↔ (map f.toMonoidHom t).WildRelR

Roe relation r_R, profinite = finite: the Roe wild relator word dies in a finite quotient iff the pushed marking satisfies the Roe wild relation WildRelR of GQ2/Roe/Words.lean. Direct analogue of GQ2.Marking.map_wildRelator_eq_one_iff.

R-admissibility pushes forward (Roe counterpart of Marking.map_admissible)

theorem GQ2.Marking.map_admissibleR {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] [Finite H] (f : G →* H) (hf : Function.Surjective ⇑f) (t : Marking G) (ht : t.AdmissibleR) : (map f t).AdmissibleR

R-admissibility pushes forward along surjective quotient maps (Roe counterpart of GQ2.Marking.map_admissible, paper §2 Lemmas 2.1–2.2). If t is an R-admissible marking of a finite group G and f : G ↠ H is a surjective homomorphism of finite groups, then t.map f is R-admissible. Only the wild clause differs from map_admissible: map_wildRelR (of GQ2/Roe/Words.lean) replaces map_wildRel; generation, the tame relation and the 2-core clause are word-independent (R1 report).

N_R and Γ_R (Roe note Definition 1.1 ⟦def:GammaR⟧; same shape as paper §2.1 eq. (7))

def GQ2.IsAdmissibleUR (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : Prop

An open normal subgroup U ≤ F₄ is R-admissible (note Definition 1.1 ⟦def:GammaR⟧) if the canonical finite quotient F₄ ⧸ U carries an R-admissible pushed marking: the images of σ, τ, x₀, x₁ generate, satisfy the tame relation and the Roe wild relation — equivalently (by map_tameRelator_eq_one_iff / map_wildRelatorR_eq_one_iff) the profinite relator words die — and the normal closure of the images of x₀, x₁ is a 2-group. Roe counterpart of GQ2.IsAdmissibleU.

Equations

• GQ2.IsAdmissibleUR U = (GQ2.Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) GQ2.univMarking).AdmissibleR

noncomputable def GQ2.NR : Subgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop

N_R (note Definition 1.1 ⟦def:GammaR⟧): the intersection of the kernels of all R-admissible finite quotients of F₄, encoded as the intersection of all R-admissible open normal subgroups. Roe counterpart of GQ2.NA.

Equations

• GQ2.NR = ⨅ (U : { U : OpenNormalSubgroup ↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop // GQ2.IsAdmissibleUR U }), ↑(↑U).toOpenSubgroup

instance GQ2.NR_normal : NR.Normal

theorem GQ2.NR_isClosed : IsClosed ↑NR

noncomputable def GQ2.GammaR : ProfiniteGrp.{0}

Γ_R (note Definition 1.1 ⟦def:GammaR⟧): the marked quotient F₄ ⧸ N_R — the largest quotient of F₄ all of whose finite quotients are R-admissible, constructed exactly as Γ_A but with the Roe wild relation. Roe counterpart of GQ2.GammaA.

Equations

• GQ2.GammaR = GQ2.profiniteQuotient GQ2.NR

theorem GQ2.NR_le_ker {P : Type} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P] (f : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* P) (hf : (Marking.map f.toMonoidHom univMarking).AdmissibleR) : NR ≤ f.ker

N_R is the note's intersection (Definition 1.1 ⟦def:GammaR⟧): the kernel of every R-admissible continuous hom to a finite (discrete) group — not just the canonical quotients F₄ ⧸ U — contains N_R. (The pushed marking being R-admissible forces f surjective, and R-admissibility transfers to the canonical quotient by the induced isomorphism F₄ ⧸ ker f ≃* P.) Roe counterpart of GQ2.NA_le_ker.

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

• eq. (1.1) = ⟦eq:defwords⟧
• eq. (1.2) = ⟦eq:relators⟧
• Definition 1.1 = ⟦def:GammaR⟧