The CFT unit-index equals the ramification index

For a finite abelian Galois layer F/ℚ₂ inside ℚ̄₂ = AlgebraicClosure ℚ_[2], local class field theory (B5, LocalReciprocity.norm_reciprocity) identifies Gal(F/ℚ₂) ≅ ℚ₂ˣ / N_{F/ℚ₂}(Fˣ), and the inertia subgroup — the image of the units ℤ₂ˣ ↪ ℚ₂ˣ under reciprocity — has order the ramification index e = FF.e. This file proves that count:

Nat.card ↥(((restrictAb F hab).comp R.recip).comp unitEmbed).range = FF.e.

Design (docs/orchestration/p15f2c2c-handoff.md §3 N2, scoping §half-(B) step 3). With n := finrank ℚ₂ F, N := normSubgroup F, U := unitEmbed.range (= ker v₂):

• norm_val (analytic core): ‖(Algebra.norm ℚ₂ x : ℚ₂)‖ = ‖(x : ℚ̄₂)‖ ^ n, via Algebra.norm_eq_prod_automorphisms + lifting each F ≃ₐ F to ℚ̄₂ (restrictNormalHom_surjective + restrictNormal_commutes) + norm_galois, then card_aut_eq_finrank;
• the integer identity e · v₂(Norm x) = n · v_F(x) (norm_eq_zpow + FF.he, raising ‖·‖ to the e to avoid fractions);
• v₂(N(Fˣ)) = f₀·ℤ for f₀ := v₂(Norm π_F) (so e·f₀ = n, normValPi_dvd_v2_of_mem); hence Gal ⧸ (unit-image) is cyclic, generated by the class of rec(2) of order f₀ (q^k = 1 ↔ f₀ ∣ k — plain orderOf arithmetic, no relindex calculus), and #(unit-image)·f₀ = #Gal = n = e·f₀ forces #(unit-image) = e (Subgroup.card_mul_index).

Kept parametric over (R : LocalReciprocity) and (FF : DyadicUnitFiltration F) (the Reciprocity.lean stress-test / half-A idiom), so the statement is std-3; the axioms B5/B13 enter only when the c2c4 assembly instantiates R := localReciprocity, FF := dyadicUnitFiltration F.

