Proposition 7.4: the H_V averaging, step 2, and the simple-head determinant

Split off from GQ2.SectionSeven, building on GQ2.SectionSeven.ModuleCore. This file assembles the genuinely tame tier and concludes Proposition 7.4:

• the H_V averaging (Prop 7.4 step 2 back half) and the tame extension;
• Prop 7.4, step 2 (q_λ|_{T₀} = 0);
• Proposition 7.4 itself (prop_7_4).

See GQ2.SectionSeven for the umbrella module docstring.

theorem GQ2.SectionSeven.prop_7_4 {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} {H : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] (π : Y →* H) (hπ : Function.Surjective ⇑π) (hkerπ : π.ker = L) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (B : MinimalBlock L) (hRN : B.frattiniK.Normal) (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (hlam_conj : ∀ (y r : Y) (hr : r ∈ B.frattiniK), lam ⟨y * r * y⁻¹, ⋯⟩ = lam ⟨r, hr⟩) (hlam_ne : lam ≠ 0) : ∃ (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2), (∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) ∧ qbar ≠ 0 ∧ ∀ (y p : Y) (hp : p ∈ B.P), qbar ↑⟨y * p * y⁻¹, ⋯⟩ = qbar ↑⟨p, hp⟩

Proposition 7.4: for every nonzero Y-invariant functional λ ∈ D_R = (R^∨)^C, the pushout square map of the central extension 1 → 𝔽₂ → K_λ → M → 1 kills T₀ and its polar form kills (T₀, M); hence it descends to a nonzero, nonsingular, Y-invariant quadratic form q̄_λ : V → 𝔽₂ on the simple head V = P/S — the form §8's Gauss sums live on. Stated with the square-map spec λ(k²) = q̄(k mod S) (hsq supplies k² ∈ R, Lemma 7.2's clause, so 7.4 is consumable independently). The framed-target head data (as in lemma_7_2) encode §7's standing hypothesis, under which the paper proves 7.4; its step 2 (q_λ|_{T₀} = 0) consumes H¹(H_V, V^∨) = 0, which needs the tame structure and fails for general finite heads. See docs/section67-extraction.md.]