The maximal pro-2 quotient of Γ_R is D_R (Roe note §3.1, Lemma 3.1 ⟦lem:pro2word⟧)

The Γ_R-half of the note's Lemma 3.1: the maximal pro-2 quotient of the Roe candidate group Γ_R = F₄ ⧸ N_R (GQ2/Roe/GammaR.lean) collapses to the three-generator one-relator pro-2 group D_R (GQ2/Roe/DRPresentation.lean), verbatim

\DR=
\angles{s,x,y\ \middle|\
r_2=(x^s)^{-1}x^{-3}y^2[y,y^s]=1}_{\mathrm{pro}\text{-}2},

matching the marked generators σ ↦ s = drS, τ ↦ 1, x₀ ↦ x = drX, x₁ ↦ y = drY. This is the Roe-candidate counterpart of GQ2.SectionThree.maxAEquiv (the Γ_A-side identification Γ_A(2) ≅ Π of Prop 3.10, GQ2/BoundaryConstruction.lean), and it is proved by the same architecture, one presentation over: forward via the maximal-pro-2 universal property fed by R-admissibility at every finite 2-group level of D_R, backward via D_R's own universal property drLiftHom (ticket R7), mutual inverse by density.

The word collapse (keystone)

The analytical heart is wildValueR_eq_drWord_of_powOmega2_id: in a 2-group (where ω₂ acts as the identity, powOmega2_eq_self_of_orderOf_two_pow), the finite Roe wild value r_R of a marking (σ, 1, x₀, x₁) with τ = 1 is exactly drWord σ x₀ x₁ — the two ω₂-powers of r_R (inside aR = (x₀⁻³τ)^{ω₂} and inside σ₂ = σ^{ω₂}) become the bare (x₀³)⁻¹ and σ, so

r_R = (x₀^σ)⁻¹ · (x₀³)⁻¹ · x₁² · [x₁, x₁^σ] = drWord σ x₀ x₁.

τ dies pro-2 (maxProPMk_gammaTauR) exactly as on the Γ_A side: the tame relation forces τ to odd order (Tame.tame_odd_order), which in a 2-group is trivial.

The two maps

• forward PhiMaxR : Γ_R(2) → D_R — the descent of the classifier σ,τ,x₀,x₁ ↦ s,1,x,y through the maximal-pro-2 quotient (Π is pro-2, and each finite 2-group level of D_R receives an R-admissible marking: NR_le_ker + the collapse + dr_relation);
• backward PsiMaxR : D_R → Γ_R(2) — drLiftHom at the images of σ, x₀, x₁ in Γ_R(2), whose relator obligation drWord_maxR_eq_one is the collapse + quotientMk_wildRelatorR_eq_one pushed into the pro-2 quotient (τ dead by maxProPMk_gammaTauR).

dr_hom_ext (R8) and topGen_maxR (from freeProfinite_topGen through the two quotient surjections) give the mutual-inverse extensionality; maxPro2Bridge bundles the result.

Consumers (R15/R32)

maxPro2Bridge and its generator-image lemmas maxPro2Bridge_gammaSigmaR/… are the pro-2 leg of the boundary bundle: R15's markedPro2_R (GQ2/Roe/MarkedPro2.lean) composes this bridge with the marked iso G_{ℚ₂}(2) ≅ Γ_R(2), and the unramified-marking compatibility ν_R = ν_{D_R} ∘ bridge is read off the generator images (nuR_gammaSigma/nuDR_drS and friends). No axiom, no B-Lab hypothesis: this half of Lemma 3.1 is unconditional (#print axioms = the standard three).

Profinite instances on the raw quotient Γ_R = F₄ ⧸ N_R

The bundled GammaR (GQ2/Roe/GammaR.lean) has instance-synthesis issues (R6 design note), so — matching R6's GQ2/Roe/Tame.lean — everything below uses the raw quotient F₄ ⧸ N_R. Its CompactSpace and IsTopologicalGroup instances are unconditional, but T2Space and TotallyDisconnectedSpace are guarded by [IsClosed N_R]; we discharge that once here (via NR_isClosed) so that maxProPQuotient 2 (F₄ ⧸ N_R) elaborates without a local haveI at every statement.

