The Galois coset-norm kit + the relative ramification index

Two axiom-free kits feeding the c2c4 assembly of the analytic hunram (docs/orchestration/p15f2c2c-handoff.md).

Part 1 — the coset norm. For H ≤ K closed subgroups of Gal(ℚ̄₂/ℚ₂) with finite index [K : H], the product cosetNorm H K x = ∏_{c ∈ K ⧸ H} (out c) • x of the K-cosets of H applied to x:

• is K-invariant, hence lands in fixedField K, when x ∈ fixedField H (cosetNorm_mem);
• has spectral norm ‖cosetNorm H K x‖ = ‖x‖ ^ [K : H] (norm_cosetNorm, from norm_galois).

So for a tower k ≤ L (H = L.fixingSubgroup ≤ K = k.fixingSubgroup) it realizes ‖x‖ ^ [L : k] ∈ ‖k^×‖ for every x ∈ L^× — the input to Part 2's divisibility.

Part 2 — the relative ramification index. Over B13 DyadicUnitFiltration data (kept as hypotheses, half-A idiom, so statements stay axiom-free), for a tower F ≤ L: relE with ‖π_F‖ = ‖π_L‖ ^ relE, the tower formula e_L = relE * e_F, and the divisibility relE ∣ n whenever ‖x‖ ^ n ∈ ‖F^×‖ for all x ∈ L^×. c2c4 instantiates twice ([L : k] ⟹ relE ∣ 2, ⟨t⟩-orbit ⟹ relE ∣ r).

Axiom-free throughout (Ax = ∅, std-3).

Part 1 — the coset norm

noncomputable def GQ2.GaloisCosetNorm.cosetNorm (H K : Subgroup (Kummer.GaloisGroup ℚ_[2])) [Fintype (↥K ⧸ H.subgroupOf K)] (x : AlgebraicClosure ℚ_[2]) : AlgebraicClosure ℚ_[2]

The coset norm: the product over the K-cosets of H of the coset representatives applied to x. Uses Quotient.out representatives; the value is representative-independent on fixedField H (smul_eq_of_quot_eq).

Equations

• GQ2.GaloisCosetNorm.cosetNorm H K x = ∏ c : ↥K ⧸ H.subgroupOf K, ↑(Quotient.out c) • x

theorem GQ2.GaloisCosetNorm.smul_eq_of_quot_eq {H K : Subgroup (Kummer.GaloisGroup ℚ_[2])} {x : AlgebraicClosure ℚ_[2]} (hx : x ∈ IntermediateField.fixedField H) {g₁ g₂ : ↥K} (h : ↑g₁ = ↑g₂) : ↑g₁ • x = ↑g₂ • x

Representative independence (the well-definedness (i)): on fixedField H, two elements of K in the same H-coset act identically.

theorem GQ2.GaloisCosetNorm.cosetNorm_ne_zero {H K : Subgroup (Kummer.GaloisGroup ℚ_[2])} [Fintype (↥K ⧸ H.subgroupOf K)] {x : AlgebraicClosure ℚ_[2]} (hx : x ≠ 0) : cosetNorm H K x ≠ 0

Each factor is nonzero, so the coset norm of a nonzero element is nonzero.

theorem GQ2.GaloisCosetNorm.norm_cosetNorm {H K : Subgroup (Kummer.GaloisGroup ℚ_[2])} [Fintype (↥K ⧸ H.subgroupOf K)] (x : AlgebraicClosure ℚ_[2]) : ‖cosetNorm H K x‖ = ‖x‖ ^ Nat.card (↥K ⧸ H.subgroupOf K)

(iii) the norm formula: ‖cosetNorm‖ = ‖x‖ ^ [K : H] (each factor is ‖x‖ by norm_galois).

