lemma_6_17_dim, reduced to the residue-trivial tame lift

This leaf assembles the f6/f7/f8 chain and feeds every input of the duality result DeepCount.hduality_of_data from lemma_6_17_dim's own hypotheses, and hands the result to f8's DimAssembly.lemma_6_17_dim_of_hduality (whose hext is already discharged by ShapiroExtend). Concretely:

• the V^∨ regular-summand package (lemma_6_11_of_tame_pair at dualModule, via DimAssembly's dual_* bricks);
• the self-duality eU/heU/ht₀U from the §6.3 invariant form (q, hq, hns, hinv) (DeepDuality.dualSelfDual/_equivariant/exists_dualModule_smul_ne);
• the B13 unit-filtration bundle for the splitting field k, supplied by the GQ2.dyadicUnitFiltration axiom (already in the census — no new axiom).

The one input that is not derivable is a residue-trivial lift of tame inertia (g₀, hg₀ : ρ g₀ = c tameTau, hg₀rt : IsResidueTrivial (ker ρ) g₀) — the standard local-field fact that tame inertia acts trivially on the residue field (Serre, Local Fields, Ch. IV). The repo works in the spectral-norm vocabulary and carries no residue-field machinery, so this is threaded hypothesis-side here (per the user's decision to keep the assembly axiom-free): the theorem lemma_6_17_dim_of_residueLift is lemma_6_17_dim reduced to exactly that lift plus the standard Galois-correspondence k-plumbing (k/FiniteDimensional/hker, threaded as everywhere in LocalKummer/DeepDualityK).

Axioms: std-3 + B6 (tateDualityAt) + B7 + B11a (hilbertSymbol_normCriterion_finiteDyadic)

• B12 (kummerClassK_surjective) + B13 (dyadicUnitFiltration) — the §6.3 deep-part budget, no new axiom. Closing SectionSix.lemma_6_17_dim outright needs the residue-trivial-lift fact (an axiom-or-infrastructure decision).

theorem GQ2.DimClose.lemma_6_17_dim_of_residueLift {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) [Finite (ContCoh.H1 (↥ρ.ker) (ZMod 2))] (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) [FiniteDimensional ℚ_[2] ↥k] (htriv : ∀ (g : ↥k.fixingSubgroup) (m : ZMod 2), g • m = m) (hker : ∀ (x : Kummer.GaloisGroup ℚ_[2]), x ∈ ρ.ker ↔ x ∈ k.fixingSubgroup) (g₀ : AbsGalQ2) (hg₀ : ρ g₀ = c tameTau) (hg₀rt : IsResidueTrivial ρ.ker g₀) : Nat.card ↑(SectionSix.deepPart ρ) ^ 2 = Nat.card (ContCoh.H1 AbsGalQ2 V)

lemma_6_17_dim, reduced to the residue-trivial tame lift (the deep-part proof finale): the §6.3 deep-half dimension identity #X₊² = #H¹(ℚ₂, V), assembled from f7's hduality_of_data + f8's lemma_6_17_dim_of_hduality, with the single arithmetic input — a residue-trivial lift of tame inertia — threaded as a hypothesis, alongside the standard Galois-correspondence k-plumbing.