Teichmüller units, odd-root separation, and successive approximation

The three σ-free ingredients of the residue-field proof of unramifiedQuadratic_units_are_norms are:

• exists_teichmuller — §1(R)1: in a finite (hence complete) subextension L/ℚ₂, a norm-one w with ‖w^q − w‖ < 1 (q of norm < 1, e.g. any even q) has a Teichmüller representative: ω ∈ L with ω^q = ω, ‖ω‖ = 1, ‖ω − w‖ < 1. The sequence w^{qⁿ} is Cauchy (cauchySeq_of_le_geometric, the HilbertLedger.sq_of_near_one template — run in ↥L, since ℚ̄₂ itself is not complete) because x ↦ x^q contracts differences on the unit ball: ‖a^q − b^q‖ ≤ max(‖q‖, ‖a−b‖)·‖a−b‖ (norm_pow_sub_pow_le, via the geometric-sum factorization — one step for any q of norm < 1, no iterated squaring needed).
• norm_sub_eq_one_of_pow_eq_one — §1(R)2: distinct m-th roots of unity (m odd) are at distance 1. Route (simpler than the plan's derivative product, no enumeration of the root set): η := ζ⁻¹ζ' ≠ 1 has ∑_{i<m} η^i = 0, so m = ∑_{i<m}(1 − η^i) with every term of norm ≤ ‖1 − η‖; hence 1 = ‖m‖ ≤ ‖1 − η‖ ≤ 1 (‖m‖ = 1 because m is odd — norm_natCast_eq_one_of_odd, the only 2-adic input).
• le_of_shared_uniformizer — §1(R)4: if π ∈ k is a shared uniformizer for k ≤ L (max-property over L) and every integral z ∈ L is congruent mod 𝔪_L to an element of k (the "l = k̄" hypothesis, in norm form), then L ≤ k — π-adic successive approximation with k-coefficients, plus closedness of the finite-dimensional k.

Interface note. These lemmas need no filtration interface — every B13 input is abstracted into an explicit norm hypothesis (hwq, hπmax, hres), so the file imports Mathlib only. GQ2/UnramifiedQuadraticNorms.lean supplies the concrete filtration data at the call sites. This keeps the elementary approximation layer independent of the filtration implementation.

Axioms: ∅ (std-3 target). Paper: §6.3 via Serre LF Ch. V §2 (see the plan).

Ultrametric power-difference estimates

theorem GQ2.TeichmullerLift.norm_pow_sub_pow_le_norm_sub {K : Type u_1} [NormedField K] [IsUltrametricDist K] {a b : K} (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (m : ℕ) : ‖a ^ m - b ^ m‖ ≤ ‖a - b‖

In an ultrametric field, x ↦ xᵐ is 1-Lipschitz on the unit ball.

theorem GQ2.TeichmullerLift.norm_pow_sub_pow_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] {a b : K} (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (q : ℕ) : ‖a ^ q - b ^ q‖ ≤ max ‖↑q‖ ‖a - b‖ * ‖a - b‖

On the unit ball of an ultrametric field, x ↦ x^q contracts differences by the factor max(‖q‖, ‖a − b‖) — the quantitative "raising to an even power deepens congruences", in one step for any q (the geometric sum ∑ aⁱb^{q−1−i} is q·a^{q−1} up to a multiple of a − b).

The 2-adic input: odd integers are units

theorem GQ2.TeichmullerLift.norm_natCast_eq_one_of_odd {m : ℕ} (hm : Odd m) : ‖↑m‖ = 1

Odd naturals have norm 1 in ℚ̄₂ (the spectral norm extends the 2-adic norm, where odd integers are units).

Brick 2: odd-root separation

theorem GQ2.TeichmullerLift.norm_one_sub_eq_one_of_pow_eq_one {m : ℕ} (hm : Odd m) {η : AlgebraicClosure ℚ_[2]} (hη : η ^ m = 1) (hne : η ≠ 1) : ‖1 - η‖ = 1

1 is at distance exactly 1 from every other root of unity of odd order: m = ∑_{i<m}(1 − ηⁱ) once ∑ ηⁱ = 0, every summand has norm ≤ ‖1 − η‖, and ‖m‖ = 1.

theorem GQ2.TeichmullerLift.norm_sub_eq_one_of_pow_eq_one {m : ℕ} (hm : Odd m) {ζ ζ' : AlgebraicClosure ℚ_[2]} (hζ : ζ ^ m = 1) (hζ' : ζ' ^ m = 1) (hne : ζ ≠ ζ') : ‖ζ - ζ'‖ = 1

Odd-root separation (plan §1(R)2): distinct roots of unity of odd order m in ℚ̄₂ are at norm-distance exactly 1 — they stay distinct in every residue field of odd characteristic-avoiding depth. (Applied at m = 2^F − 1 in the residue layer.)

Brick 1: Teichmüller representatives

theorem GQ2.TeichmullerLift.exists_teichmuller (L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥L] {q : ℕ} (hqn : ‖↑q‖ < 1) {w : AlgebraicClosure ℚ_[2]} (hwL : w ∈ L) (hw1 : ‖w‖ = 1) (hwq : ‖w ^ q - w‖ < 1) : ∃ ω ∈ L, ω ^ q = ω ∧ ‖ω‖ = 1 ∧ ‖ω - w‖ < 1

Teichmüller representative (plan §1(R)1). In a finite (hence complete) subextension L/ℚ₂, every norm-one w ∈ L with ‖w^q − w‖ < 1 (for an exponent q of norm < 1 — in application q = #l, a power of 2, and the congruence is Lagrange in the residue field) is congruent mod 𝔪_L to a genuine (q−1)-st root of unity ω ∈ L: the π-adic limit of the sequence w^{qⁿ}.

Brick 3: successive approximation

theorem GQ2.TeichmullerLift.le_of_shared_uniformizer (k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (hkL : k ≤ L) {π : AlgebraicClosure ℚ_[2]} (hπk : π ∈ k) (hπ0 : π ≠ 0) (hπ1 : ‖π‖ < 1) (hπmax : ∀ z ∈ L, ‖z‖ < 1 → ‖z‖ ≤ ‖π‖) (hres : ∀ z ∈ L, ‖z‖ ≤ 1 → ∃ x ∈ k, ‖z - x‖ < 1) : L ≤ k

Successive approximation (plan §1(R)4). If π ∈ k is a shared uniformizer for the pair k ≤ L (‖π‖ dominates every sub-unit norm of L) and every integral element of L is congruent mod 𝔪_L to an element of k (the residue fields agree), then L ≤ k: every z ∈ O_L is the limit of its π-adic partial sums with k-coefficients, and the finite-dimensional k is closed; a π-power scaling handles general z.