Γ_A and the literal Theorem 1.2

The paper's candidate group, exactly as defined in §2.1, eq. (7) (the marked quotient construction): let F₄ be the free profinite group on σ, τ, x₀, x₁; call a finite quotient φ : F₄ ⟶ G admissible if the pushed marking generates G, satisfies the relations (5) τ^σ = τ² and (6) h₀u₁⁻¹x₁^σc₀ = 1, and the normal closure of the images of x₀, x₁ is a 2-group; then

N_A = ⋂ {ker φ | φ admissible}, Γ_A = F₄ ⧸ N_A.

Note the pro-2 condition on the wild part is part of the presentation data — Γ_A is not the bare two-relator profinite presentation. Since kernels of continuous homs to finite discrete groups are exactly the open normal subgroups, N_A is faithfully encoded as the intersection of all admissible open normal subgroups (GQ2.NA); NA_le_ker certifies that every admissible quotient in the paper's sense (arbitrary finite target) contains N_A in its kernel.

This file also provides the relations (5)/(6) in their profinite reading: the auxiliary words of eqs. (1)–(3) with genuine ω₂ ∈ ℤ̂ exponents (Marking.sigma2Hat, …, Marking.wildRelator, via ^ᶻ omega2 from GQ2/Zhat.lean). The bridge lemmas map_tameRelator_eq_one_iff / map_wildRelator_eq_one_iff prove that killing these profinite words in a finite quotient is the same as the finite-level relations of GQ2/Words.lean (via the profinite-exponentiation API headline map_zpowHat_omega2) — so the two readings of Theorem 1.2's relations provably agree, and the admissibility used in N_A is exactly the paper's.

Finally, Theorem 1.2 in its literal form (main_presentation_literal, Γ_A ≅ G_{ℚ₂} as topological groups) is stated against this honest Γ_A and proved in GQ2/PresentationLiteral.lean (the literal-presentation proof), via Prop. 2.3 + the surjection-count theorem (see docs/orchestration/formalization-plan.md).

The auxiliary words with genuine profinite ω₂-exponents (eqs. (1)–(3), profinitely)

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

σ₂ = σ^{ω₂} (eq. (1)), with the genuine profinite exponent ω₂ ∈ ℤ̂.

Equations

• t.sigma2Hat = GQ2.zpowHat t.σ GQ2.omega2

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

u(ξ) = (ξτ)^{ω₂} (eq. (1)).

Equations

• t.uHat xi = GQ2.zpowHat (xi * t.τ) GQ2.omega2

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

u₀ = (x₀τ)^{ω₂}.

Equations

• t.u0Hat = t.uHat t.x₀

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

u₁ = (x₁τ)^{ω₂}.

Equations

• t.u1Hat = t.uHat t.x₁

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

d₀ = u₀x₀⁻¹ (eq. (1)).

Equations

• t.d0Hat = t.u0Hat * t.x₀⁻¹

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

z₀ = x₀^{σ₂} (eq. (2)).

Equations

• t.z0Hat = GQ2.conjP t.x₀ t.sigma2Hat

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

c₀ = [d₀, z₀] (eq. (2)).

Equations

• t.c0Hat = GQ2.commP t.d0Hat t.z0Hat

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

g₀ = σ₂² (eq. (2)).

Equations

• t.g0Hat = t.sigma2Hat ^ 2

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

d_g = d₀^{g₀} (eq. (2)).

Equations

• t.dgHat = GQ2.conjP t.d0Hat t.g0Hat

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

h_c = [d_g, d₀] (eq. (3)).

Equations

• t.hcHat = GQ2.commP t.dgHat t.d0Hat

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

h₀ = x₀^{g₀} · x₀ · d_g · d₀ · d₀² · h_c (eq. (3); note the bare d₀, cf. docs/erratum-h0-transcription.md).

Equations

• t.h0Hat = GQ2.conjP t.x₀ t.g0Hat * t.x₀ * t.dgHat * t.d0Hat * t.d0Hat ^ 2 * t.hcHat

def GQ2.Marking.tameRelator {G : Type} [Group G] (t : Marking G) : G

The tame relator τ^σ · (τ²)⁻¹ — relation (5) as a word.

Equations

• t.tameRelator = GQ2.conjP t.τ t.σ * (t.τ ^ 2)⁻¹

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

The wild relator h₀ · u₁⁻¹ · x₁^σ · c₀ — relation (6) as a word (its letters use the profinite ω₂-exponents above).

Equations

• t.wildRelator = t.h0Hat * t.u1Hat⁻¹ * GQ2.conjP t.x₁ t.σ * t.c0Hat

Faithfulness bridge: the profinite words evaluate to the finite words

Through any continuous homomorphism to a finite group, the ^ᶻ omega2-ledger computes the powOmega2-ledger of GQ2/Words.lean (the profinite-exponentiation API headline map_zpowHat_omega2, pushed through the whole word ledger). In particular relations (5)/(6) read profinitely (relator dies) and finitely (TameRel/WildRel of the pushed marking) are the same condition.

theorem GQ2.Marking.map_tameRelator_eq_one_iff {G : Type} [Group G] [TopologicalSpace G] {P : Type} [Group P] [TopologicalSpace P] (f : G →ₜ* P) (t : Marking G) : f.toMonoidHom t.tameRelator = 1 ↔ (map f.toMonoidHom t).TameRel