theorem GQ2.instT2SpaceQuotNR : T2Space (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

theorem GQ2.instTDSpaceQuotNR : TotallyDisconnectedSpace (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

The word collapse at τ = 1 in a 2-group (keystone)

theorem GQ2.powOmega2_id_of_isPGroup {Q : Type u_1} [Group Q] (hQ : IsPGroup 2 Q) (g : Q) : powOmega2 g = g

On a 2-group ω₂ acts as the identity: every element has 2-power order (IsPGroup.iff_orderOf), so powOmega2 g = g (powOmega2_eq_self_of_orderOf_two_pow). The elementwise face of "ω₂ ≡ 1 on the 2-part", specialised to a group all of whose elements are 2-primary.

theorem GQ2.wildValueR_eq_drWord_of_powOmega2_id {G : Type u_1} [Group G] (σ x₀ x₁ : G) (ho : ∀ (g : G), powOmega2 g = g) : { σ := σ, τ := 1, x₀ := x₀, x₁ := x₁ }.wildValueR = drWord σ x₀ x₁

The word collapse ⟦lem:pro2word⟧ (keystone). In a group where ω₂ acts as the identity (automatic in a 2-group, powOmega2_id_of_isPGroup), the finite Roe wild value r_R of the marking (σ, 1, x₀, x₁) with τ = 1 equals the pro-2 relator word drWord σ x₀ x₁: the ω₂-power in aR = (x₀⁻³τ)^{ω₂} collapses to (x₀³)⁻¹ (with τ = 1) and the ω₂-power in σ₂ = σ^{ω₂} collapses to σ, leaving

r_R = (x₀^σ)⁻¹ · (x₀³)⁻¹ · x₁² · [x₁, x₁^σ] = drWord σ x₀ x₁.

The Roe-candidate counterpart of GQ2.SectionThree.wildRelWord_eq (GQ2/BoundaryConstruction.lean).

Topological generation of D_R in discrete quotients

theorem GQ2.gen_DR_quotient {H : Type u_1} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] (f : ↑DR.toProfinite.toTop →* H) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.closure {f drS, f drX, f drY} = ⊤

In every discrete continuous quotient of D_R, the images of s, x, y generate — the pushforward of dr_topGen (R8). Roe counterpart of GQ2.SectionThree.gen_piBd_quotient.

The forward descent Γ_R → D_R

noncomputable def GQ2.drClassifier : FreeProfiniteGroup (Fin 4) ⟶ DR

The pro-2 classifier F₄ ⟶ D_R: σ ↦ s = drS, τ ↦ 1, x₀ ↦ x = drX, x₁ ↦ y = drY. Roe counterpart of GQ2.SectionThree.piClassifier.

Equations

• GQ2.drClassifier = (GQ2.FreeProfiniteGroup.homEquiv (Fin 4) GQ2.DR).symm ![GQ2.drS, 1, GQ2.drX, GQ2.drY]

theorem GQ2.isAdmissibleR_drClassifier_level (V : OpenNormalSubgroup ↑DR.toProfinite.toTop) : (Marking.map ((QuotientGroup.mk' ↑V.toOpenSubgroup).comp (ProfiniteGrp.Hom.hom drClassifier).toMonoidHom) univMarking).AdmissibleR

Through every finite 2-group level of D_R, the marking pushed from the pro-2 classifier is R-admissible: τ ↦ 1, the Roe wild value collapses to drWord, which vanishes by dr_relation, and generation / 2-core are automatic in the 2-group. Roe counterpart of GQ2.SectionThree.isAdmissible_piClassifier_level.

theorem GQ2.NR_le_ker_drClassifier : NR ≤ (ProfiniteGrp.Hom.hom drClassifier).ker

N_R is contained in the kernel of the pro-2 classifier (each finite level is R-admissible, isAdmissibleR_drClassifier_level, so NR_le_ker applies). Roe counterpart of GQ2.SectionThree.NA_le_ker_piClassifier.

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

The descent φ_{D_R} : Γ_R → D_R (σ ↦ s, τ ↦ 1, x₀ ↦ x, x₁ ↦ y). Roe counterpart of GQ2.SectionThree.phiP.

Equations

• GQ2.phiDR = GQ2.quotientLift GQ2.NR (ProfiniteGrp.Hom.hom GQ2.drClassifier) GQ2.NR_le_ker_drClassifier

@[simp]

theorem GQ2.phiDR_gammaSigmaR : phiDR gammaSigmaR = drS

@[simp]

theorem GQ2.phiDR_gammaTauR : phiDR gammaTauR = 1

@[simp]

theorem GQ2.phiDR_gammaX0R : phiDR gammaX0R = drX

@[simp]

theorem GQ2.phiDR_gammaX1R : phiDR gammaX1R = drY

noncomputable def GQ2.PhiMaxR : ↑(maxProPQuotient 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)).toProfinite.toTop →ₜ* ↑DR.toProfinite.toTop

The forward map Φ : Γ_R(2) → D_R, the descent of φ_{D_R} through the maximal pro-2 quotient (D_R is pro-2, so φ_{D_R} kills the pro-2 kernel). Roe counterpart of GQ2.SectionThree.PhiMax.

Equations

• GQ2.PhiMaxR = GQ2.quotientLift (GQ2.proPKernel 2 (↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ GQ2.NR)) GQ2.phiDR GQ2.PhiMaxR._proof_2

τ dies in the maximal pro-2 quotient of Γ_R

theorem GQ2.gammaMarkingR_tameRel : conjP gammaTauR gammaSigmaR = gammaTauR ^ 2

The marked tame relation holds in Γ_R: the tame relator dies in N_R (quotientMk_NR_tameRelator_eq_one). Roe counterpart of GQ2.SectionThree.gammaMarking_tameRel.

theorem GQ2.maxProPMk_gammaTauR : (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR = 1

τ dies in the maximal pro-2 quotient of Γ_R (⟦lem:pro2word⟧; ⟦lem:tame⟧ restricted to the pro-2 quotient): in every finite 2-group level the image of τ has both odd order (tame relation, Tame.tame_odd_order) and 2-power order, hence is trivial. Roe counterpart of GQ2.SectionThree.maxProPMk_gammaTau.

The backward relator kill and the backward descent D_R → Γ_R(2)

theorem GQ2.drWord_maxR_eq_one : drWord ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR) ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R) ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R) = 1

The pro-2 relator holds in Γ_R(2) ⟦lem:pro2word⟧: drWord vanishes at the images of σ, x₀, x₁. In every finite 2-group level the Roe wild relation holds (wildRelatorR dies in Γ_R, quotientMk_wildRelatorR_eq_one, transported by map_wildRelatorR) and τ ↦ 1 (maxProPMk_gammaTauR), so the collapse gives drWord = 1; separated by finite quotients, it vanishes in the limit. Roe counterpart of GQ2.SectionThree.piRelatorWord_maxA_eq_one; this is the relator obligation of the backward drLiftHom.

noncomputable def GQ2.PsiMaxR : ↑DR.toProfinite.toTop →ₜ* ↑(maxProPQuotient 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)).toProfinite.toTop

