The analytic hunram from equal value groups

The involution vanish route of the Lemma 6.17 vanishing proof (SectionSix.lemma_6_17_vanish) threads, through ShapiroDeepness.hvanish_involution / hvanish_involution_of_deepClass and ultimately SectionSix.lemma_6_16 / HilbertLedger.cup_unramified_unit, the analytic hunram hypothesis

∀ x : ℚ̄₂, x ≠ 0 → x ∈ L → ∃ y : ℚ̄₂, y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖,

i.e. the value groups of the tower k ≤ L coincide (‖L^×‖ = ‖k^×‖) — the statement that L/k is unramified, in the repo's spectral-norm vocabulary (no valuation ring / residue field; see B13's convention).

This file is half (A) of the Lemma 6.17 vanishing proof (docs/orchestration/p15f2c2c-scoping.md): given the B13 DyadicUnitFiltration data of k and L and the unramifiedness datum in norm vocabulary — equal uniformizer norm ‖π_L‖ = ‖π_k‖ (equivalently equal absolute ramification index e_L = e_k) — the analytic hunram holds. The remaining half (B) — deriving ‖π_L‖ = ‖π_k‖ from the group-level datum ρ(ĝ) ∉ inertia (c2b Step-0) — is the flagged leaf decision (axiom-vs-derive, owner sign-off); it is not in this file.

The core is exists_nat_val (GQ2/DeepCount.lean): B13 discreteness (hπ_max) makes every nonzero k-integral element's norm an exact power of ‖π‖. We lift it to a ℤ-power (norm_eq_zpow, handling ‖x‖ > 1 via x⁻¹) and transport across the equal uniformizer norm.

theorem GQ2.UnramifiedNorm.norm_eq_zpow {k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (F : DyadicUnitFiltration k) {x : AlgebraicClosure ℚ_[2]} (hx : x ∈ k) (hx0 : x ≠ 0) : ∃ (n : ℤ), ‖x‖ = ‖F.π‖ ^ n

Value-group generation. With a B13 uniformizer π for k (discreteness hπ_max), every nonzero x ∈ k has norm an integer power of ‖π‖. For ‖x‖ ≤ 1 this is exists_nat_val; for ‖x‖ > 1 apply it to x⁻¹ ∈ k and negate the exponent.

theorem GQ2.UnramifiedNorm.hunram_of_uniformizer_norm_eq {k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (Fk : DyadicUnitFiltration k) (FL : DyadicUnitFiltration L) (hπ : ‖FL.π‖ = ‖Fk.π‖) (x : AlgebraicClosure ℚ_[2]) : x ≠ 0 → x ∈ L → ∃ (y : AlgebraicClosure ℚ_[2]), y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖

c2c-A: the analytic hunram from equal uniformizer norm. Given B13 filtration data for k and L with ‖π_L‖ = ‖π_k‖ (the unramifiedness datum in norm vocabulary), every nonzero x ∈ L has the same norm as some nonzero y ∈ k — namely y = π_k^n where ‖x‖ = ‖π_L‖^n. This is exactly the hunram hypothesis of SectionSix.lemma_6_16 / ShapiroDeepness.hvanish_involution.

theorem GQ2.UnramifiedNorm.uniformizer_norm_eq_of_e_eq {k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} (Fk : DyadicUnitFiltration k) (FL : DyadicUnitFiltration L) (he : FL.e = Fk.e) : ‖FL.π‖ = ‖Fk.π‖

Equal absolute ramification index ⟹ equal uniformizer norm. Both uniformizers satisfy ‖2‖ = ‖π‖^e (he), so equal e forces equal ‖π‖ (positive e-th roots of the same ‖2‖ ∈ (0,1)). Lets half (B) supply the unramifiedness datum in the conceptually-cleaner e_L = e_k form.