The residue-trivial tame lift — proved, no new axiom

DimClose.lemma_6_17_dim_of_residueLift reduced lemma_6_17_dim to one arithmetic input: a lift g₀ of tame inertia (ρ g₀ = c tameTau) acting trivially on the residue field (IsResidueTrivial (ker ρ) g₀). The classical statement is "tame inertia acts trivially on residue fields" (Serre, Local Fields, Ch. IV §1: inertia is by definition the kernel of the residue action, and wild + tame inertia sit inside it). This file derives it from the existing axiom budget — no residue fields and no new axiom — by a commutator trick:

1. τ is a commutator. The tame relation σ⁻¹τσ = τ² gives τ = (σ⁻¹τσ)τ⁻¹ = [σ⁻¹, τ] in T_tame, so tameF-surjectivity produces a lift of τ that is a literal commutator g₀ = s⁻¹ t s t⁻¹ in G_ℚ₂.
2. Commutators are residue-trivial, because the residue action is abelian (Gal(𝔽̄₂/𝔽₂) = Ẑ). In the repo's spectral-norm vocabulary this is proved from scratch:
   • Teichmüller approximation (exists_rootOfUnity_near): every y ∈ ℚ̄₂ with ‖y‖ = 1 is within norm < 1 of a root of unity. Proof: k := ℚ₂(y) is finite over ℚ₂; the B13 unit-filtration bundle gives #(U⁰(k)/U¹(k)) = 2^f − 1 =: m, so ‖y^m − 1‖ < 1; X^m − 1 splits over ℚ̄₂ and ∏_ζ ‖y − ζ‖ = ‖y^m − 1‖ < 1, so some factor is < 1 (ultrametric pigeonhole — no Hensel needed).
   • Commuting action on roots of unity (galois_smul_smul_comm_of_rootOfUnity): Galois elements act on ⟨ζ⟩ by power maps (IsPrimitiveRoot.eq_pow_of_pow_eq_one), which commute.
   • Hence ‖[a,b]x − x‖ = ‖(ab)y − (ba)y‖ ≤ max(‖y − ζ‖, 0, ‖ζ − y‖) < 1 (commutator_isResidueTrivial).

The result is exists_residueTrivial_tameLift. Everything is #print axioms ⊆ std-3 + B13 (dyadicUnitFiltration), already in the census.

Step 1: the ultrametric pigeonhole

theorem GQ2.ResidueLift.exists_nthRoot_near (y : AlgebraicClosure ℚ_[2]) (m : ℕ) (hm : 1 ≤ m) (h : ‖y ^ m - 1‖ < 1) : ∃ (ζ : AlgebraicClosure ℚ_[2]), ζ ^ m = 1 ∧ ‖y - ζ‖ < 1

If ‖y^m − 1‖ < 1 (m ≥ 1), some m-th root of unity is within norm < 1 of y: X^m − 1 splits over ℚ̄₂ and the product of the root distances is ‖y^m − 1‖.

Step 2: Teichmüller approximation via the B13 unit filtration

theorem GQ2.ResidueLift.exists_rootOfUnity_near (y : AlgebraicClosure ℚ_[2]) (hy : ‖y‖ = 1) : ∃ (m : ℕ) (ζ : AlgebraicClosure ℚ_[2]), 1 ≤ m ∧ ζ ^ m = 1 ∧ ‖y - ζ‖ < 1

Every norm-one element of ℚ̄₂ is within norm < 1 of a root of unity. k := ℚ₂(y) is finite over ℚ₂; the B13 bundle gives #(U⁰(k)/U¹(k)) = 2^f − 1 =: m, so ‖y^m − 1‖ ≤ ‖π‖ < 1, and the pigeonhole produces the nearby m-th root of unity.

Step 3: Galois elements commute on roots of unity

theorem GQ2.ResidueLift.galois_smul_smul_comm_of_rootOfUnity (ζ : AlgebraicClosure ℚ_[2]) (m : ℕ) (hm : 1 ≤ m) (hζ : ζ ^ m = 1) (a b : Kummer.GaloisGroup ℚ_[2]) : a • b • ζ = b • a • ζ

