The hunram assembly — increment 1, the e-chain

The capstone of the analytic-hunram derivation (docs/orchestration/p15f2c2c-handoff.md §2): for the involution tower k ≤ L of c2b ([L : k]-fixing-index 2) the norm value groups agree, ‖L^×‖ = ‖k^×‖, in the verbatim shape hvanish_involution consumes.

This increment builds the complete arithmetic skeleton — everything except the "e_{F₀} is odd" input (steps 3–4 of the derivation, gated on c2c2's CFT unit-index theorem + the c2c3 factoring/orientation), which is threaded as the hypothesis hodd:

1. the index-2 leg (relE_dvd_of_index, instantiated at c2b's hindex): m := e(L/k) ∣ 2 — c2c1's coset norm at the pair L.fixingSubgroup ≤ k.fixingSubgroup, memberships transported along the Galois correspondence fixedField (fixingSubgroup ·) = ·.
2. the ⟨t⟩-preimage leg: T₀ := ρ⁻¹⟨t⟩ (the kerGal two-views idiom), F₀ := fixedField T₀ finite-dimensional (open subgroup), [T₀ : ker ρ] = orderOf t (first isomorphism at the restricted ρ), whence e(L/F₀) ∣ orderOf t — odd by Tame.tame_odd_order at the instantiation.
3. the assembly (hunram_of_odd_eF0): e_L = e(L/F₀)·e_{F₀} odd [hodd], e_L = m·e_k, m ∣ 2 ⟹ m = 1 ⟹ ‖π_L‖ = ‖π_k‖ ⟹ half (A)'s hunram_of_uniformizer_norm_eq.

Axioms: everything here is std-3 (B13 data threaded as DyadicUnitFiltration hypotheses, the half-(A) idiom). The increment-2 discharge of hodd will carry {B5, B10′} via c2c2/c2c3; the final instantiation adds B13 at the dyadicUnitFiltration call sites.

Leg 1 — the index-2 pair: relE (L/k) ∣ [k.fixingSubgroup : L.fixingSubgroup]

theorem GQ2.UnramifiedBridge.relE_dvd_of_index {k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} [FiniteDimensional ℚ_[2] ↥k] [FiniteDimensional ℚ_[2] ↥L] (Fk : DyadicUnitFiltration k) (FL : DyadicUnitFiltration L) (hkL : k ≤ L) [Finite (↥k.fixingSubgroup ⧸ L.fixingSubgroup.subgroupOf k.fixingSubgroup)] : GaloisCosetNorm.relE Fk FL hkL ∣ ↑(Nat.card (↥k.fixingSubgroup ⧸ L.fixingSubgroup.subgroupOf k.fixingSubgroup))

relE divides the fixing-subgroup index (leg 1, general form): for a tower k ≤ L of finite-dimensional intermediate fields, the relative ramification index e(L/k) divides [k.fixingSubgroup : L.fixingSubgroup]. c2c1's coset-norm package at the subgroup pair, with memberships transported along the Galois correspondence.

theorem GQ2.UnramifiedBridge.relE_dvd_two {k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} [FiniteDimensional ℚ_[2] ↥k] [FiniteDimensional ℚ_[2] ↥L] (Fk : DyadicUnitFiltration k) (FL : DyadicUnitFiltration L) (hkL : k ≤ L) (hindex : (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index = 2) : GaloisCosetNorm.relE Fk FL hkL ∣ 2

Leg 1 at c2b's shape: the index-2 hypothesis gives e(L/k) ∣ 2.

Leg 2 — the ⟨t⟩-preimage: T₀ := ρ⁻¹⟨t⟩, F₀ := fixedField T₀, [T₀ : ker ρ] = ord t

def GQ2.UnramifiedBridge.preimGal {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (S : Subgroup C) : Subgroup (Kummer.GaloisGroup ℚ_[2])

The ρ-preimage of a subgroup S ≤ C, repackaged as a subgroup of the AlgEquiv-view Galois group (the ResidueLift.kerGal two-views idiom: the closure proofs cross the AbsGalQ2/Kummer.GaloisGroup instance split by exact-level defeq).

Equations

• GQ2.UnramifiedBridge.preimGal ρ S = { carrier := {x : GQ2.Kummer.GaloisGroup ℚ_[2] | ρ (GQ2.ResidueLift.toAbs x) ∈ S}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

noncomputable def GQ2.UnramifiedBridge.inertiaField {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (t : C) : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])

The ⟨t⟩-preimage field F₀ := ℚ̄₂^{ρ⁻¹⟨t⟩} — the fixed field of the preimage of the inertia-image ⟨t⟩ ≤ C.

Equations

• GQ2.UnramifiedBridge.inertiaField ρ t = IntermediateField.fixedField (GQ2.UnramifiedBridge.preimGal ρ (Subgroup.zpowers t))

theorem GQ2.UnramifiedBridge.fixingSubgroup_inertiaField {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) (t : C) : (inertiaField ρ t).fixingSubgroup = preimGal ρ (Subgroup.zpowers t)

The closed-subgroup Galois correspondence recovers the preimage from its fixed field (the ResidueLift.fixingSubgroup_splitField mirror).

theorem GQ2.UnramifiedBridge.inertiaField_finiteDimensional {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) (t : C) : FiniteDimensional ℚ_[2] ↥(inertiaField ρ t)

F₀ is finite over ℚ₂ (its fixing subgroup is open).

theorem GQ2.UnramifiedBridge.inertiaField_le {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (t : C) : inertiaField ρ t ≤ IntermediateField.fixedField (ResidueLift.kerGal ρ)

F₀ ≤ L for L := fixedField (ker ρ): the fixed field is antitone in the subgroup.

theorem GQ2.UnramifiedBridge.card_quot_preimGal {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (hρsurj : Function.Surjective ⇑ρ) (t : C) : Nat.card (↥(preimGal ρ (Subgroup.zpowers t)) ⧸ (ResidueLift.kerGal ρ).subgroupOf (preimGal ρ (Subgroup.zpowers t))) = orderOf t

The quotient count of leg 2: [T₀ : ker ρ] = orderOf t for surjective ρ — the first isomorphism theorem at the restriction T₀ → ⟨t⟩ of ρ.

Leg 3 + assembly — the odd e-chain forces m = 1, whence hunram

theorem GQ2.UnramifiedBridge.hunram_of_odd_eF0 {k L F₀ : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} [FiniteDimensional ℚ_[2] ↥k] [FiniteDimensional ℚ_[2] ↥L] [FiniteDimensional ℚ_[2] ↥F₀] (Fk : DyadicUnitFiltration k) (FL : DyadicUnitFiltration L) (F₀F : DyadicUnitFiltration F₀) (hkL : k ≤ L) (hF₀L : F₀ ≤ L) (hm2 : GaloisCosetNorm.relE Fk FL hkL ∣ 2) {r : ℕ} (hrodd : Odd r) (hdvd : GaloisCosetNorm.relE F₀F FL hF₀L ∣ ↑r) (hodd : Odd F₀F.e) (x : AlgebraicClosure ℚ_[2]) : x ≠ 0 → x ∈ L → ∃ (y : AlgebraicClosure ℚ_[2]), y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖

The e-chain assembly (the Lemma 6.17 vanishing proof, modulo the c2c2/c2c3 oddness input): given

• the index-2 leg e(L/k) ∣ 2,
• the inertia leg e(L/F₀) ∣ r with r odd, and
• the CFT input e_{F₀} odd (hodd — c2c2's unit-index theorem + the c2c3 factoring/orientation kill the even part; threaded here),

the tower k ≤ L has equal uniformizer norms, hence equal value groups — the analytic hunram, verbatim in the shape ShapiroDeepness.hvanish_involution consumes.

Arithmetic: e_L = e(L/F₀)·e_{F₀} is odd (both factors odd — a divisor of an odd number is odd); e_L = e(L/k)·e_k then forces e(L/k) odd; an odd positive divisor of 2 is 1; relE_spec at 1 gives ‖π_k‖ = ‖π_L‖.

Increment 2 — the oddness input hodd

The remaining CFT/orientation half (design §2 steps 3–4): Gal(F₀/ℚ₂) is abelian, its ℤ₂-unit image (c2c2's card_unitImage_eq_e: #Gu = e_{F₀}) dies in every finite 2-group quotient (the c2c3 factoring through ν_t + the B10′ orientation), and a subgroup of a finite group with commuting elements that dies in the odd-torsion quotient has odd order — whence e_{F₀} is odd.

Descending a hom along a surjection

noncomputable def GQ2.UnramifiedBridge.descendHom {G : Type u_1} {C : Type u_2} {Q : Type u_3} [Group G] [Group C] [Group Q] (ρ : G →* C) (hρ : Function.Surjective ⇑ρ) (ξ : G →* Q) (hker : ρ.ker ≤ ξ.ker) : C →* Q

Descend ξ : G →* Q along a surjection ρ : G →* C with ker ρ ≤ ker ξ.

Equations

• GQ2.UnramifiedBridge.descendHom ρ hρ ξ hker = { toFun := fun (c : C) => ξ (Function.surjInv hρ c), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.UnramifiedBridge.descendHom_apply {G : Type u_1} {C : Type u_2} {Q : Type u_3} [Group G] [Group C] [Group Q] (ρ : G →* C) (hρ : Function.Surjective ⇑ρ) (ξ : G →* Q) (hker : ρ.ker ≤ ξ.ker) (g : G) : (descendHom ρ hρ ξ hker) (ρ g) = ξ g

The defining property: descendHom ρ hρ ξ hker (ρ g) = ξ g.

The odd-part machinery

def GQ2.UnramifiedBridge.oddTorsion {G : Type u_1} [Group G] (hab : ∀ (a b : G), a * b = b * a) : Subgroup G

The odd-torsion subgroup of a finite group whose elements commute: the elements of odd order. (Stated with the commutativity as a hypothesis hab rather than [CommGroup G], matching the hab-shape of Gal(F₀/ℚ₂) in the assembly.)

Equations

• GQ2.UnramifiedBridge.oddTorsion hab = { carrier := {g : G | Odd (orderOf g)}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem GQ2.UnramifiedBridge.oddTorsion_normal {G : Type u_1} [Group G] (hab : ∀ (a b : G), a * b = b * a) : (oddTorsion hab).Normal

theorem GQ2.UnramifiedBridge.odd_card_oddTorsion {G : Type u_1} [Group G] [Finite G] (hab : ∀ (a b : G), a * b = b * a) : Odd (Nat.card ↥(oddTorsion hab))

The odd-torsion subgroup has odd order (Cauchy contrapositive: an even order would produce an element of order 2 inside it).

theorem GQ2.UnramifiedBridge.isPGroup_quotient_oddTorsion {G : Type u_1} [Group G] [Finite G] (hab : ∀ (a b : G), a * b = b * a) : IsPGroup 2 (G ⧸ oddTorsion hab)

The quotient by the odd torsion is a 2-group: g^{2^a} has odd order for a := (orderOf g).factorization 2, so every class has 2-power order.

The tame kill: reciprocity unit-images die in every finite 2-group through C

theorem GQ2.UnramifiedBridge.unit_dies_in_two_group {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {Q : Type u_1} [Group Q] [Finite Q] (hQ2 : IsPGroup 2 Q) (R : LocalReciprocity) (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (horient : TameUnitOrientation R B.tameF) (ξ' : C →* Q) (u : ℤ_[2]ˣ) (g : AbsGalQ2) (hg : toAb g = R.recip (unitEmbed u)) : ξ' (ρ g) = 1

The tame kill (design §2 step 4): any hom ξ' : C →* Q into a finite 2-group kills ρ g whenever g lifts a reciprocity unit-image. ξ' ∘ ρ = (ξ' ∘ c) ∘ B.tameF (hfac) with ξ' ∘ c continuous (C discrete), the orientation gives ν_t (B.tameF g) = 1, and the c2c3 factoring map_eq_one_of_nuT_eq_one_finite kills it. The topology on Q is irrelevant — the discrete one is installed locally.

e_{F₀} is odd

theorem GQ2.UnramifiedBridge.odd_e_inertiaField {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (R : LocalReciprocity) (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (horient : TameUnitOrientation R B.tameF) (F₀F : DyadicUnitFiltration (inertiaField ρ (c tameTau))) : Odd F₀F.e

The oddness input (design §2 steps 3–4 assembled): for the inertia-preimage field F₀ := ℚ̄₂^{ρ⁻¹⟨t⟩} at t := c tameTau, the absolute ramification index e_{F₀} is odd.

⟨t⟩ ◁ C (Tame.zpowers_normal_of_tame on the pushed tame relation), so F₀/ℚ₂ is Galois (InfiniteGalois.normal_iff_isGalois); the restriction G_ℚ₂ → Gal(F₀/ℚ₂) descends along ρ to a surjection κ : C →* Gal(F₀/ℚ₂) killing ⟨t⟩, so Gal(F₀/ℚ₂) is a quotient of the cyclic C/⟨t⟩ — abelian. c2c2's card_unitImage_eq_e counts the reciprocity unit-image as e_{F₀}; the tame kill sends it into the odd-torsion subgroup, whose order is odd.

The finale: the analytic hunram for the involution tower

theorem GQ2.UnramifiedBridge.hunram_involution {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {k L : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])} [FiniteDimensional ℚ_[2] ↥k] [FiniteDimensional ℚ_[2] ↥L] (R : LocalReciprocity) (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (horient : TameUnitOrientation R B.tameF) (hkL : k ≤ L) (hindex : (L.fixingSubgroup.subgroupOf k.fixingSubgroup).index = 2) (hLfix : L.fixingSubgroup = ResidueLift.kerGal ρ) (x : AlgebraicClosure ℚ_[2]) : x ≠ 0 → x ∈ L → ∃ (y : AlgebraicClosure ℚ_[2]), y ≠ 0 ∧ y ∈ k ∧ ‖x‖ = ‖y‖

the Lemma 6.17 vanishing proof, the result: the analytic hunram for c2b's involution tower — for k ≤ L with fixing-index 2 and L the splitting field of ρ (hLfix), the norm value groups of L and k agree, verbatim in the shape ShapiroDeepness.hvanish_involution and SectionSix.lemma_6_16 consume.

Composes the whole c2c chain: half (A) + increments 1–2 of this file + c2c1's relE kit + c2c2's card_unitImage_eq_e + c2c3's factoring/orientation. Parametric in R : LocalReciprocity and the orientation horient (instantiated by the consumer at R := localReciprocity, horient := tameUnitOrientation_witness-style at the axiom witness); the B13 filtrations are taken from dyadicUnitFiltration. Ax: std-3 + B13 (B5/B10′ enter only at the consumer's instantiation of R/horient).