The backward map Ψ : D_R → Γ_R(2), via D_R's universal property drLiftHom (R7) at the images of σ, x₀, x₁ in the (pro-2) quotient Γ_R(2); the relator obligation is drWord_maxR_eq_one. Roe counterpart of GQ2.SectionThree.PsiMax.

Equations

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

Topological generation of Γ_R(2) and the two composites

theorem GQ2.topGen_maxR : (Subgroup.closure {(maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR, (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR, (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R, (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R}).topologicalClosure = ⊤

Γ_R(2) is topologically generated by the images of the four marked generators — the pushforward of freeProfinite_topGen (R8) through the two quotient surjections F₄ ↠ Γ_R ↠ Γ_R(2). Roe counterpart of GQ2.SectionThree.topGen_maxA.

theorem GQ2.PhiMaxR_PsiMaxR (x : ↑DR.toProfinite.toTop) : PhiMaxR (PsiMaxR x) = x

Φ ∘ Ψ = id on D_R (both fix s, x, y; dr_hom_ext).

theorem GQ2.PsiMaxR_PhiMaxR (x : ↑(maxProPQuotient 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)).toProfinite.toTop) : PsiMaxR (PhiMaxR x) = x

Ψ ∘ Φ = id on Γ_R(2) (checked on the four marked generator images; topGen_maxR, τ dead by maxProPMk_gammaTauR).

The marked isomorphism Γ_R(2) ≅ D_R (⟦lem:pro2word⟧, Γ_R half of Lemma 3.1)

noncomputable def GQ2.maxPro2Bridge : ↑(maxProPQuotient 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)).toProfinite.toTop ≃ₜ* ↑DR.toProfinite.toTop

The maximal pro-2 quotient of Γ_R is D_R ⟦lem:pro2word⟧ (the Γ_R half of the note's Lemma 3.1): a continuous isomorphism Γ_R(2) ≅ D_R matching the marked generators σ ↦ s, τ ↦ 1, x₀ ↦ x, x₁ ↦ y. Roe counterpart of GQ2.SectionThree.maxAEquiv; the pro-2 leg of the boundary bundle that R15's markedPro2_R and R32 consume.

Equations

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

Generator-image lemmas (the marked compatibility hooks R15/R32 consume)

@[simp]

theorem GQ2.maxPro2Bridge_gammaSigmaR : maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR) = drS

@[simp]

theorem GQ2.maxPro2Bridge_gammaTauR : maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR) = 1

@[simp]

theorem GQ2.maxPro2Bridge_gammaX0R : maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R) = drX