Relation (5), profinite = finite: the tame relator dies in a finite quotient iff the pushed marking satisfies the tame relation of GQ2/Words.lean. (No ω₂ occurs in (5), so no topology is needed.)

theorem GQ2.Marking.map_wildRelator_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.wildRelator = 1 ↔ (map f.toMonoidHom t).WildRel

Relation (6), profinite = finite: the wild relator dies in a finite quotient iff the pushed marking satisfies the wild relation of GQ2/Words.lean.

The universal marking and the homs it classifies

noncomputable def GQ2.Marking.toHom {P : ProfiniteGrp.{0}} (t : Marking ↑P.toProfinite.toTop) : FreeProfiniteGroup (Fin 4) ⟶ P

The continuous homomorphism F₄ ⟶ P classified by a marking of a profinite group P (the universal property of the free profinite group, inverted).

Equations

• t.toHom = (GQ2.FreeProfiniteGroup.homEquiv (Fin 4) P).symm ![t.σ, t.τ, t.x₀, t.x₁]

noncomputable def GQ2.univMarking : Marking ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop

The universal marking: the four generators of the free profinite group on four letters, in the paper's order σ, τ, x₀, x₁.

Equations

• GQ2.univMarking = { σ := GQ2.FreeProfiniteGroup.of 0, τ := GQ2.FreeProfiniteGroup.of 1, x₀ := GQ2.FreeProfiniteGroup.of 2, x₁ := GQ2.FreeProfiniteGroup.of 3 }

@[simp]

theorem GQ2.univMarking_map_toHom {P : ProfiniteGrp.{0}} (t : Marking ↑P.toProfinite.toTop) : Marking.map (ProfiniteGrp.Hom.hom t.toHom).toMonoidHom univMarking = t

Pushing the universal marking through the hom classified by t recovers t — the universal property really is "evaluate at the generators".

theorem GQ2.surjective_of_map_generates {P : Type u_1} [Group P] (f : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →* P) (hgen : (Marking.map f univMarking).Generates) : Function.Surjective ⇑f

A marking whose pushforward of the universal marking generates classifies a surjective hom (the image contains a generating set).

N_A and Γ_A (paper §2.1, eq. (7))

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

An open normal subgroup U ≤ F₄ is admissible (paper §2.1) if the canonical finite quotient F₄ ⧸ U carries an admissible pushed marking: the images of σ, τ, x₀, x₁ generate, satisfy relations (5) and (6) — equivalently (by map_tameRelator_eq_one_iff / map_wildRelator_eq_one_iff) the profinite relator words die — and the normal closure of the images of x₀, x₁ is a 2-group. Open normal subgroups are exactly the kernels of continuous homs to finite discrete groups, so this encodes the paper's class Q_A of admissible finite quotients (see NA_le_ker for the certificate).

Equations

• GQ2.IsAdmissibleU U = (GQ2.Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) GQ2.univMarking).Admissible

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

N_A (paper eq. (7)): the intersection of the kernels of all admissible finite quotients of F₄, encoded as the intersection of all admissible open normal subgroups.

Equations

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

instance GQ2.NA_normal : NA.Normal

theorem GQ2.NA_isClosed : IsClosed ↑NA

noncomputable def GQ2.GammaA : ProfiniteGrp.{0}

Γ_A (paper §2.1, eq. (7)): the marked quotient F₄ ⧸ N_A — the profinite group "topologically generated by σ, τ, x₀, x₁, with the closed normal subgroup generated by x₀, x₁ pro-2, subject to relations (5) and (6)" of Theorem 1.2, constructed exactly as in the paper as the largest quotient of F₄ all of whose finite quotients are admissible.

Equations

• GQ2.GammaA = GQ2.profiniteQuotient GQ2.NA

theorem GQ2.NA_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).Admissible) : NA ≤ f.ker

N_A is the paper's intersection (eq. (7)): the kernel of every admissible continuous hom to a finite (discrete) group — not just the canonical quotients F₄ ⧸ U — contains N_A. (The pushed marking being admissible forces f surjective, and admissibility transfers to the canonical quotient by the induced isomorphism F₄ ⧸ ker f ≃* P.)

Theorem 1.2, literal form

Theorem 1.2 (literal presentation form) — Γ_A ≅ G_{ℚ₂} as topological groups, with Γ_A the honest marked-quotient profinite group of paper eq. (7) defined above — is GQ2.main_presentation_literal, proved in GQ2/PresentationLiteral.lean (the literal-presentation proof), not here: its proof instantiates Statement.main_presentation at Γ_A with hΓA := prop_2_3 (Prop. 2.3, the Γ_A admissible-marking count) and hcount := SectionTen.main_surjection_count' (Theorem 1.2 count form for G_{ℚ₂}, eq. (154) + Prop 2.3) plus the two topological finite-generation witnesses — and prop_2_3/main_surjection_count' are downstream of this upstream file, so an in-place proof would create an import cycle. Its trust base is std-3 plus the nine census axioms of GQ2/Foundations/Axioms.lean.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (1) = ⟦eq-defwords⟧
• eq. (154) = ⟦eq-app-cup-convention⟧ [≥ drift window; verify against v428 tex]
• eq. (2) = ⟦eq-defwords2⟧
• eq. (3) = ⟦eq-defwords3⟧
• eq. (7) = ⟦eq-candidateinverse⟧
• Prop 2.3 = ⟦prop-epi-semantics⟧
• Theorem 1.2 = ⟦thm-main⟧