Proposition 3.2 — proofs

Proves the §3 statements for the paper's Prop. 3.2 (common tame quotient) and the two ν-surjectivities of Prop. 3.14. The theorems are declared here, in the same GQ2.SectionThree namespace, because their proofs import the definition layer in GQ2/SectionThree.lean.

• Γ_A side (prop_3_2_gammaA, axiom-free): the classifier F₄ → T_tame (σ↦σ, τ↦τ, x₀,x₁↦1) kills N_A — through every finite level the pushed marking (σ̄, τ̄, 1, 1) is admissible, because τ̄ has odd order (Lemma 3.1, GQ2/Tame.lean), so ω₂ kills it and the whole eq. (1)–(3) word ledger collapses (u_i = d₀ = c₀ = d_g = h_c = h₀ = 1), making relation (6) trivially true — exactly the paper's proof. Descending and inverting via the presentation universal property gives the marked isomorphism Γ_A/W_A ≅ T_tame; the two composites are the identity by density of the marked generators.
• ν-surjectivities (nuT_surjective, nuTwo_surjective, axiom-free): the ranges are closed subgroups (continuous images of compact groups) containing ν(σ) = 1, and 1 topologically generates Z₂ (via ℤ dense in ℤ̂, the profinite-exponentiation API).
• Local side (prop_3_2_local, Ax = B10): the axiom GQ2.tameQuotient supplies the closed normal pro-2 W with G_{ℚ₂}/W ≅ T_tame; Lemma 3.3's maximality is proved — T_tame has no nontrivial "normal subgroup with 2-group finite images", by the paper's argument: through each Fermat-level quotient C_{2^{2^m}−1} ⋊ C_{2^m} (faithful squaring action, trivial center) the image is central hence trivial, so the Ẑ-coordinate of such a subgroup is infinitely 2-divisible; the inertia part then dies levelwise (odd ∧ 2-power).

Infrastructure (all axiom-free): topological generation of free profinite groups by their generators (also proved by the finite-generation proof's GQ2/FinitelyGenerated.lean in IsTopologicallyFinGen packaging; the overlap is one lemma deep and flagged for dedup), its transfer along continuous surjections and into finite quotients, and equality-on-topological-generators for continuous homomorphisms.

Topological generation: free profinite groups and their quotients

theorem GQ2.SectionThree.range_fin_two {α : Type u_1} (v : Fin 2 → α) : Set.range v = {v 0, v 1}

Set.range of a Fin 2-tuple is the unordered pair.

theorem GQ2.SectionThree.topGen_freeProfiniteGroup (X : Type) : (Subgroup.closure (Set.range FreeProfiniteGroup.of)).topologicalClosure = ⊤

The free profinite group is topologically generated by its generators (the discrete free group is dense in its profinite completion). Cf. the finite-generation proof's GQ2/FinitelyGenerated.lean for the same fact in IsTopologicallyFinGen packaging.

theorem GQ2.SectionThree.topGen_map {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) {S : Set G} (hS : (Subgroup.closure S).topologicalClosure = ⊤) : (Subgroup.closure (⇑f '' S)).topologicalClosure = ⊤

Topological generation transfers along a continuous surjective homomorphism.

theorem GQ2.SectionThree.gen_of_topGen_discrete {H : Type u_1} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] {S : Set H} (hS : (Subgroup.closure S).topologicalClosure = ⊤) : Subgroup.closure S = ⊤

In a discrete (e.g. finite) group, topological generation is plain generation.

theorem GQ2.SectionThree.monoidHom_eq_of_topGen {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [T2Space H] {f g : G →* H} (hf : Continuous ⇑f) (hg : Continuous ⇑g) {S : Set G} (hS : (Subgroup.closure S).topologicalClosure = ⊤) (h : ∀ x ∈ S, f x = g x) (x : G) : f x = g x

Two continuous homomorphisms agreeing on a topologically generating set agree everywhere.

Marked topological generation of T_tame and its finite levels

theorem GQ2.SectionThree.topGen_ttame : (Subgroup.closure {tameSigma, tameTau}).topologicalClosure = ⊤

T_tame is topologically generated by σ, τ.

theorem GQ2.SectionThree.gen_ttame_quotient {H : Type u_1} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] (f : ↑Ttame.toProfinite.toTop →* H) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Subgroup.closure {f tameSigma, f tameTau} = ⊤

In every discrete continuous quotient of T_tame, the images of σ, τ generate.

The word-ledger collapse