@[simp]

theorem GQ2.maxPro2Bridge_gammaX1R : maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R) = drY

@[simp]

theorem GQ2.maxPro2Bridge_symm_drS : maxPro2Bridge.symm drS = (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR

@[simp]

theorem GQ2.maxPro2Bridge_symm_drX : maxPro2Bridge.symm drX = (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R

@[simp]

theorem GQ2.maxPro2Bridge_symm_drY : maxPro2Bridge.symm drY = (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R

theorem GQ2.maxPro2Bridge_spec : ∃ (e : ↑(maxProPQuotient 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)).toProfinite.toTop ≃ₜ* ↑DR.toProfinite.toTop), e ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR) = drS ∧ e ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR) = 1 ∧ e ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R) = drX ∧ e ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R) = drY

The bridge with its marked generator images ⟦lem:pro2word⟧, in the existence shape of GQ2.SectionThree.prop_3_10_gammaA_proved — the interface R15/R32 consume for the pro-2 leg.

Stress lemmas (plan rule 9)

theorem GQ2.maxPro2Bridge_generators : maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaSigmaR) = drS ∧ maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR) = 1 ∧ maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX0R) = drX ∧ maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaX1R) = drY

Stress test (marked generator images). maxPro2Bridge realizes the marked pattern σ ↦ s, τ ↦ 1, x₀ ↦ x, x₁ ↦ y on the four generator images.

theorem GQ2.maxPro2Bridge_gammaTauR_eq_one : (maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) gammaTauR = 1 ∧ maxPro2Bridge 1 = 1

Stress test (τ-death, marked form). The class of τ in Γ_R(2) is trivial, so the bridge carries it to 1 ∈ D_R — the pro-2 face of "τ dies" (⟦lem:pro2word⟧).

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

• Lemma 3.1 = ⟦lem:pro2word⟧ (maxPro2Bridge, maxPro2Bridge_spec; the Γ_R half — maxPro2(Γ_R) = D_R — mirroring the Γ_A-side GQ2.SectionThree.maxAEquiv of Prop 3.10)
• eq. (3.1) = ⟦lem:pro2word⟧ (drWord-relator, via drWord_maxR_eq_one / dr_relation)
• Lemma 2.1 = ⟦lem:tame⟧ (maxProPMk_gammaTauR: τ dies pro-2)