Labute's classification of G_{ℚ₂}(2) — the one irreducible local input

(Stage: Local)

This file isolates the single genuinely external, local-class-field-theoretic input of the entire Q₂ development as one clearly named, auditable axiom. Every other ingredient of the marked dyadic Demushkin normalization (Q2Presentation.Q2_marked_Demushkin) is proved from this axiom sorry-free.

The mathematical statement

labute_GQ2_maxPro2_marked asserts the fully marked comparison (MarkedLabuteIso): an isomorphism of profinite groups

MaximalPro2Quotient GQ2Profinite ≅ D0,

i.e. the maximal pro-2 quotient G_{ℚ₂}(2) of the absolute Galois group of ℚ₂ is the standard rank-three dyadic Demushkin group D₀ = ⟨a, s, y ∣ a² s⁴ [s,y] = 1⟩_{pro-2} (the object D0 of Boundary/D0.lean), together with a local unramified character nu_ur_loc and the compatibility nu_ur_loc = iso.hom ≫ nu_ur intertwining it with the D₀-model character — the full ℤ₂ marking the manuscript's boundary gluing requires (see "Scope" below).

This is Labute's classification of Demushkin groups (J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Theorem 8), specialized to the local field ℚ₂:

• a local field K ⊇ ℚ_p containing μ_p has G_K(p) a Demushkin group of rank [K:ℚ_p] + 2; for K = ℚ₂, p = 2 (and μ₂ = {±1} ⊆ ℚ₂) the rank is 1 + 2 = 3, with Demushkin invariant q = 2 and secondary exponent 2^f = 4, giving exactly the relator a² s⁴ [s,y] of D₀;
• see reference/q2_manuscript.tex, Lemma lem:standardorientation (l.509–534) and the abstract isomorphism f : D_loc ⟶ D₀ invoked at the start of the proof of Prop markedDem (l.917–955); the manuscript itself attributes this step to "Labute's classification, local reciprocity, and a lifting theorem for automorphisms of its abelianization" (l.128–132).

Why this is an irreducible gap (not provable in mathlib v4.28.0)

mathlib v4.28.0 contains none of the prerequisites for an internal proof:

• no theory of Demushkin / pro-p duality groups, nor Labute's classification (lean_loogle/lean_leansearch for Demushkin, Labute, "local field Galois group structure" find nothing);
• no local class field theory at the level needed (the local reciprocity isomorphism ℚ₂^× ≅ G_{ℚ₂}^{ab} with its ramification filtration, the dyadic Hilbert-symbol / cup-product computation, the 2-adic cyclotomic character as the canonical orientation);
• indeed mathlib does not even have the structure theorem identifying G_K(p) as a one-relator pro-p group.

Formalizing Labute's theorem is a major project in its own right, well outside the scope of this development. We therefore record it as the project's single external axiom and build the rest of the local normalization on top of it.

Scope of what this axiom carries: the full marked comparison

The manuscript (reference/q2_manuscript.tex, Remark rem:fullmarkingload, l.1113–1123) is explicit that an unmarked Demushkin classification — a bare abstract isomorphism G_{ℚ₂}(2) ≅ D₀ — is insufficient for the downstream boundary gluing ∂_bd = T × _{ℤ₂} Π: it "identifies only the abstract pro-2 group; it does not fix the terminal comparison after passage to all finite quotients C_{2^m}" of the unramified coordinate. What is genuinely needed (Prop compatiblemarking, l.1085–1110; l.4532–4534) is the fully marked isomorphism (Π, ν₂) ≅ (G_{ℚ₂}(2), ν_ur) of maximal pro-2 quotients — intertwining the integral unramified character, not merely its mod-2 reduction.

This axiom therefore packages the full marked datum (MarkedLabuteIso): besides the profinite isomorphism iso : G_{ℚ₂}(2) ≅ D₀, it supplies the genuine local unramified character nu_ur_loc : G_{ℚ₂}(2) ↠ ℤ₂ (geometric Frobenius ↦ 1) together with the character-compatibility nu_ur_loc = iso.hom ≫ nu_ur — i.e. iso carries the local ν_ur to the D₀-model character Q2Presentation.nu_ur (Local/NuUr.lean, marks (-2, 1, 0)) on the nose.