Paper, proofs of Prop. 3.2 / Prop. 3.10: at a marking with trivial wild letters and odd-order τ, the ω₂-exponent kills τ-words and the auxiliary words (1)–(3) all collapse to 1, so relation (6) holds trivially.

theorem GQ2.SectionThree.powOmega2_eq_one_of_odd {G : Type u_1} [Group G] {x : G} (hx : Odd (orderOf x)) : powOmega2 x = 1

x^{ω₂} = 1 for an element of odd order (the 2-primary part of an odd-order element).

The Γ_A side: the classifier and its levels

noncomputable def GQ2.SectionThree.tameClassifier : FreeProfiniteGroup (Fin 4) ⟶ Ttame

The classifier F₄ ⟶ T_tame: σ ↦ σ, τ ↦ τ, x₀ ↦ 1, x₁ ↦ 1.

Equations

• GQ2.SectionThree.tameClassifier = (GQ2.FreeProfiniteGroup.homEquiv (Fin 4) GQ2.Ttame).symm ![GQ2.tameSigma, GQ2.tameTau, 1, 1]

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

Through every open normal level of T_tame, the marking pushed from the classifier is admissible: τ̄ has odd order (Lemma 3.1), so the ledger collapses.

The descent Γ_A → T_tame and its inverse

theorem GQ2.SectionThree.tameRelator_mem_NA' : univMarking.tameRelator ∈ NA

The tame relator of the universal marking lies in N_A (it dies in every admissible quotient — relation (5) is part of admissibility). Also proved by the admissible-limit proof's GQ2/AdmissibleLimit.lean; kept inline for import hygiene, flagged for dedup.

theorem GQ2.SectionThree.NA_le_ker_tameClassifier : NA ≤ (ProfiniteGrp.Hom.hom tameClassifier).ker

N_A is contained in the kernel of the classifier F₄ → T_tame (each of its finite levels is an admissible quotient, by isAdmissible_tameClassifier_level).

noncomputable def GQ2.SectionThree.wildPartB : Subgroup ↑GammaA.toProfinite.toTop

