Module core of the H_V averaging: (V∨)^C = 0

Split off from GQ2.SectionSeven, building on GQ2.SectionSeven.Prop74Step1. This file reduces the block-module vanishing (V∨)^C = 0 to pure group theory:

• the (F1) odd-order averaging core avg_dual_zero and its bridge, and the (A) simplicity lemma on the Ctil-fixed space;
• the (P1) normal-2-group counting lemmas on V = P/S;
• the unramified and ramified oddness lemmas feeding the H_V averaging.

See GQ2.SectionSeven for the umbrella module docstring.

Module core of the H_V averaging ((V∨)^C = 0)

Two verified bricks that reduce the block-module vanishing to a pure group-theory statement:

• avg_dual_zero (F1) — the odd-order averaging: V^C = 0 ⟹ (V∨)^C = 0.
• fixed_zero_of_moves (A) — simplicity: a Y-normal Ctil that moves V = P/S has V^C = 0, since the Ctil-fixed space fixSub is Y-normal between S and P, so chief forces it to be S.

Together they reduce the block-module vanishing to producing an odd normal Ctil that moves V (the tame construction, discharged by the case split in hv_average_helper).

theorem GQ2.SectionSeven.fixed_zero_of_moves {Y : Type} [Group Y] (S P K Ctil : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (hCtil : Ctil.Normal) (hSP : S ≤ P) (hKP : K ≤ P) (chief : ∀ (X : Subgroup Y), X.Normal → S ≤ X → X ≤ P → X = S ∨ X = P) (hmoves : ∃ p ∈ P, ∃ c ∈ Ctil, c⁻¹ * p * c * p⁻¹ ∉ S) (k : Y) : k ∈ K → (∀ c ∈ Ctil, c⁻¹ * k * c * k⁻¹ ∈ S) → k ∈ S

(A) simplicity: if Ctil ◁ Y moves V = P/S (some c ∈ Ctil moves some p ∈ P off S), the chief condition forces V^Ctil = 0 — any k ∈ K fixed by Ctil mod S lies in S.

theorem GQ2.SectionSeven.L_le_blockPerm_ker {Y : Type} [Group Y] [Finite Y] (S P Lm : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (hL : Lm.Normal) (hSP : S < P) (hPL : P ≤ Lm) (h2L : IsPGroup 2 ↥Lm) (chief : ∀ (X : Subgroup Y), X.Normal → S ≤ X → X ≤ P → X = S ∨ X = P) : Lm ≤ (blockPerm S P hS hP).ker

(P1): a normal 2-group L ⊇ P acts trivially on V = P/S ⟹ L ≤ ker(blockPerm).

theorem GQ2.SectionSeven.dual_vanish_concrete {Y : Type} [Group Y] [Finite Y] (S K Ctil YV : Subgroup Y) (hS : S.Normal) (hK : K.Normal) (_hCtil : Ctil.Normal) (hYVn : YV.Normal) (hcomm : ∀ a ∈ K, ∀ b ∈ K, a * b * a⁻¹ * b⁻¹ ∈ S) (hYVtriv : ∀ z ∈ YV, ∀ k ∈ K, z * k * z⁻¹ * k⁻¹ ∈ S) (hodd : Odd (Nat.card (↥Ctil ⧸ YV.subgroupOf Ctil))) (hfix0 : ∀ k ∈ K, (∀ c ∈ Ctil, c⁻¹ * k * c * k⁻¹ ∈ S) → k ∈ S) (φ : Y → ZMod 2) (hφhom : ∀ k ∈ K, ∀ l ∈ K, φ (k * l) = φ k + φ l) (hφS : ∀ k ∈ K, k ∈ S → φ k = 0) (hφCinv : ∀ c ∈ Ctil, ∀ k ∈ K, φ (c⁻¹ * k * c) = φ k) (k : Y) : k ∈ K → φ k = 0

(F1) bridge (V∨)^Ctil = 0 ⟸ V^Ctil = 0: with K/(K∩S) abelian (hcomm), YV acting trivially (hYVtriv), Ctil/YV odd, and V^Ctil = 0 (hfix0), any Ctil-invariant hom φ : K → 𝔽₂ vanishing on K∩S vanishes on K. Averages φ over Ctil/YV via avg_dual_zero: the fixed vector it produces is nonzero unless φ = 0.

theorem GQ2.SectionSeven.unram_odd {Y : Type} [Group Y] [Finite Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (hSP : S < P) (hP2 : IsPGroup 2 ↥P) (chief : ∀ (X : Subgroup Y), X.Normal → S ≤ X → X ≤ P → X = S ∨ X = P) (hcyc : IsCyclic (Y ⧸ (blockPerm S P hS hP).ker)) : Odd (Nat.card (Y ⧸ (blockPerm S P hS hP).ker))

(unramified) oddness — Y/Y_V (Y_V = ker blockPerm) is odd when it is cyclic and the action on the simple V = P/S is faithful.

theorem GQ2.SectionSeven.cyc_YV {Y : Type u_1} {H : Type u_2} [Group Y] [Finite Y] [Group H] [Finite H] (π : Y →* H) (hπ : Function.Surjective ⇑π) (YV : Subgroup Y) [YV.Normal] (hLYV : π.ker ≤ YV) (s t : H) (hgen : Subgroup.closure {s, t} = ⊤) (htYV : t ∈ Subgroup.map π YV) : IsCyclic (Y ⧸ YV)

theorem GQ2.SectionSeven.top_quot_card {Y : Type u_1} [Group Y] (YV : Subgroup Y) [YV.Normal] : Nat.card (↥⊤ ⧸ YV.subgroupOf ⊤) = Nat.card (Y ⧸ YV)

theorem GQ2.SectionSeven.odd_preimage_quot {Y : Type u_1} {H : Type u_2} [Group Y] [Finite Y] [Group H] (π : Y →* H) (hπ : Function.Surjective ⇑π) (YV : Subgroup Y) (hLYV : π.ker ≤ YV) (t : H) (ht : Odd (orderOf t)) : Odd (Nat.card (↥(Subgroup.comap π (Subgroup.zpowers t)) ⧸ YV.subgroupOf (Subgroup.comap π (Subgroup.zpowers t))))

(ramified) oddness — if π : Y ↠ H has ker π ≤ YV and t : H has odd order, the quotient π⁻¹⟨t⟩ / (YV ∩ π⁻¹⟨t⟩) is odd (a quotient of π⁻¹⟨t⟩ / ker π ≅ ⟨t⟩).