Galois elements act on the powers of a root of unity by commuting power maps.

Step 4: commutators are residue-trivial

theorem GQ2.ResidueLift.commutator_isResidueTrivial (N : Subgroup (Kummer.GaloisGroup ℚ_[2])) (a b : Kummer.GaloisGroup ℚ_[2]) : IsResidueTrivial N (a * b * a⁻¹ * b⁻¹)

Commutators of G_ℚ₂ are residue-trivial — the residue action is abelian, in spectral-norm form: for any a, b and integral x, ‖(aba⁻¹b⁻¹)x − x‖ < 1. (The N-fixedness hypothesis of IsResidueTrivial is not even needed.)

Step 5: the residue-trivial tame lift

theorem GQ2.ResidueLift.exists_residueTrivial_tameLift {C : Type} [Group C] [TopologicalSpace C] (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) : ∃ (g₀ : AbsGalQ2), ρ g₀ = c tameTau ∧ IsResidueTrivial ρ.ker g₀

The residue-trivial tame lift — proved (no axiom): the tame relation σ⁻¹τσ = τ² makes τ a commutator, so it lifts to a commutator of G_ℚ₂, which is residue-trivial by commutator_isResidueTrivial. This is the last input of DimClose.lemma_6_17_dim_of_residueLift.

Step 6: the splitting-field plumbing from the infinite Galois correspondence

def GQ2.ResidueLift.toAbs (x : Kummer.GaloisGroup ℚ_[2]) : AbsGalQ2

The identity bridge from the AlgEquiv-view Galois group to AbsGalQ2 (the two views are the same type; the bridge keeps function applications in one view).

Equations

• GQ2.ResidueLift.toAbs x = x

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

ker ρ, repackaged as a subgroup of the AlgEquiv-view Galois group (the two views' Group instances agree only at default transparency, so the closure proofs go by exact).

Equations

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

theorem GQ2.ResidueLift.mem_kerGal {C : Type} [Group C] [TopologicalSpace C] (ρ : AbsGalQ2 →ₜ* C) (x : Kummer.GaloisGroup ℚ_[2]) : x ∈ ρ.ker ↔ x ∈ kerGal ρ

theorem GQ2.ResidueLift.kerGal_isOpen {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) : IsOpen ↑(kerGal ρ)

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

The splitting field of ρ: the fixed field of ker ρ.

Equations

• GQ2.ResidueLift.splitField ρ = IntermediateField.fixedField (GQ2.ResidueLift.kerGal ρ)

theorem GQ2.ResidueLift.fixingSubgroup_splitField {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) : (splitField ρ).fixingSubgroup = kerGal ρ

The closed-subgroup Galois correspondence recovers ker ρ from its fixed field.

theorem GQ2.ResidueLift.splitField_finiteDimensional {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (ρ : AbsGalQ2 →ₜ* C) : FiniteDimensional ℚ_[2] ↥(splitField ρ)

ker ρ is open, so its fixed field is finite over ℚ₂.

theorem GQ2.ResidueLift.htriv_zmod2 {G : Type u_1} [Group G] [DistribMulAction G (ZMod 2)] (g : G) (m : ZMod 2) : g • m = m

Any action of any group on 𝔽₂ is trivial.

Step 7: lemma_6_17_dim, fully closed downstream

theorem GQ2.ResidueLift.lemma_6_17_dim_final {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [Finite V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), c tameTau • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) : Nat.card ↑(SectionSix.deepPart ρ) ^ 2 = Nat.card (ContCoh.H1 AbsGalQ2 V)

lemma_6_17_dim, closed (the deep-part proof + the residue-lift derivation): the §6.3 deep-half dimension identity #X₊² = #H¹(ℚ₂, V), from SectionSix.lemma_6_17_dim's own hypothesis set plus only the finiteness instance [Finite (H¹(ker ρ, 𝔽₂))] (the local finiteness H¹(G_K, 𝔽₂) ≅ K^×/2, supplied by the B12/B13 interface). No new axiom: the residue-trivial tame lift is exists_residueTrivial_tameLift, and the splitting field with its Galois-correspondence data is splitField.