The ↥Γ_A-spelled copy of wildPart (definitionally equal; the admissible-limit layer spells wildPart at the raw quotient F₄ ⧸ N_A, but this file's constructions all run at the bundled-carrier spelling ↥Γ_A, where the ProfiniteGrp instance path applies uniformly).

Equations

• GQ2.SectionThree.wildPartB = GQ2.SectionThree.wildPart

instance GQ2.SectionThree.wildPartB_normal : wildPartB.Normal

theorem GQ2.SectionThree.wildPartB_eq_closure : wildPartB = (Subgroup.normalClosure {gammaX0, gammaX1}).topologicalClosure

noncomputable def GQ2.SectionThree.phiA : ↑GammaA.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop

The descent φ_A : Γ_A → T_tame of the classifier (σ↦σ, τ↦τ, x₀,x₁↦1).

Equations

• GQ2.SectionThree.phiA = GQ2.quotientLift GQ2.NA (ProfiniteGrp.Hom.hom GQ2.SectionThree.tameClassifier) GQ2.SectionThree.NA_le_ker_tameClassifier

@[simp]

theorem GQ2.SectionThree.phiA_gammaSigma : phiA gammaSigma = tameSigma

@[simp]

theorem GQ2.SectionThree.phiA_gammaTau : phiA gammaTau = tameTau

@[simp]

theorem GQ2.SectionThree.phiA_gammaX0 : phiA gammaX0 = 1

@[simp]

theorem GQ2.SectionThree.phiA_gammaX1 : phiA gammaX1 = 1

theorem GQ2.SectionThree.wildPartB_le_ker_phiA : wildPartB ≤ phiA.ker

W_A ≤ ker φ_A (the wild generators map to 1, and the kernel is closed normal).

noncomputable def GQ2.SectionThree.psiW : ↑GammaA.toProfinite.toTop ⧸ wildPartB →ₜ* ↑Ttame.toProfinite.toTop

ψ : Γ_A/W_A → T_tame, the descent of φ_A.

Equations

• GQ2.SectionThree.psiW = GQ2.quotientLift GQ2.SectionThree.wildPartB GQ2.SectionThree.phiA GQ2.SectionThree.wildPartB_le_ker_phiA

noncomputable def GQ2.SectionThree.TameA : ProfiniteGrp.{0}

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

Equations

• GQ2.SectionThree.TameA = GQ2.profiniteQuotient GQ2.SectionThree.wildPartB

noncomputable def GQ2.SectionThree.chiBase : FreeProfiniteGroup (Fin 2) ⟶ TameA

The base map F₂ ⟶ Γ_A/W_A: σ ↦ σ̄, τ ↦ τ̄.

Equations

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

theorem GQ2.SectionThree.chiBase_tameWord : (ProfiniteGrp.Hom.hom chiBase).toMonoidHom tameWord = 1

The base map kills the tame relator: its image is the W_A-class of the Γ_A-image of univMarking.tameRelator ∈ N_A.

noncomputable def GQ2.SectionThree.chiW : ↑Ttame.toProfinite.toTop →ₜ* ↑TameA.toProfinite.toTop

χ : T_tame → Γ_A/W_A, by the universal property of the presentation.

Equations

• GQ2.SectionThree.chiW = GQ2.presentationLift {GQ2.tameWord} (ProfiniteGrp.Hom.hom GQ2.SectionThree.chiBase) ⋯

theorem GQ2.SectionThree.topGen_tameA : (Subgroup.closure (Set.range fun (i : Fin 4) => (quotientMk wildPartB) ((quotientMk NA) (FreeProfiniteGroup.of i)))).topologicalClosure = ⊤

Γ_A/W_A is topologically generated by the classes of the four marked generators.

theorem GQ2.SectionThree.psiW_chiW (x : ↑Ttame.toProfinite.toTop) : psiW (chiW x) = x

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

theorem GQ2.SectionThree.chiW_psiW (x : ↑GammaA.toProfinite.toTop ⧸ wildPartB) : chiW (psiW x) = x

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

noncomputable def GQ2.SectionThree.tameAEquiv : ↑GammaA.toProfinite.toTop ⧸ wildPartB ≃ₜ* ↑Ttame.toProfinite.toTop

The marked isomorphism Γ_A/W_A ≅ T_tame (Prop. 3.2, Γ_A side).

Equations

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

theorem GQ2.SectionThree.prop_3_2_gammaA : ∃ (e : ↑GammaA.toProfinite.toTop ⧸ wildPart ≃ₜ* ↑Ttame.toProfinite.toTop), e ↑gammaSigma = tameSigma ∧ e ↑gammaTau = tameTau

Prop. 3.2, Γ_A side: the quotient of Γ_A by W_A is T_tame, matching the marked generators.

The ν-surjectivities of Prop. 3.14

theorem GQ2.SectionThree.topGen_zhat : (Subgroup.closure {Zhat.ofInt 1}).topologicalClosure = ⊤

ℤ̂ is topologically generated by 1.

theorem GQ2.SectionThree.topGen_ztwo : (Subgroup.closure {ztwoOne}).topologicalClosure = ⊤

Z₂ is topologically generated by ztwoOne.

theorem GQ2.SectionThree.surjective_of_mem_range_topGen {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [CompactSpace G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H] (f : G →ₜ* H) {x : H} (hgen : (Subgroup.closure {x}).topologicalClosure = ⊤) (hx : x ∈ Set.range ⇑f) : Function.Surjective ⇑f

A continuous homomorphism from a compact group hitting a topological generator of a T2 target is surjective.

theorem GQ2.SectionThree.nuT_surjective : Function.Surjective ⇑GQ2.nuT

ν_t : T_tame ↠ Z₂ is surjective (Prop. 3.14's arrow). nuT is qualified GQ2.nuT (the BoundaryFrame Ttame → Z₂ map) to disambiguate from the later SectionThree.nuT (the ν_ur descent through (G_ℚ₂(2))^ab, a different map) which otherwise shadows it in this namespace.

theorem GQ2.SectionThree.nuTwo_surjective : Function.Surjective ⇑nuTwo

ν₂ : Π ↠ Z₂ is surjective (eq. (21)'s arrow).

Pro-2 subgroups have 2-group finite images

theorem GQ2.SectionThree.isPGroup_map_of_isProP {P : Type u_1} [Group P] [TopologicalSpace P] {N : Subgroup P} (hN : IsProP 2 ↥N) {G : Type u_2} [Group G] [TopologicalSpace G] [DiscreteTopology G] (f : P →* G) (hf : Continuous ⇑f) : IsPGroup 2 ↥(Subgroup.map f N)

A closed-subgroup-free transfer: if N ≤ P is pro-2 (as a topological group) then its image under any continuous homomorphism to a finite discrete group is a 2-group.

The inertia quotient Q = T_tame / ⟨⟨τ⟩⟩

noncomputable def GQ2.SectionThree.inertiaPart : Subgroup ↑Ttame.toProfinite.toTop

The closed normal closure of τ in T_tame — the (pro-odd) tame inertia.

Equations

• GQ2.SectionThree.inertiaPart = (Subgroup.normalClosure {GQ2.tameTau}).topologicalClosure

instance GQ2.SectionThree.inertiaPart_normal : inertiaPart.Normal

noncomputable def GQ2.SectionThree.Qur : ProfiniteGrp.{0}

Q = T_tame / ⟨⟨τ⟩⟩, the procyclic unramified quotient.

Equations

• GQ2.SectionThree.Qur = GQ2.profiniteQuotient GQ2.SectionThree.inertiaPart

noncomputable def GQ2.SectionThree.qMk : ↑Ttame.toProfinite.toTop →ₜ* ↑Qur.toProfinite.toTop

The projection T_tame → Q, typed at the bundled carrier.

Equations

• GQ2.SectionThree.qMk = GQ2.quotientMk GQ2.SectionThree.inertiaPart

noncomputable def GQ2.SectionThree.qSigma : ↑Qur.toProfinite.toTop

The image of σ in Q.

Equations

• GQ2.SectionThree.qSigma = (GQ2.quotientMk GQ2.SectionThree.inertiaPart) GQ2.tameSigma

theorem GQ2.SectionThree.closure_pair_one {G : Type u_1} [Group G] (a : G) : Subgroup.closure {a, 1} = Subgroup.closure {a}

closure {a, 1} = closure {a}.

theorem GQ2.SectionThree.topGen_qur : (Subgroup.closure {qSigma}).topologicalClosure = ⊤

Q is topologically generated by σ.

The Fermat levels G_m = C_{2^{2^m}−1} ⋊ C_{2^m}

The paper's proof of Lemma 3.3: the finite quotients of T_tame in which geometric Frobenius has order exactly 2^m on inertia of order e_m = 2^{2^m} − 1 (the squaring action is faithful, since the order of 2 mod e_m is exactly 2^m). Their centers are trivial, so normal 2-subgroups die; this pins the Ẑ-coordinate of a pro-2 normal subgroup to be divisible by every 2^m.

def GQ2.SectionThree.emN (m : ℕ) : ℕ

e_m = 2^{2^m} − 1.

Equations

• GQ2.SectionThree.emN m = 2 ^ 2 ^ m - 1

instance GQ2.SectionThree.instNeZeroNatEmN (m : ℕ) : NeZero (emN m)

theorem GQ2.SectionThree.coprime_two_emN (m : ℕ) : Nat.Coprime 2 (emN m)

noncomputable def GQ2.SectionThree.u2 (m : ℕ) : (ZMod (emN m))ˣ

The unit 2 ∈ (ℤ/e_m)ˣ.

Equations

• GQ2.SectionThree.u2 m = ZMod.unitOfCoprime 2 ⋯

theorem GQ2.SectionThree.u2_pow_eq_one_iff (m : ℕ) {j : ℕ} (hj : j < 2 ^ m) (h : u2 m ^ j = 1) : j = 0

The order of 2 mod e_m is exactly 2^m, in the only form needed: no smaller power of the unit 2 is 1.

def GQ2.SectionThree.unitsMulAut (e : ℕ) : (ZMod e)ˣ →* MulAut (Multiplicative (ZMod e))

Units of ZMod e, acting as automorphisms of the multiplicative cyclic group of order e (the vehicle for the squaring action of Frobenius on inertia).

Equations

• GQ2.SectionThree.unitsMulAut e = { toFun := fun (u : (ZMod e)ˣ) => AddEquiv.toMultiplicative (DistribMulAction.toAddEquiv (ZMod e) u), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def GQ2.SectionThree.uChar (m : ℕ) : Multiplicative (ZMod (2 ^ m)) →* (ZMod (emN m))ˣ

The character C_{2^m} → (ℤ/e_m)ˣ sending the generator to 2⁻¹ (the inverse squaring, so that s⁻¹ t s = t² holds with the paper's conjugation convention).

Equations

• GQ2.SectionThree.uChar m = { toFun := fun (h : Multiplicative (ZMod (2 ^ m))) => (GQ2.SectionThree.u2 m)⁻¹ ^ (Multiplicative.toAdd h).val, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def GQ2.SectionThree.phiFermat (m : ℕ) : Multiplicative (ZMod (2 ^ m)) →* MulAut (Multiplicative (ZMod (emN m)))

The Frobenius action φ_m : C_{2^m} → Aut(C_{e_m}).

Equations

• GQ2.SectionThree.phiFermat m = (GQ2.SectionThree.unitsMulAut (GQ2.SectionThree.emN m)).comp (GQ2.SectionThree.uChar m)

@[reducible, inline]

noncomputable abbrev GQ2.SectionThree.GFermat (m : ℕ) : Type

The Fermat level G_m = C_{e_m} ⋊ C_{2^m} with (inverse-)squaring action. (An abbrev, so all SemidirectProduct instances apply without wrapper friction.)

Equations

• GQ2.SectionThree.GFermat m = (Multiplicative (ZMod (GQ2.SectionThree.emN m)) ⋊[GQ2.SectionThree.phiFermat m] Multiplicative (ZMod (2 ^ m)))

@[implicit_reducible]

instance GQ2.SectionThree.instTopGFermat (m : ℕ) : TopologicalSpace (GFermat m)

Equations

• GQ2.SectionThree.instTopGFermat m = ⊥

instance GQ2.SectionThree.instDiscGFermat (m : ℕ) : DiscreteTopology (GFermat m)

instance GQ2.SectionThree.instFiniteGFermat (m : ℕ) : Finite (GFermat m)

noncomputable def GQ2.SectionThree.sFermat (m : ℕ) : GFermat m

s ∈ G_m: the Frobenius generator.

Equations

• GQ2.SectionThree.sFermat m = SemidirectProduct.inr (Multiplicative.ofAdd 1)

noncomputable def GQ2.SectionThree.tFermat (m : ℕ) : GFermat m

t ∈ G_m: the inertia generator.

Equations

• GQ2.SectionThree.tFermat m = SemidirectProduct.inl (Multiplicative.ofAdd 1)

theorem GQ2.SectionThree.fermat_relation (m : ℕ) : (sFermat m)⁻¹ * tFermat m * sFermat m = tFermat m ^ 2

The tame relation holds in G_m: s⁻¹ t s = t².

theorem GQ2.SectionThree.fermat_gen (m : ℕ) : Subgroup.closure {sFermat m, tFermat m} = ⊤

G_m is generated by s, t.

theorem GQ2.SectionThree.fermat_central_eq_one (m : ℕ) {z : GFermat m} (hz : z ∈ Subgroup.center (GFermat m)) : z = 1

The center of G_m is trivial (the action is faithful and fixed-point-free on the generator).

theorem GQ2.SectionThree.fermat_relator (m : ℕ) : conjP (tFermat m) (sFermat m) * (tFermat m ^ 2)⁻¹ = 1

The tame relator dies in G_m (product form, for the presentation lift).

noncomputable def GQ2.SectionThree.fermatBase (m : ℕ) : FreeProfiniteGroup (Fin 2) ⟶ ProfiniteGrp.of (GFermat m)

The classifying map F₂ ⟶ G_m (σ ↦ s, τ ↦ t).

Equations

• GQ2.SectionThree.fermatBase m = (GQ2.FreeProfiniteGroup.homEquiv (Fin 2) (ProfiniteGrp.of (GQ2.SectionThree.GFermat m))).symm ![GQ2.SectionThree.sFermat m, GQ2.SectionThree.tFermat m]

noncomputable def GQ2.SectionThree.fermatHom (m : ℕ) : ↑Ttame.toProfinite.toTop →ₜ* GFermat m

The marked map T_tame → G_m (σ ↦ s, τ ↦ t).

Equations

• GQ2.SectionThree.fermatHom m = GQ2.presentationLift {GQ2.tameWord} (ProfiniteGrp.Hom.hom (GQ2.SectionThree.fermatBase m)) ⋯

theorem GQ2.SectionThree.fermatHom_eq_one_of_mem (m : ℕ) {M : Subgroup ↑Ttame.toProfinite.toTop} [hMn : M.Normal] (h2 : ∀ (G : Type) [inst : Group G] [inst_1 : TopologicalSpace G] [DiscreteTopology G] [Finite G] (f : ↑Ttame.toProfinite.toTop →* G), Continuous ⇑f → IsPGroup 2 ↥(Subgroup.map f M)) {x : ↑Ttame.toProfinite.toTop} (hx : x ∈ M) : (fermatHom m) x = 1

Elements of a normal subgroup with 2-group finite images die in every Fermat level (the image is a central 2-subgroup of a center-free group).

theorem GQ2.SectionThree.multiplicative_zmod_pow (n : ℕ) [NeZero n] (x : Multiplicative (ZMod n)) : x = Multiplicative.ofAdd 1 ^ (Multiplicative.toAdd x).val

Every element of Multiplicative (ℤ/n) is a power of ofAdd 1.

noncomputable def GQ2.SectionThree.fermatNu (m : ℕ) : ↑Ttame.toProfinite.toTop →ₜ* Multiplicative (ZMod (2 ^ m))

The unramified coordinate at level m: ν_m = rightHom ∘ (T_tame → G_m).

Equations

• GQ2.SectionThree.fermatNu m = { toMonoidHom := SemidirectProduct.rightHom.comp (GQ2.SectionThree.fermatHom m).toMonoidHom, continuous_toFun := ⋯ }

noncomputable def GQ2.SectionThree.psiFermatQ (m : ℕ) : ↑Qur.toProfinite.toTop →ₜ* Multiplicative (ZMod (2 ^ m))

The level maps ψ_m : Q → C_{2^m} descend from ν_m.

Equations

• GQ2.SectionThree.psiFermatQ m = GQ2.quotientLift GQ2.SectionThree.inertiaPart (GQ2.SectionThree.fermatNu m) ⋯

Cyclic-group torsion helper

theorem GQ2.SectionThree.mem_of_orderOf_dvd_card {C : Type u_1} [Group C] [IsCyclic C] [Finite C] {K : Subgroup C} {x : C} (hdvd : orderOf x ∣ Nat.card ↥K) : x ∈ K

In a finite cyclic group, an element whose order divides #K lies in K (the subgroup of order #K is exactly the #K-torsion, by the cyclic root-count bound).

theorem GQ2.SectionThree.tame_rel_map {H : Type u_1} [Group H] (f : ↑Ttame.toProfinite.toTop →* H) : (f tameSigma)⁻¹ * f tameTau * f tameSigma = f tameTau ^ 2

The tame relation through any homomorphism out of T_tame.

Lemma 3.3, core form

theorem GQ2.SectionThree.eq_bot_of_normal_two_images (M : Subgroup ↑Ttame.toProfinite.toTop) [hMn : M.Normal] (h2 : ∀ (G : Type) [inst : Group G] [inst_1 : TopologicalSpace G] [DiscreteTopology G] [Finite G] (f : ↑Ttame.toProfinite.toTop →* G), Continuous ⇑f → IsPGroup 2 ↥(Subgroup.map f M)) : M = ⊥

Lemma 3.3 (core): a normal subgroup of T_tame all of whose finite continuous images are 2-groups is trivial. Paper argument: through each Fermat level G_m the image is a central 2-subgroup of a center-free group, hence trivial, so the Q-coordinate dies in every C_{2^m}; the cyclic level-comparison then kills the Q-image entirely, and the remaining inertia part has both odd and 2-power order levelwise.

Proposition 3.2, local side

theorem GQ2.SectionThree.tameData_maximal [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (T' : TameQuotientData) (N : Subgroup AbsGalQ2) : N.Normal → IsClosed ↑N → IsProP 2 ↥N → N ≤ T'.W

Lemma 3.3's maximality, for any B10 datum (extracted from prop_3_2_local's proof so the marked pro-2 isomorphisms oriented witness can reuse it): every closed normal pro-2 subgroup lies in T.W (eq_bot_of_normal_two_images applied to the image of the competitor N in T_tame).

theorem GQ2.SectionThree.prop_3_2_local [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : Nonempty LocalTameQuotient

Prop. 3.2, local side (Ax = B10): the tame quotient of G_{ℚ₂} is T_tame, by the maximal closed normal pro-2 subgroup. Existence is axiom B10 (oriented form B10′ since the marked pro-2 isomorphisms; only the underlying TameQuotientData is used here); maximality is Lemma 3.3 (tameData_maximal).

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

• eq. (1) = ⟦eq-defwords⟧
• eq. (21) = ⟦eq-nu2⟧
• eq. (3) = ⟦eq-defwords3⟧
• Lemma 3.1 = ⟦lem-tamefinite⟧
• Lemma 3.3 = ⟦lem-o2tame⟧
• Prop 3.10 = ⟦prop-pro2⟧
• Prop 3.14 = ⟦prop-compatiblemarking⟧
• Prop 3.2 = ⟦prop-tamequotient⟧