B11b-1 — the quadratic layer · B11b-2 — the residue layer #
Proves the former axiom interface B11b (unramifiedQuadratic_units_are_norms) in-repo. This
file is the quadratic layer
(lane B, §1(Q)+(D)): the conjugation σ, k-coordinates on k⟮δa⟯, the norm/trace forms, and
the degenerate δa ∈ k case. Imports Mathlib only (the B13 filtration and the σ-free
Teichmüller bricks of GQ2.TeichmullerLift enter later, at the engine B11b-3).
For k ≤ ℚ̄₂ finite and δa ∈ ℚ̄₂ with δa² = a ∈ kˣ, δa ∉ k:
exists_conj— a global↥k-algebra involutionσ : ℚ̄₂ ≃ₐ[↥k] ℚ̄₂withσδa = −δa(infinite Galois correspondence; the B11b-0 route,QuadraticAdjoin.exists_conjre-ported);norm_galois/norm_conj_eq—σpreserves the spectral norm;conj_apply,norm_coord,trace_coord—σ(x + yδa) = x − yδa,N(x+yδa) = x² − ay²,s(x+yδa) = 2x(x, y ∈ k);exists_coords— everyz ∈ ↥k⟮δa⟯isx + yδa(modByMonicremainder);conj_fixed_iff— on↥k⟮δa⟯,σz = z ↔ z ∈ k;norm_form_of_mem— the degenerate case: ifδa ∈ keveryu ∈ ↥kisx² − ay².
The residue layer below builds on the quadratic layer and the σ-free bricks of
GQ2.TeichmullerLift:
le_of_conj_residue_trivial— the cruxσ̄ = id ⟹ L ≤ k, entirely in norm vocabulary (σ̄ = id⟺∀ z ∈ O_L, ‖σz − z‖ < 1): a norm-onezhas a Teichmüller representativeω(ω^{q−1} = 1,ω ≡ z);σωis a root of unity of the same odd order in the same residue class, so odd-root separation forcesσω = ω, i.e.ω ∈ k— every residue ofLlies ink, and successive approximation closesL ≤ k.exists_conj_unit— contrapositive atδa ∈ L ∖ k: somez₁ ∈ O_Lhas‖σz₁ − z₁‖ = 1("σ̄ ≠ id").trace_covers— the engine result (consumed by the B11b-3 increments): the traces(z) = z + σzcovers the integral elements ofkexactly (not just mod𝔪): writingz₁ = x + yδa, the unit trace valuet := s(z₁) = 2x ∈ khas‖t‖ = 1(char-2 shift:s(z₁)andσz₁ − z₁differ by2z₁), andk-linearity ofsscales it to any target — no residue-field orl^σ̄-linear-algebra interface is needed.
The residue-field inputs of the crux stay hypothesis-abstracted (q, hqn, hqodd,
hlag — Lagrange ‖z^q − z‖ < 1 at L; π, hπmax — the shared uniformizer): B11b-3
discharges them from the B13 filtration at L (q := 2^F, q − 1 odd).
Galois invariance of the spectral norm #
Galois invariance of the spectral norm on ℚ̄₂ (re-port of HilbertLedger.norm_galois,
which is downstream of the axiom file). The extension norm on an algebraic extension of a
complete field is unique, so it is invariant under every ℚ₂-algebra automorphism.
σ preserves the spectral norm (σ is ↥k-linear, a fortiori ℚ₂-linear).
The ⊥-membership port and the conjugation #
Membership in ⊥ : IntermediateField ↥k ℚ̄₂ is membership in k (re-port of
QuadraticAdjoin.mem_bot_iff_mem).
The conjugation σ : ℚ̄₂ ≃ₐ[↥k] ℚ̄₂ with σδa = −δa (re-port of
QuadraticAdjoin.exists_conj): built from the infinite Galois correspondence
(fixedField ⊤ = ⊥), with (σδa)² = δa² forcing the sign.
Coordinate action, norm, and trace #
σ fixes the base: σ (x : ℚ̄₂) = x for x ∈ ↥k.
The conjugation on k-coordinates: σ(x + yδa) = x − yδa.
The norm form: (x + yδa)(x − yδa) = x² − a y² in ↥k (with δa² = a).
The trace form: (x + yδa) + (x − yδa) = x + x (= 2x ∈ k).
Coordinates exist on the adjoin #
The ↥k-minimal polynomial of δa (with δa² = d, δa ∉ k) has degree 2.
Coordinates: every z ∈ ↥k⟮δa⟯ is x + yδa for unique x, y ∈ k
(re-port of QuadraticAdjoin.exists_coords, p %ₘ minpoly remainder).
On ↥k⟮δa⟯, σ fixes exactly k: σz = z ↔ z ∈ k.
The degenerate case δa ∈ k #
Degenerate case: if δa ∈ k (so a is already a square in k), every u ∈ ↥k is a
norm x² − a y² — solve (x − δ'y)(x + δ'y) = u with x = (1+u)/2, y = (u−1)/(2δ').
The residue layer (B11b-2, lane B closure) #
‖2‖ < 1 in ℚ̄₂ (the spectral norm extends the 2-adic norm).
The residue crux (plan §1(R)3, "σ̄ = id ⟹ L = k"), in pure norm vocabulary. If the
conjugation is trivial on residues — ‖σz − z‖ < 1 for every integral z ∈ L — then L ≤ k:
a norm-one z ∈ L has a Teichmüller representative ω (exists_teichmuller, using the
Lagrange input hlag), whose conjugate σω is a root of unity of the same odd order q − 1
in the same residue class, so odd-root separation (norm_sub_eq_one_of_pow_eq_one) forces
σω = ω, i.e. ω ∈ k (conj_fixed_iff); thus every residue of L lies in k, and
successive approximation (le_of_shared_uniformizer) closes L ≤ k.
The residue-field inputs are hypothesis-abstracted (B11b-3 supplies them from the B13
filtration at L): q with ‖q‖ < 1 and q − 1 odd (q = 2^F), Lagrange hlag, and the
shared uniformizer π.
σ̄ ≠ id, in contrapositive form: with δa ∈ L ∖ k
witnessing ¬(L ≤ k), some integral z₁ ∈ L has ‖σz₁ − z₁‖ = 1 — the conjugation moves a
residue.
Trace coverage. The trace s(z) = z + σz hits every integral element
of k from an integral element of L: the witness z₁ of σ̄ ≠ id has unit trace value
t := s(z₁) = 2x ∈ k (z₁ = x + yδa; s(z₁) differs from σz₁ − z₁ by 2z₁, of norm
< 1), and s is k-linear, so z := (c/t)·z₁ does it. No residue-field interface and no
mod 𝔪 bookkeeping: the covering is on the nose.
The approximation engine (B11b-3) — filtration helpers #
‖1 + x‖ = 1 when ‖x‖ < 1 (ultrametric: the unit dominates).
The (↥K)ˣ → ↥K → ℚ̄₂ coercion commutes with powers.
Lagrange in U⁰/U¹ — the single group-theoretic input behind both residue facts. The
graded piece U⁰_K/U¹_K is a finite group of order 2^f − 1 (card_gr_zero), so every
norm-one unit u satisfies u^{2^f − 1} ∈ U¹_K.
Depth-1 start (the square residue layer, via Lagrange with x := u^{2^{f−1}}): a norm-one
unit is a square modulo U¹. Since 2·2^{f−1} = 2^f, x² = u^{2^f} and
u^{2^f} − u = u(u^{2^f−1} − 1) with u^{2^f−1} ∈ U¹.
The Lagrange input hlag for trace_covers at L: with q := 2^F (F the residue
degree of L), ‖z^q − z‖ < 1 for every integral z ∈ L. Unit case: Lagrange
(z^{q−1} ∈ U¹_L); non-unit case: ultrametric on ‖z‖ < 1.
The engine (non-degenerate case). For δa ∉ k, every norm-one unit of k is a value
of the norm form x² − a y². Sets up L = k(δa), the conjugation σ, the shared uniformizer
π (via hunram), and the residue data at L, then runs the successive-approximation engine
against trace_covers.
hunram is IsUnramifiedQuadraticSpectral k δa written unfolded — that predicate is a plain
def in the (downstream) axiom file, so it cannot be named here; the B11b flip supplies it
definitionally.
The B11b capstone (B11b-4): units of an unramified quadratic extension k(√a)/k are
norms — every norm-one u ∈ k is x² − a y². Dispatches the degenerate case δa ∈ k
(norm_form_of_mem, the norm form is then universal) against the engine
units_are_norms_nondegen.
The statement is the axiom GQ2.unramifiedQuadratic_units_are_norms
(GQ2/Foundations/Axioms.lean) with IsUnramifiedQuadraticSpectral k δa written unfolded —
that predicate is a plain def downstream of this file, so it cannot be named here; the B11b-5
public theorem supplies it definitionally from
unramifiedQuadratic_units_are_norms' k a δa hδa hunram.