theorem GQ2.UnitNormIndex.norm_val (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (x : ↥F) : ‖(Algebra.norm ℚ_[2]) x‖ = ‖↑x‖ ^ Module.finrank ℚ_[2] ↥F

Analytic core. The ℚ₂-norm of x ∈ F has spectral absolute value ‖x‖^{[F:ℚ₂]}: the norm is the product over Gal(F/ℚ₂) of the conjugates (Algebra.norm_eq_prod_automorphisms), each conjugate has the same spectral norm as x (lift the F-automorphism to ℚ̄₂ and apply norm_galois), and there are finrank ℚ₂ F of them (card_aut_eq_finrank).

theorem GQ2.UnitNormIndex.norm_two : ‖2‖ = 2 ^ (-1)

‖(2 : ℚ₂)‖ = 2 ^ (-1): v₂(2) = 1.

theorem GQ2.UnitNormIndex.e_mul_val_norm (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (FF : DyadicUnitFiltration F) (y : ↥F) (hy : y ≠ 0) (m : ℤ) (hm : ‖↑y‖ = ‖FF.π‖ ^ m) : ↑FF.e * ((Algebra.norm ℚ_[2]) y).valuation = ↑(Module.finrank ℚ_[2] ↥F) * m

The ramification identity. For y ∈ Fˣ with ‖(y:ℚ̄₂)‖ = ‖π_F‖^m (the value-group exponent, norm_eq_zpow), e · v₂(N_{F/ℚ₂} y) = [F:ℚ₂] · m. (Raise ‖N y‖ = ‖π_F‖^{n·m} to the e and match 2-power exponents: ‖π_F‖^e = ‖2‖ = 2^{-1}.)

The v₂-calculus on ℚ₂ˣ and the uniformizer-unit decomposition

theorem GQ2.UnitNormIndex.v2_mul (x y : ℚ_[2]ˣ) : v2 (x * y) = v2 x + v2 y

v₂ is additive: units of ℚ₂ are nonzero, so Padic.valuation_mul applies.

theorem GQ2.UnitNormIndex.v2_zpow (x : ℚ_[2]ˣ) (k : ℤ) : v2 (x ^ k) = k * v2 x

v₂(x^k) = k·v₂(x) for k : ℤ.

theorem GQ2.UnitNormIndex.v2_inv (x : ℚ_[2]ˣ) : v2 x⁻¹ = -v2 x

v₂(x⁻¹) = -v₂(x).

theorem GQ2.UnitNormIndex.v2_uniformizer : v2 uniformizer = 1

v₂(2) = 1.

theorem GQ2.UnitNormIndex.v2_unitEmbed (u : ℤ_[2]ˣ) : v2 (unitEmbed u) = 0

v₂ kills the ℤ₂-units (u and u⁻¹ are both 2-adic integers, so both valuations are ≥ 0 and they sum to 0).

theorem GQ2.UnitNormIndex.mem_unitEmbed_range_of_v2_eq_zero {x : ℚ_[2]ˣ} (hx : v2 x = 0) : x ∈ unitEmbed.range

ker v₂ = unitEmbed.range, the substantive inclusion: a ℚ₂ˣ-element of valuation 0 is the embedding of a ℤ₂-unit — ℤ₂ is literally {x : ℚ₂ // ‖x‖ ≤ 1}, and PadicInt.isUnit_iff detects units by norm 1.

theorem GQ2.UnitNormIndex.eq_zpow_uniformizer_mul_unit (x : ℚ_[2]ˣ) : ∃ (u : ℤ_[2]ˣ), x = uniformizer ^ v2 x * unitEmbed u

The uniformizer-unit decomposition of ℚ₂ˣ: every x is 2^{v₂(x)}·u with u ∈ ℤ₂ˣ.

The norm-valuation f₀ := v₂(N_{F/ℚ₂}(π_F)) and the valuation image of the norm

subgroup

noncomputable def GQ2.UnitNormIndex.piUnit (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (FF : DyadicUnitFiltration F) : (↥F)ˣ

The uniformizer π_F as a unit of the field ↥F.

Equations

• GQ2.UnitNormIndex.piUnit F FF = Units.mk0 ⟨FF.π, ⋯⟩ ⋯

noncomputable def GQ2.UnitNormIndex.normValPi (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (FF : DyadicUnitFiltration F) : ℤ

f₀ := v₂(N_{F/ℚ₂}(π_F)), the valuation of the norm of the uniformizer. (This is the residue degree f = n/e; we never need that identification, only e·f₀ = n and the divisibility f₀ ∣ v₂(N(Fˣ)).)

Equations

• GQ2.UnitNormIndex.normValPi F FF = GQ2.v2 ((Units.map (Algebra.norm ℚ_[2])) (GQ2.UnitNormIndex.piUnit F FF))

theorem GQ2.UnitNormIndex.e_mul_normValPi (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (FF : DyadicUnitFiltration F) : ↑FF.e * normValPi F FF = ↑(Module.finrank ℚ_[2] ↥F)

e · f₀ = n — the m = 1 case of e_mul_val_norm at y = π_F.

theorem GQ2.UnitNormIndex.normValPi_pos (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (FF : DyadicUnitFiltration F) : 1 ≤ normValPi F FF

f₀ ≥ 1.

theorem GQ2.UnitNormIndex.normValPi_dvd_v2_of_mem (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (FF : DyadicUnitFiltration F) {x : ℚ_[2]ˣ} (hx : x ∈ normSubgroup F) : normValPi F FF ∣ v2 x

v₂ maps the norm subgroup into f₀·ℤ: every norm from Fˣ has valuation a multiple of f₀ (the value-group exponent of y scales through e_mul_val_norm, and e cancels).

theorem GQ2.UnitNormIndex.exists_mem_normSubgroup_v2_eq (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] (FF : DyadicUnitFiltration F) (m : ℤ) : ∃ w ∈ normSubgroup F, v2 w = normValPi F FF * m

Realizing the multiples: for every m, some norm has valuation f₀·m — namely N(π_F^m).

The main count: the unit-image in Gal(F/ℚ₂) has exactly e elements

theorem GQ2.UnitNormIndex.card_unitImage_eq_e (R : LocalReciprocity) (F : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥F] [IsGalois ℚ_[2] ↥F] (hab : ∀ (σ τ : Gal(↥F/ℚ_[2])), σ * τ = τ * σ) (FF : DyadicUnitFiltration F) : Nat.card ↥(((restrictAb F hab).comp R.recip).comp unitEmbed).range = FF.e

the Lemma 6.17 vanishing proof, the result. For a finite abelian Galois layer F/ℚ₂ with B13 filtration data FF, the image in Gal(F/ℚ₂) of the ℤ₂-units under the (bundled) reciprocity map has exactly FF.e elements — "inertia has order e", in the only vocabulary the repo carries (no inertia subgroup, no residue fields).

Proof shape (see the module docstring): the quotient of Gal(F/ℚ₂) by the unit-image Gu is generated by the class q of φ(2) (uniformizer-unit decomposition + B5(a) surjectivity), and q^k = 1 ↔ f₀ ∣ k (B5(a) kernel = norm subgroup + the v₂-bookkeeping of normValPi), so [Gal : Gu] = orderOf q = f₀ and #Gu · f₀ = n = e · f₀.

Parametric in R : LocalReciprocity and FF (the half-A idiom): this statement is std-3; the axioms B5/B13 enter only when the c2c4 assembly instantiates R := localReciprocity, FF := dyadicUnitFiltration F. Consumed by c2c4 at F := F₀ = L^{⟨t⟩} to convert "unit-image is odd" into "e_{F₀} is odd".