The tame quotient of Γ_R and the unramified character (Roe note §2, Lemma 2.1 ⟦lem:tame⟧)

Formalizes the note's §2 for the Roe-candidate group Γ_R (GQ2/Roe/GammaR.lean). With W_R = ⟪x₀, x₁⟫ the closed normal closure of the wild generators (GQ2.wildCoreR, R3), the note's Lemma 2.1 ⟦lem:tame⟧ asserts, verbatim,

The quotient by W_R is the standard tame group  T_R = ⟨σ, τ | τ^σ = τ²⟩.
Moreover  ν_R(σ)=1,  ν_R(τ)=ν_R(x_0)=ν_R(x_1)=0
defines a continuous epimorphism  ν_R : Γ_R ↠ ℤ₂.

together with the O₂-corollary (note, after ⟦lem:tame⟧, verbatim W_R=O_2(\GammaR)).

The proof mirrors the Γ_A side (GQ2/Prop32.lean, GQ2/SectionTenSources.lean) with an R suffix, so the P5 assembly (R32) consumes the results as drop-ins for the tame/pro-2 discharge:

• Finite-level redundancy of the wild relation (⟦lem:tame⟧, first half): in any finite group a marking with t.TameRel has powOmega2 t.τ = 1 (τ of odd order, Lemma 3.1); and after killing x₀, x₁ the Roe wild value collapses t.wildValueR = powOmega2 t.τ, so the Roe wild relation is automatic (Marking.powOmega2_tau_eq_one_of_tameRel, Marking.wildValueR_of_trivial_wild, Marking.wildRelR_of_trivial_wild).
• The tame coordinate phiR : Γ_R →ₜ* T_tame (σ, τ ↦ σ, τ, x₀, x₁ ↦ 1), descended from the shared classifier through N_R (using the redundancy above at every finite level of T_tame), with phiR_surjective and ker phiR = W_R (ker_phiR, via the marked iso tameREquiv, the Γ_R side of Prop. 3.2). These have the exact statement shapes of phiA_surjective / ker_phiA.
• W_R = O₂(Γ_R) (wildCoreR_isMax): every closed normal pro-2 subgroup lies in W_R. Since W_R is itself pro-2 (GQ2.isProP_wildCoreR, R3), W_R is the largest — the maximal-closed-normal- pro-2 shape of the BoundaryMaps.wild_isMax field, proved here without axiom B10 (B10 concerns G_ℚ₂'s tame quotient) from T_tame's intrinsic eq_bot_of_normal_two_images (whose engine is Lemma 3.1's tame_normal_two_subgroup_central).
• The unramified character nuR : Γ_R →ₜ* Z₂ (nuT ∘ phiR; σ ↦ 1, τ, x₀, x₁ ↦ 0) with nuR_surjective, in the ν-shape the boundary bundle's compatA-field consumes (nuT (phiR g) on the tame side, GQ2/BoundaryFrame.lean).

Finite-level facts: the Roe wild relation is redundant after killing x₀, x₁

Note ⟦lem:tame⟧, first half. In a finite quotient of ⟨σ, τ | τ^σ = τ²⟩ conjugation preserves the order of τ, so τ and τ² have equal order, forcing τ of odd order and hence τ^{ω₂} = 1. For the killed-wild marking (σ, τ, 1, 1) the Roe wild value r_R = (x₀^σ)⁻¹ · a · x₁² · c collapses to a = (x₀⁻³τ)^{ω₂}|_{x₀=1} = τ^{ω₂} (the conjugation and commutator factors die), so r_R = 1.

theorem GQ2.Marking.powOmega2_tau_eq_one_of_tameRel {G : Type u_1} [Group G] [Finite G] (t : Marking G) (h : t.TameRel) : powOmega2 t.τ = 1

⟦lem:tame⟧ (odd-order collapse). In a finite group, a marking satisfying the tame relation τ^σ = τ² has τ of odd order (Lemma 3.1, GQ2.Tame.tame_odd_order), hence its ω₂-power is trivial. The tame-frame input to the redundancy of the Roe wild relation.

theorem GQ2.Marking.wildValueR_of_trivial_wild {G : Type u_1} [Group G] (t : Marking G) (hx0 : t.x₀ = 1) (hx1 : t.x₁ = 1) : t.wildValueR = powOmega2 t.τ

⟦lem:tame⟧ (killed-wild collapse of r_R). When both wild generators are trivial, the Roe wild value reduces to powOmega2 t.τ: the first factor (x₀^σ)⁻¹ = 1, the auxiliary commutator c = [x₁, y₁] = 1 and x₁² = 1 all die, leaving a = (x₀⁻³τ)^{ω₂} = τ^{ω₂}. Roe counterpart of the Γ_A-side collapse GQ2.Marking.wildRel_of_trivial_wild, but stated as the exact value.

theorem GQ2.Marking.wildRelR_of_trivial_wild {G : Type u_1} [Group G] (t : Marking G) (hx0 : t.x₀ = 1) (hx1 : t.x₁ = 1) (hτ : powOmega2 t.τ = 1) : t.WildRelR

⟦lem:tame⟧ (wild relation redundant). If both wild generators are trivial and τ has trivial ω₂-power (e.g. τ of odd order, powOmega2_tau_eq_one_of_tameRel), the Roe wild relation r_R = 1 holds automatically. Roe counterpart of GQ2.Marking.wildRel_of_trivial_wild; the finite-level input for φ_R's classifier being R-admissible at every tame level.

The tame coordinate φ_R : Γ_R ↠ T_tame (⟦lem:tame⟧, tame-quotient claim)

The classifier F₄ → T_tame (σ, τ ↦ σ, τ, x₀, x₁ ↦ 1) is the one shared with Γ_A (GQ2.SectionThree.tameClassifier). It kills N_R: through every finite level of T_tame the pushed marking (σ̄, τ̄, 1, 1) is R-admissible — the three word-independent clauses come from the Γ_A computation, and the Roe wild relation is redundant by the collapse above. Descending gives φ_R.

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

The image of σ in Γ_R = F₄ ⧸ N_R.

Equations

• GQ2.gammaSigmaR = (GQ2.quotientMk GQ2.NR) GQ2.univMarking.σ

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

The image of τ in Γ_R = F₄ ⧸ N_R.

Equations

• GQ2.gammaTauR = (GQ2.quotientMk GQ2.NR) GQ2.univMarking.τ

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

The image of x₀ in Γ_R = F₄ ⧸ N_R.

Equations

• GQ2.gammaX0R = (GQ2.quotientMk GQ2.NR) GQ2.univMarking.x₀

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

The image of x₁ in Γ_R = F₄ ⧸ N_R.

Equations

• GQ2.gammaX1R = (GQ2.quotientMk GQ2.NR) GQ2.univMarking.x₁

theorem GQ2.isAdmissibleR_tameClassifier_level (V : OpenNormalSubgroup ↑Ttame.toProfinite.toTop) : (Marking.map ((QuotientGroup.mk' ↑V.toOpenSubgroup).comp (ProfiniteGrp.Hom.hom SectionThree.tameClassifier).toMonoidHom) univMarking).AdmissibleR

Through every open normal level of T_tame, the marking pushed from the shared classifier is R-admissible. The generation, tame-relation and pro-2-core clauses are word-independent (taken from the Γ_A computation isAdmissible_tameClassifier_level); the Roe wild relation is redundant because the marking is (σ̄, τ̄, 1, 1) with τ̄ of odd order (⟦lem:tame⟧).

theorem GQ2.NR_le_ker_tameClassifier : NR ≤ (ProfiniteGrp.Hom.hom SectionThree.tameClassifier).ker

N_R is contained in the kernel of the shared classifier F₄ → T_tame (each finite level is an R-admissible quotient, isAdmissibleR_tameClassifier_level, so NR_le_ker applies).

noncomputable def GQ2.phiR : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* ↑Ttame.toProfinite.toTop

φ_R : Γ_R → T_tame, the descent of the classifier (σ, τ ↦ σ, τ, x₀, x₁ ↦ 1). Roe counterpart of GQ2.SectionThree.phiA.

Equations

• GQ2.phiR = GQ2.quotientLift GQ2.NR (ProfiniteGrp.Hom.hom GQ2.SectionThree.tameClassifier) GQ2.NR_le_ker_tameClassifier

@[simp]

theorem GQ2.phiR_gammaSigma : phiR gammaSigmaR = tameSigma

@[simp]

theorem GQ2.phiR_gammaTau : phiR gammaTauR = tameTau

@[simp]

theorem GQ2.phiR_gammaX0 : phiR gammaX0R = 1

@[simp]

theorem GQ2.phiR_gammaX1 : phiR gammaX1R = 1

theorem GQ2.wildCoreR_le_ker_phiR : wildCoreR ≤ phiR.ker

W_R ≤ ker φ_R (the wild generators map to 1, and the kernel is closed normal). Roe counterpart of GQ2.SectionThree.wildPartB_le_ker_phiA.

The marked iso Γ_R / W_R ≅ T_tame (Prop. 3.2, Γ_R side)

Exactly the Γ_A construction (GQ2/Prop32.lean): the presentation T_tame = ⟨σ, τ | τ^σ = τ²⟩ lets us build the section χ_R : T_tame → Γ_R/W_R (the tame relator dies in Γ_R/W_R because tameRelator ∈ N_R, R3), and the two composites with the descent ψ_R = φ_R / W_R are the identity by density of the marked generators.

noncomputable def GQ2.TameR : ProfiniteGrp.{0}

Γ_R / W_R as a profinite group (for the universal property of T_tame's presentation).

Equations

• GQ2.TameR = GQ2.profiniteQuotient GQ2.wildCoreR

noncomputable def GQ2.chiBaseR : FreeProfiniteGroup (Fin 2) ⟶ TameR

The base map F₂ ⟶ Γ_R/W_R: σ ↦ σ̄, τ ↦ τ̄.

Equations

• GQ2.chiBaseR = (GQ2.FreeProfiniteGroup.homEquiv (Fin 2) GQ2.TameR).symm ![(GQ2.quotientMk GQ2.wildCoreR) GQ2.gammaSigmaR, (GQ2.quotientMk GQ2.wildCoreR) GQ2.gammaTauR]

theorem GQ2.chiBaseR_tameWord : (ProfiniteGrp.Hom.hom chiBaseR).toMonoidHom tameWord = 1

The base map kills the tame relator: its image is the W_R-class of the Γ_R-image of univMarking.tameRelator ∈ N_R (R3's tameRelator_mem_NR).

noncomputable def GQ2.chiWR : ↑Ttame.toProfinite.toTop →ₜ* ↑TameR.toProfinite.toTop

χ_R : T_tame → Γ_R/W_R, by the universal property of the presentation.

Equations

• GQ2.chiWR = GQ2.presentationLift {GQ2.tameWord} (ProfiniteGrp.Hom.hom GQ2.chiBaseR) ⋯

noncomputable def GQ2.psiWR : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) ⧸ wildCoreR →ₜ* ↑Ttame.toProfinite.toTop

ψ_R : Γ_R/W_R → T_tame, the descent of φ_R.

Equations

• GQ2.psiWR = GQ2.quotientLift GQ2.wildCoreR GQ2.phiR GQ2.wildCoreR_le_ker_phiR

theorem GQ2.topGen_tameR : (Subgroup.closure (Set.range fun (i : Fin 4) => (quotientMk wildCoreR) ((quotientMk NR) (FreeProfiniteGroup.of i)))).topologicalClosure = ⊤

Γ_R/W_R is topologically generated by the classes of the four marked generators.

theorem GQ2.psiWR_chiWR (x : ↑Ttame.toProfinite.toTop) : psiWR (chiWR x) = x

ψ_R ∘ χ_R = id on T_tame (both send σ ↦ σ, τ ↦ τ; density).

theorem GQ2.chiWR_psiWR (x : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) ⧸ wildCoreR) : chiWR (psiWR x) = x

χ_R ∘ ψ_R = id on Γ_R/W_R (checked on the four marked generator classes; density).

noncomputable def GQ2.tameREquiv : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) ⧸ wildCoreR ≃ₜ* ↑Ttame.toProfinite.toTop

Prop. 3.2, Γ_R side (⟦lem:tame⟧, tame-quotient claim): the marked isomorphism Γ_R / W_R ≅ T_tame, σ̄ ↦ σ, τ̄ ↦ τ. Roe counterpart of GQ2.SectionThree.tameAEquiv.

Equations

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

The discharge package for R32: surjectivity, kernel, and W_R = O₂

theorem GQ2.phiR_surjective : Function.Surjective ⇑phiR

htame for Γ_R: φ_R is onto (Prop 3.2, via tameREquiv). Statement shape of GQ2.SectionThree.phiA_surjective.

theorem GQ2.ker_phiR : phiR.ker = wildCoreR

ker φ_R = W_R. ⊇ is wildCoreR_le_ker_phiR; ⊆ because the descent ψ_R = φ_R / W_R is injective — it is the underlying map of the Prop-3.2 iso tameREquiv. Statement shape of GQ2.SectionTen.ker_phiA; consumed by R32 as the wild-inertia identification.

theorem GQ2.wildCoreR_isMax (N : Subgroup (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) (hNn : N.Normal) (_hNc : IsClosed ↑N) (hNp : IsProP 2 ↥N) : N ≤ wildCoreR

W_R = O₂(Γ_R) (note, after ⟦lem:tame⟧, verbatim W_R=O_2(\GammaR)): every closed normal pro-2 subgroup of Γ_R lies in W_R. Since W_R is itself closed normal pro-2 (wildCoreR_normal, wildCoreR_isClosed, GQ2.isProP_wildCoreR), it is the largest — i.e. O₂(Γ_R). Proved from T_tame's intrinsic triviality of normal pro-2 subgroups (eq_bot_of_normal_two_images, whose engine is Lemma 3.1's tame_normal_two_subgroup_central) applied to the image under φ_R; independent of axiom B10. This is the wild_isMax-shape of BoundaryMaps.

The unramified character ν_R : Γ_R ↠ Z₂ (⟦lem:tame⟧, second half)

ν_R = ν_t ∘ φ_R factors the standard unramified character through the tame quotient — the "geometric unramified character" of the note. Its values σ ↦ 1, τ, x₀, x₁ ↦ 0 are exactly the tame-side ν-datum the boundary bundle's compatA-field (nuT (tameA g), GQ2/BoundaryFrame.lean) consumes; surjectivity is ν_t onto composed with φ_R onto.

noncomputable def GQ2.nuR : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* ↑Ztwo.toProfinite.toTop

ν_R : Γ_R → Z₂ (⟦lem:tame⟧): ν_R(σ) = 1, ν_R(τ) = ν_R(x₀) = ν_R(x₁) = 0, as ν_t ∘ φ_R. Roe counterpart of the tame-side ν_t ∘ tameA of GQ2.BoundaryMaps.

Equations

• GQ2.nuR = GQ2.nuT.comp GQ2.phiR

@[simp]

theorem GQ2.nuR_gammaSigma : nuR gammaSigmaR = ztwoOne

@[simp]

theorem GQ2.nuR_gammaTau : nuR gammaTauR = 1

@[simp]

theorem GQ2.nuR_gammaX0 : nuR gammaX0R = 1

@[simp]

theorem GQ2.nuR_gammaX1 : nuR gammaX1R = 1

theorem GQ2.nuR_surjective : Function.Surjective ⇑nuR

ν_R is a continuous epimorphism onto Z₂ (⟦lem:tame⟧, second half): ν_t is onto (nuT_surjective) and φ_R is onto (phiR_surjective).

Stress tests (plan rule 9)

Explicit generator evaluations pinning φ_R (tame generators to σ, τ, wild generators to 1) and ν_R (the unramified pattern (1, 0, 0, 0)).

theorem GQ2.phiR_generators : phiR gammaSigmaR = tameSigma ∧ phiR gammaTauR = tameTau ∧ phiR gammaX0R = 1 ∧ phiR gammaX1R = 1

Stress test. φ_R on the four explicit generators: σ, τ ↦ σ, τ, x₀, x₁ ↦ 1.

theorem GQ2.nuR_generators : nuR gammaSigmaR = ztwoOne ∧ nuR gammaTauR = 1 ∧ nuR gammaX0R = 1 ∧ nuR gammaX1R = 1

Stress test. ν_R realizes the unramified pattern ν_R(σ) = 1, ν_R(τ) = ν_R(x₀) = ν_R(x₁) = 0 (⟦lem:tame⟧).

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

• Lemma 2.1 = ⟦lem:tame⟧
• Definition 1.1 = ⟦def:GammaR⟧