**Lemma 7.1, head clause** — recorded in its load-bearing form `R ≤ K ∩ S` (the paper's
"Since `K/(K∩S) ≅ V` is elementary abelian, `R ≤ K∩S`; the displayed sequence follows"): given
`gen : K ⊔ S = P`, the exact sequence `0 → T₀ → M → V → 0` and the head identification
`M/T₀ ≅ V` are then the second isomorphism theorem
(`QuotientGroup.quotientInfEquivProdNormalQuotient`), which Mathlib supplies — so the inclusion
is the §7-specific content.  [the §§6–7 statement; proof the §§6–7 proof layer.] 

**Lemma 7.1, radical clause**: `T₀ = (K ∩ S)·R` is the unique maximal `Y`-normal subgroup
of `K` above `R` — i.e. `T₀ = rad_{𝔽₂[C]} M` and `M/T₀` is the unique simple head.
[the §§6–7 statement; proof the §§6–7 proof layer: the head clause collapses the right-hand side to `K ⊓ S`; the
chief dichotomy on `X ⊔ S` then leaves two branches — `= P` dies by `K`'s minimality, `= S`
pins `X = K ⊓ S` by `X`'s maximality (a strict inclusion would force `K ≤ S`, hence `P = S`).
Stated after the head clause, which it consumes.] 

**Lemma 7.1, dual-invariants clause**: `(M^∨)^C = 0` — `K` has no `Y`-normal subgroup of
index 2 above `R` (a nonzero invariant functional on `M` would be its kernel).
[the §§6–7 statement; proof the §§6–7 proof layer — chief-dichotomy on `X ⊔ S` + minimality; the `X ⊔ S = S` branch
pins `|P/S| = 2`, whence the `Y`-action mod `S` is trivial, contradicting `nontrivial_action`.
Finiteness-free.] 

**Lemma 7.2**: for a tame head (the target's head map factors through `GQ2.Ttame`),
`R = Φ(K)` is central elementary abelian in `K`, and `K⁴ = 1`.  [the §§6–7 statement; proof the §§6–7 proof layer
(odd Hall lift + three-subgroup lemma + the `G`-equivariant fourth-power map).] 

**Lemma 7.3 (decorations vanish on the block)**: every homomorphism from `Y` to an
elementary abelian 2-group kills `K` (via Lemma 7.1's dual clause).  The frame decorations
`θ_Y` of `GQ2.MarkedTarget` are such homomorphisms.  [the §§6–7 statement; proof the §§6–7 proof layer: a nonzero
value `f k₀ ≠ 1` yields — through the `𝔽₂`-module structure on `Additive E` and a separating
dual functional — a `C₂`-character of `Y` nontrivial on `K` and killing `R`, whose kernel meets
`K` in a `Y`-normal index-2 subgroup above `R`, contradicting `lemma_7_1_dual`.
Finiteness-free.] 

**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`.] 

**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`.