The parametric lemma_6_17_dim assembly

The capstone card_deepPart_sq_of_duality (GQ2/AdmissibleCount.lean) proves #X₊² = #H¹(ℚ₂,V) — lemma_6_17_dim's exact conclusion — from: hρsurj, hinf, hext, a regular-summand package (ι, r) for the dual module V^∨ = V →+ 𝔽₂, and the graded duality hduality. This file exposes two parametric assembly theorems: one taking both hext and hduality, and one deriving hext internally and taking only hduality.

• profinite plumbing — rho_surjective (ρ = c ∘ tameF is onto), gen_of_surjective (the images of σ, τ generate the finite discrete image, via SectionThree.gen_ttame_quotient), tame_rel_image (the tame relation σ⁻¹τσ = τ² pushed through c, from tame_relation);
• hinf — discharged via the banked inflationVanishes_ramifiedTame;
• the V^∨ package — lemma_6_11_of_tame_pair applied at dualModule, with the 𝔽₂-dual transport bricks dual_faithful / dual_simple / dual_ram proving that V^∨ inherits faithfulness, simplicity, and inertia-nontriviality from V (separation of points by functionals, exists_functional_ne_zero; annihilator + double-dual counting via card_addHom_zmod2 for simplicity).

The second theorem derives FamiliesExtend from the V-side regular-module package using inverse Shapiro and retract transfer. The concrete arithmetic producer for hduality lives in GQ2/DeepCount.lean.

The declarations here use only the standard axioms; B6/B7 enter through the supplied downstream lemmas at instantiation.

Profinite plumbing

theorem GQ2.DimAssembly.rho_surjective {C : Type} [Group C] [TopologicalSpace C] (B : BoundaryMaps) (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) (ρ : AbsGalQ2 →ₜ* C) (hfac : ∀ (g : AbsGalQ2), ρ g = c (B.tameF g)) : Function.Surjective ⇑ρ

ρ = c ∘ tameF is surjective when c is (tameF is onto, B.tameF_surjective).

theorem GQ2.DimAssembly.gen_of_surjective {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] (c : ↑Ttame.toProfinite.toTop →ₜ* C) (hc : Function.Surjective ⇑c) : Subgroup.closure {c tameSigma, c tameTau} = ⊤

The images of σ, τ generate any finite discrete continuous image of T_tame (gen_ttame_quotient; the discrete group is topological for free).

theorem GQ2.DimAssembly.tame_rel_image {C : Type} [Group C] [TopologicalSpace C] (c : ↑Ttame.toProfinite.toTop →ₜ* C) : (c tameSigma)⁻¹ * c tameTau * c tameSigma = c tameTau ^ 2

The tame relation σ⁻¹τσ = τ² in the image (tame_relation pushed through c).

𝔽₂-dual transport: V^∨ inherits the ramified-simple-faithful package from V

Stated in pointwise form (no SMul (V →+ 𝔽₂) instance mentioned), so they can be consumed under any letI := dualModule without instance-diamond friction (the deep-part proof handoff idiom).

theorem GQ2.DimAssembly.eq_of_forall_functional_eq {V : Type} [AddCommGroup V] (hV2 : ∀ (v : V), v + v = 0) {a b : V} (h : ∀ (φ : V →+ ZMod 2), φ a = φ b) : a = b

Functionals separate points (via exists_functional_ne_zero).

theorem GQ2.DimAssembly.dual_faithful {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (hV2 : ∀ (v : V), v + v = 0) (hfaith : ∀ (h : C), (∀ (v : V), h • v = v) → h = 1) (h : C) (hh : ∀ (φ : V →+ ZMod 2) (v : V), φ (h⁻¹ • v) = φ v) : h = 1

Dual faithfulness: if h fixes every functional (pointwise form φ (h⁻¹ • v) = φ v), it is the identity.

theorem GQ2.DimAssembly.dual_ram {C : Type} [Group C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (hV2 : ∀ (v : V), v + v = 0) {t : C} (hram : ∃ (v : V), t • v ≠ v) : ∃ (φ : V →+ ZMod 2) (v : V), φ (t⁻¹ • v) ≠ φ v

Dual inertia-nontriviality: if t moves a vector, it moves a functional (pointwise form).

theorem GQ2.DimAssembly.dual_simple {C : Type} [Group C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (hV2 : ∀ (v : V), v + v = 0) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (W : AddSubgroup (V →+ ZMod 2)) (hW : ∀ (h : C), ∀ φ ∈ W, φ.comp (DistribSMul.toAddMonoidHom V h⁻¹) ∈ W) : W = ⊥ ∨ W = ⊤

Dual simplicity: a C-stable subgroup of V^∨ (stability in composition form) is ⊥ or ⊤. Route: the annihilator in V is C-stable, hence ⊥ by simplicity of V (it cannot be ⊤ unless W = ⊥); then evaluation V ↪ W^∨ is injective and the card_addHom_zmod2 count forces #W = #V^∨.

The parametric close

theorem GQ2.DimAssembly.lemma_6_17_dim_of_hext_hduality {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) [Finite (ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hext : LocalKummer.FamiliesExtend ρ) (hduality : Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker)) = Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker))) : Nat.card ↑(SectionSix.deepPart ρ) ^ 2 = Nat.card (ContCoh.H1 AbsGalQ2 V)

lemma_6_17_dim, parametric over hext and hduality (the deep-part proof, increment 1): from lemma_6_17_dim's own hypothesis set, discharge hρsurj/hgen/hinf (profinite plumbing + inflationVanishes_ramifiedTame) and the V^∨ regular-summand package (lemma_6_11_of_tame_pair at dualModule, via the 𝔽₂-dual transport bricks), and apply the f6 capstone. The parameters are hext (FamiliesExtend) and hduality (the deep-part proof's result).

theorem GQ2.DimAssembly.lemma_6_17_dim_of_hduality {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) [Finite (ContCoh.H1 (↥ρ.ker) (ZMod 2))] (hduality : Nat.card ↥(equivHoms C (V →+ ZMod 2) ↥(deepClassesSubgroup ρ.ker)) = Nat.card ↥(equivHoms C (V →+ ZMod 2) (ContCoh.H1 (↥ρ.ker) (ZMod 2) ⧸ deepClassesSubgroup ρ.ker))) : Nat.card ↑(SectionSix.deepPart ρ) ^ 2 = Nat.card (ContCoh.H1 AbsGalQ2 V)

lemma_6_17_dim, parametric over hduality alone (the deep-part proof, increment 2): the hext parameter of lemma_6_17_dim_of_hext_hduality is now discharged — the V-side regular-summand package (lemma_6_11_of_tame_pair at V itself, whose hypotheses are the theorem's own) feeds ShapiroExtend.familiesExtend_of_package (inverse Shapiro at the regular module + the retract transfer). The final parameter is the deep-part duality hypothesis hduality.