Proposition 7.4, step 1 and the averaging machinery

Split off from GQ2.SectionSeven, building on GQ2.SectionSeven.Decorations. This file provides the abstract-block tier of Proposition 7.4:

• Prop 7.4, step 1 (b_λ(T₀, M) = 0) and its dual-invariants endgame;
• the odd averaging (odd_average) and the σ₀-extension of a hom K ∩ S → 𝔽₂;
• the quotient averaging (the H_V-analogue of odd_average).

See GQ2.SectionSeven for the umbrella module docstring.

Proposition 7.4 (simple-head determinant)

The proof layer splits the paper's argument into an abstract-block tier (everything except step 2) and the genuinely tame step 2 (q_λ|_{T₀} = 0), which needs H¹(H_V, V^∨) = 0 for the head's action image and is therefore stated with the framed-target head data (the §§6–7 proof layer amendment: the §§6–7 statement had dropped §7's standing framed-target hypothesis, under which the paper proves 7.4 — restored here; see docs/section67-extraction.md).

theorem GQ2.SectionSeven.sq_mem_R {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) {k : Y} (hk : k ∈ B.K) : k * k ∈ B.frattiniK

Squares of K generate into R = Φ(K).

theorem GQ2.SectionSeven.comm_mem_R {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) {k l : Y} (hk : k ∈ B.K) (hl : l ∈ B.K) : k * l * k⁻¹ * l⁻¹ ∈ B.frattiniK

Commutators of K generate into R = Φ(K).

theorem GQ2.SectionSeven.lam_comm_vanish {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) (hRN : B.frattiniK.Normal) (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⟩) (k : Y) : k ∈ B.K → ∀ t ∈ B.K ⊓ B.S, ∀ (h : k * t * k⁻¹ * t⁻¹ ∈ B.frattiniK), lam ⟨k * t * k⁻¹ * t⁻¹, h⟩ = 0

Prop 7.4, step 1 (b_λ(T₀, M) = 0): a Y-invariant additive λ : R → 𝔽₂ kills every commutator [k, t], k ∈ K, t ∈ K ∩ S. Abstract-block proof (no tame input) — the paper's socle argument run at subgroup level: the right kernel T of the pairing (k, t) ↦ λ([k, t]) is a Y-normal subgroup; were some t₀ ∈ K ∩ S outside it, the scalar-stack chain of S intersected with K ∩ S would have a first layer ⊄ T, and any t* there has all its Y-commutators inside T — making k ↦ λ([k, t*]) a nonzero Y-invariant functional on K killing R, whose kernel is a Y-normal index-2 subgroup of K above R, contradicting lemma_7_1_dual.

theorem GQ2.SectionSeven.invariant_hom_absurd {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) (ψ : Y → ZMod 2) (hψhom : ∀ k ∈ B.K, ∀ l ∈ B.K, ψ (k * l) = ψ k + ψ l) (hψinv : ∀ (y k : Y), k ∈ B.K → ψ (y * k * y⁻¹) = ψ k) (t₀ : Y) (ht₀K : t₀ ∈ B.K) (ht₀ : ψ t₀ ≠ 0) : False

Endgame for Prop 7.4 step 2 (the (K/R)^{∨ Y} = 0 clause, = lemma_7_1_dual): a Y-invariant group homomorphism ψ : K → 𝔽₂ that is nonzero somewhere on K is impossible. Such a ψ automatically kills R = Φ(K) (squares and commutators die in 𝔽₂), so its kernel is a Y-normal index-2 subgroup of K above R, contradicting lemma_7_1_dual. This is the abstract-block back half of step 2; the tame front half (key_extension) supplies the ψ.

theorem GQ2.SectionSeven.sigma0_extends {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) (σ : Y → ZMod 2) (hσhom : ∀ k ∈ B.K ⊓ B.S, ∀ l ∈ B.K ⊓ B.S, σ (k * l) = σ k + σ l) (hσR : ∀ r ∈ B.frattiniK, σ r = 0) : ∃ (σ₀ : Y → ZMod 2), (∀ k ∈ B.K, ∀ l ∈ B.K, σ₀ (k * l) = σ₀ k + σ₀ l) ∧ ∀ k ∈ B.K ⊓ B.S, σ₀ k = σ k

The σ₀ extension: a hom σ : K ∩ S → 𝔽₂ killing R extends to a hom σ₀ : K → 𝔽₂. Via K/R as an 𝔽₂-vector space and LinearMap.exists_extend.

theorem GQ2.SectionSeven.quotient_average {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : MinimalBlock L) (YV Ctil : Subgroup Y) (hYVn : YV.Normal) (hCtiln : Ctil.Normal) (hodd : Odd (Nat.card (↥Ctil ⧸ YV.subgroupOf Ctil))) (σ₀ : Y → ZMod 2) (hσ₀hom : ∀ k ∈ B.K, ∀ l ∈ B.K, σ₀ (k * l) = σ₀ k + σ₀ l) (hσ₀KSinv : ∀ k ∈ B.K ⊓ B.S, ∀ (y : Y), σ₀ (y * k * y⁻¹) = σ₀ k) (hσ₀YV : ∀ k ∈ B.K, ∀ z ∈ YV, σ₀ (z * k * z⁻¹) = σ₀ k) (hVC : ∀ (φ : Y → ZMod 2), (∀ k ∈ B.K, ∀ l ∈ B.K, φ (k * l) = φ k + φ l) → (∀ k ∈ B.K ⊓ B.S, φ k = 0) → (∀ c ∈ Ctil, ∀ k ∈ B.K, φ (c⁻¹ * k * c) = φ k) → ∀ k ∈ B.K, φ k = 0) : ∃ (ψ : Y → ZMod 2), (∀ k ∈ B.K, ∀ l ∈ B.K, ψ (k * l) = ψ k + ψ l) ∧ (∀ (y k : Y), k ∈ B.K → ψ (y * k * y⁻¹) = ψ k) ∧ ∀ k ∈ B.K ⊓ B.S, ψ k = σ₀ k

Quotient averaging (the H_V-analogue of odd_average): average a Y_V-invariant hom σ₀ over the odd quotient C̃/Y_V. With (V∨)^C = 0 (any C̃-conj-invariant hom K→𝔽₂ vanishing on K∩S is 0), the average is a Y-invariant hom extending σ₀|_{K∩S}.