The unit filtration of a finite dyadic field (supporting definitions for B13)

The norm-one unit subgroup and the depth filtration U^{(i)} = 1 + 𝔭_k^i of a finite extension k/ℚ₂ inside ℚ̄₂, in the repo's spectral-norm vocabulary (the IsDeepUnit idiom): depth is measured against a uniformizer π by ‖u − 1‖ ≤ ‖π‖^i — no valuation ring, residue field, or ramification bookkeeping is introduced.

The structure DyadicUnitFiltration bundles the former B13 axiom content: existence of a uniformizer (discreteness of the value group), the normalization ‖2‖ = ‖π‖^e, and the residue counts of the graded pieces of the filtration — Serre, Local Fields [7], Ch. IV §2, Proposition 6 (verified verbatim against the cited source; the audit copy is not vendored): U^{(0)}/U^{(1)} ≅ k̄^× (order 2^f − 1) and U^{(i)}/U^{(i+1)} ≅ k̄⁺ (order 2^f) for i ≥ 1. The interface GQ2.dyadicUnitFiltration asserting an instance for every finite k lives in GQ2/Foundations/Axioms.lean; everything in this file is a plain definition or a proved lemma.

The proposal's (F2) clause (the inertia twist θ_g = (g•π)/π acting on gr_j by θ_g^j) turned out to be derivable and is therefore NOT a field: g•(1+a) = 1 + θ_g^i·g(a/π^i)·π^i is exact ℚ̄₂-algebra, and θ_g^e = g(u)/u ≡ 1 (mod 𝔪) for inertial g follows from the he normalization with u = π^e/2. See docs/orchestration/p15f1-axiom-proposal.md and the B13 entry of docs/literature-axioms.md.

the deep-part proof.

def GQ2.normUnits (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) : Subgroup (↥k)ˣ

The norm-one units of k — the arithmetic unit group O_k^× of the field k, cut out of (↥k)ˣ (which is all of k ∖ {0}) by the spectral norm.

Equations

• GQ2.normUnits k = { carrier := {u : (↥k)ˣ | ‖↑↑u‖ = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem GQ2.mem_normUnits (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (u : (↥k)ˣ) : u ∈ normUnits k ↔ ‖↑↑u‖ = 1

Membership in normUnits unfolded.

def GQ2.depthUnits (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) (i : ℕ) : Subgroup (↥k)ˣ

The depth-i unit subgroup U^{(i)} = 1 + 𝔭_k^i relative to a uniformizer π: norm-one units with ‖u − 1‖ ≤ ‖π‖^i. (At i = 0 this is all of normUnits k — depthUnits_zero; no hypothesis on π is needed for the subgroup property.)

Equations

• GQ2.depthUnits k π i = { carrier := {u : (↥k)ˣ | ‖↑↑u‖ = 1 ∧ ‖↑↑u - 1‖ ≤ ‖π‖ ^ i}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem GQ2.mem_depthUnits (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) (i : ℕ) (u : (↥k)ˣ) : u ∈ depthUnits k π i ↔ ‖↑↑u‖ = 1 ∧ ‖↑↑u - 1‖ ≤ ‖π‖ ^ i

Membership in depthUnits unfolded.

theorem GQ2.depthUnits_zero (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) : depthUnits k π 0 = normUnits k

At depth 0 the filtration is the full norm-one unit group (‖u − 1‖ ≤ 1 is automatic by the ultrametric inequality).

theorem GQ2.depthUnits_antitone (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (π : AlgebraicClosure ℚ_[2]) (hπ : ‖π‖ ≤ 1) {i j : ℕ} (hij : i ≤ j) : depthUnits k π j ≤ depthUnits k π i

The depth filtration is decreasing (for ‖π‖ ≤ 1).

structure GQ2.DyadicUnitFiltration (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) : Type

The B13 bundle — the unit-filtration data of a finite dyadic field: a uniformizer (value-group discreteness), the ‖2‖ = ‖π‖^e normalization, and the residue counts of the graded pieces (Serre LF [7], Ch. IV §2, Prop. 6). Asserted for every finite k by the axiom GQ2.dyadicUnitFiltration (GQ2/Foundations/Axioms.lean); see the docstring there for the full citation/deviation record.

• π : AlgebraicClosure ℚ_[2]

  A uniformizer: an element of k of maximal norm < 1.

• hπ_mem : self.π ∈ k
• hπ_ne : self.π ≠ 0
• hπ_lt : ‖self.π‖ < 1
• hπ_max (x : AlgebraicClosure ℚ_[2]) : x ∈ k → ‖x‖ < 1 → ‖x‖ ≤ ‖self.π‖

  Discreteness: π attains the maximal norm below 1 (so ‖π‖ generates the value group of k).

• e : ℕ

  The absolute ramification index: v_k(2) = e.

• he_pos : 1 ≤ self.e
• he : ‖2‖ = ‖self.π‖ ^ self.e
• f : ℕ

  The residue degree: #k̄ = 2^f.

• hf_pos : 1 ≤ self.f
• card_gr_zero : Nat.card (↥(normUnits k) ⧸ (depthUnits k self.π 1).subgroupOf (normUnits k)) = 2 ^ self.f - 1

  Serre LF IV §2 Prop. 6(a): U^{(0)}/U^{(1)} ≅ k̄^×, of order 2^f − 1.

• card_gr (i : ℕ) : 1 ≤ i → Nat.card (↥(depthUnits k self.π i) ⧸ (depthUnits k self.π (i + 1)).subgroupOf (depthUnits k self.π i)) = 2 ^ self.f

  Serre LF IV §2 Prop. 6(b): U^{(i)}/U^{(i+1)} ≅ k̄⁺, of order 2^f, for every i ≥ 1.