§7: a minimal nontrivial module layer in the wild kernel — statements

Statement-first extraction of the paper's §7 (pages 37–38): the group-theoretic block structure that §8 fixes ("For the simple-head block fixed in section 7, write T = T₀"). This file is now a thin umbrella: the content lives in the GQ2/SectionSeven/ sub-modules imported above (Basic, Decorations, Prop74Step1, ModuleCore, Prop74). Every statement carries its paper reference; all are proved.

The paper's setup and its encoding

For a framed target G (here Y, cf. GQ2.MarkedTarget) with marked normal 2-subgroup L and tame quotient H, suppose not every chief factor of L is a trivial (scalar) module; choose

• S ◁ P ◁ G, P ≤ L, with all chief factors below S trivial and V = P/S the first nontrivial simple factor;
• K ◁ G, K ≤ P, minimal subject to KS = P; and put R = Φ(K) = K²[K,K], M = K/R, T₀ = (K ∩ S)/R, C = G/K.

Encodings (docs/section67-extraction.md §7):

• Everything is phrased at the level of subgroups of Y (normality in Y = the module condition), avoiding quotient-module instances; the quotients M, V appear only where the paper's claims are irreducibly about them (lemma_7_1_head, prop_7_4), via subgroup quotients ↥K ⧸ ….
• "All chief factors trivial" is IsScalarStack: a normal chain from ⊥ with G-commutators dropping one level (⁅y, x⁆ ∈ cᵢ for x ∈ cᵢ₊₁) — for a finite 2-group this is exactly "every chief factor is the trivial 𝔽₂-module".
• R = Φ(K) is the subgroup generated by squares and commutators of K (frattiniLike).
• Tameness of the head (used by 7.2/7.4) is carried as a marked surjection from GQ2.Ttame (GQ2/BoundaryFrame.lean), matching the frame's α.
• The dual-invariants clause (M^∨)^C = 0 of Lemma 7.1 is stated as: K has no Y-normal subgroup of index 2 above R (nonzero invariant functionals ↔ such subgroups).

Axioms: none (statement layer).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 7.1 = ⟦lem-simplehead⟧
• Lemma 7.2 = ⟦lem-collapse⟧
• Lemma 7.3 = ⟦lem-decorationblock⟧
• Proposition 7.4 = ⟦prop-simpleheaddet⟧