Mathematically this is Prop markedDem in full = Labute Thm 8 (the abstract classification, lem:standardorientation) plus the orientation-lift rigidification (Prop orientationlift / Labute Thm 4, Prop 3.9, l.839–955: the canonical Demushkin orientation χ₀/χ_loc and the Ψ_u/Θ_b automorphisms correcting an arbitrary abstract f so it fixes the marked abelianization). Both ingredients are irreducible local/anabelian class-field-theoretic input, unavailable in mathlib v4.28.0; we record their conjunction as the project's single external axiom and build the rest of the local normalization on top of it.

structure Q2Presentation.MarkedLabuteIso : Type

The fully marked Labute comparison datum. Bundles the profinite isomorphism G_{ℚ₂}(2) ≅ D₀ of Labute's classification together with the genuine local unramified character nu_ur_loc and the character-compatibility that makes the isomorphism marked (intertwine nu_ur_loc with the D₀-model character Q2Presentation.nu_ur). This is what the manuscript's ∂_bd gluing requires (Remark rem:fullmarkingload): a bare abstract iso is insufficient.

• iso : MaximalPro2Quotient GQ2Profinite ≅ D0

  The abstract profinite isomorphism G_{ℚ₂}(2) ≅ D₀ (Labute's classification).

• nu_ur_loc : MaximalPro2Quotient GQ2Profinite ⟶ ProfiniteZ2

  The genuine local unramified character ν_ur : G_{ℚ₂}(2) ↠ ℤ₂ (geometric Frobenius ↦ 1).

• marked : self.nu_ur_loc = CategoryTheory.CategoryStruct.comp self.iso.hom nu_ur

  Character-compatibility / the marking. The isomorphism intertwines the local unramified character with the D₀-model character: ν_ur on G_{ℚ₂}(2) equals iso followed by Q2Presentation.nu_ur on D₀. This is the orientation-lift content that an unmarked classification lacks.

axiom Q2Presentation.labute_GQ2_maxPro2_marked : MarkedLabuteIso

Labute's classification of G_{ℚ₂}(2), fully marked — the project's single irreducible local-class-field-theoretic input.

The maximal pro-2 quotient G_{ℚ₂}(2) = MaximalPro2Quotient GQ2Profinite of the absolute Galois group of ℚ₂ is isomorphic, as a profinite group, to the standard rank-three dyadic Demushkin group D₀ = ⟨a, s, y ∣ a² s⁴ [s,y] = 1⟩_{pro-2}, and this isomorphism can be chosen to intertwine the unramified characters (MarkedLabuteIso).

This is Labute, Classification of Demushkin groups (Canad. J. Math. 19 (1967) 106–132), Theorem 8 (p. 132, due to Serre, Sém. Bourbaki 1962/63 Exp. 252; stated for q = 2, d odd: x₁²x₂⁴(x₂,x₃)⋯ — at d = [ℚ₂:ℚ₂] = 1 exactly our three- generator a² s⁴ [s,y], the secondary exponent 4 being FORCED by the theorem, not a specialization step), together with the orientation lift (Labute Thm 4 + Corollary, p. 120: the UNIQUE continuous χ : G → U_p, with Im χ an invariant) that rigidifies the abstract isomorphism to the marked one — exactly the content of manuscript Prop markedDem. Secondary confirmation: NSW 2nd ed. p. 417 states the ℚ₂ presentation explicitly. Verbatim-verified against the original paper, 2026-07-09 citability audit (audit/CITABILITY_AUDIT_20260708.md §D1; the former "Prop 3.9" pointer matched no numbered item in Labute 1967 and is corrected here). See the module docstring for why it cannot be proved internally in mathlib v4.28.0, and reference/q2_manuscript.tex l.509–534, 839–955, 1113–1123.

It is consumed only by Q2_marked_Demushkin to supply the fields MarkedDemushkinQ2.isMaximalPro2, .nu_ur_loc, and .marked; #print axioms Q2_marked_Demushkin exhibits it as the sole non-standard axiom of the theorem.

JOINT-CONTENT NOTE (2026-07-08 keep audit): the marking fields are standalone-vacuous — any abstract isomorphism inhabits MarkedLabuteIso via nu_ur_loc := iso.hom ≫ nu_ur — and the orientation-lift content this docstring claims is enforced only JOINTLY with gq2_tame_quotient's nu_compat clause (rigidity of ν_t under Aut(T_A)). The two keeps together carry the marked classification; neither alone does.