theorem GQ2.GaloisCosetNorm.cosetNorm_mem {H K : Subgroup (Kummer.GaloisGroup ℚ_[2])} [Fintype (↥K ⧸ H.subgroupOf K)] {x : AlgebraicClosure ℚ_[2]} (hx : x ∈ IntermediateField.fixedField H) : cosetNorm H K x ∈ IntermediateField.fixedField K

(ii) K-invariance: on fixedField H the coset norm lands in fixedField K (left multiplication by g ∈ K permutes the cosets, and the finite product is reordered).

theorem GQ2.GaloisCosetNorm.exists_mem_fixedField_norm_pow {H K : Subgroup (Kummer.GaloisGroup ℚ_[2])} [Fintype (↥K ⧸ H.subgroupOf K)] {x : AlgebraicClosure ℚ_[2]} (hx : x ∈ IntermediateField.fixedField H) (hx0 : x ≠ 0) : ∃ y ∈ IntermediateField.fixedField K, y ≠ 0 ∧ ‖x‖ ^ Nat.card (↥K ⧸ H.subgroupOf K) = ‖y‖

c2c4-facing package: for a nonzero x ∈ fixedField H, the power ‖x‖ ^ [K : H] is the spectral norm of a nonzero element of fixedField K (the coset norm). This is the ‖x‖ ^ n ∈ ‖(fixedField K)^×‖ input consumed by relE_dvd.

Part 2 — the relative ramification index of a tower F ≤ L

noncomputable def GQ2.GaloisCosetNorm.relE {F L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (FF : DyadicUnitFiltration F) (FL : DyadicUnitFiltration L) (hFL : F ≤ L) : ℤ

The relative ramification index e(L/F) of a tower F ≤ L, in norm vocabulary: the integer m with ‖π_F‖ = ‖π_L‖ ^ m (it exists by norm_eq_zpow, as π_F ∈ F ≤ L).

Equations

• GQ2.GaloisCosetNorm.relE FF FL hFL = ⋯.choose

theorem GQ2.GaloisCosetNorm.relE_spec {F L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (FF : DyadicUnitFiltration F) (FL : DyadicUnitFiltration L) (hFL : F ≤ L) : ‖FF.π‖ = ‖FL.π‖ ^ relE FF FL hFL

Defining property of relE: ‖π_F‖ = ‖π_L‖ ^ e(L/F).

theorem GQ2.GaloisCosetNorm.e_eq_relE_mul {F L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (FF : DyadicUnitFiltration F) (FL : DyadicUnitFiltration L) (hFL : F ≤ L) : ↑FL.e = relE FF FL hFL * ↑FF.e

Tower multiplicativity of the absolute ramification index: e_L = e(L/F) · e_F (both uniformizers meet ‖2‖ = ‖π‖^e, and ‖π_F‖ = ‖π_L‖^{e(L/F)}; zpow-injectivity on ‖π_L‖ ∈ (0,1)).

theorem GQ2.GaloisCosetNorm.relE_pos {F L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (FF : DyadicUnitFiltration F) (FL : DyadicUnitFiltration L) (hFL : F ≤ L) : 1 ≤ relE FF FL hFL

e(L/F) ≥ 1 (a genuine relative index): from tower multiplicativity and e_L, e_F ≥ 1.

theorem GQ2.GaloisCosetNorm.relE_dvd {F L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (FF : DyadicUnitFiltration F) (FL : DyadicUnitFiltration L) (hFL : F ≤ L) {n : ℕ} (hn : ∀ (x : AlgebraicClosure ℚ_[2]), x ≠ 0 → x ∈ L → ∃ (y : AlgebraicClosure ℚ_[2]), y ≠ 0 ∧ y ∈ F ∧ ‖x‖ ^ n = ‖y‖) : relE FF FL hFL ∣ ↑n

The divisibility feeding c2c4: if ‖x‖ ^ n lies in ‖(fixedField F)^×‖ for every x ∈ L^×, then e(L/F) ∣ n. (Test at x = π_L: ‖π_L‖^n = ‖π_F‖^a = ‖π_L‖^{e(L/F)·a}.)