Stage §7 — A minimal non-scalar module layer in the wild kernel (manuscript sec:block)

This file builds the §7 block machinery (reference/q2_manuscript.tex, sec:block, l.3597–3771) that founds the nonterminal Fourier branch Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch of Induction/Recursion.lean. Given a boundary-framed target whose marked 2-kernel L_Y has a non-scalar chief factor, §7 isolates:

• the minimal non-scalar layer S ◁ P ≤ L_Y, the minimal Y-normal K ≤ P with KS = P, and R = Φ(K), M = K/R, T = (K∩S)/R, with simple head V = M/T (lem:simplehead, l.3658; lem:collapse, l.3677; lem:decorationblock, l.3710);
• the determinant character space 𝒳_R = (R^∨)^B = (R^∨)^C, canonically the dual of the obstruction space O_R (lem:obstructionseparation, l.4213: 𝒳_R = Ŵ, W = O_R = (𝒳_R)^∨), and the lift-torsor exponent/size dimExp = 2·dim R, zR = 2^{dimExp}·|𝒳_R| = 2^{dimExp}·|Ŵ| (prop:finalfourier, z_R = 2^{2 dim R + dim 𝒳_R});
• the determinant pushout on the simple head (prop:simpleheaddet, l.3730): for 0 ≠ λ ∈ 𝒳_R, the square map q_λ of the central pushout K_λ = K/ker λ satisfies q_λ|_T = 0, b_λ(T, M) = 0, hence descends to a nonzero nonsingular C-invariant quadratic form q̄_λ : V → 𝔽₂.

Decomposition: proven vs. isolated

The abstract algebra is genuinely proven, sorry-free:

• Part 1 (Annihilates/descend): the pure 𝔽₂-linear-algebra heart of prop:simpleheaddet — a QuadF2 M that annihilates a submodule T (q.form|_T = 0, q.polar(T,·) = 0) descends to a QuadF2 (M ⧸ T), and the descended form is nonsingular exactly when the polar radical of q lies in T. This is the descent of prop:simpleheaddet over the exact sequence 0 → T → M → V → 0 of lem:simplehead, reusing Quadratic.QuadF2.
• Part 2/3 (MinimalBlock): the §7 block packaged as data, with the determinant character space 𝒳_R = (R^∨)^C (= Ŵ) constructed from R and the C-action and the obstruction space W = O_R := Module.Dual 𝒳_R, the exponent dimExp = 2·dim R and size zR = 2^{dimExp}·|Ŵ| in exactly the shape FourierBranchData.hzR consumes (zR_eq_fintype), and the determinant pushout family; prop:simpleheaddet (the descended nonzero, nonsingular, C-invariant head form headForm) is proven on top of Part 1.

The genuinely deep finite-group / representation-theoretic inputs of §7 — the existence of the minimal non-scalar configuration (chief series + minimality of K), the Frattini–centralizer collapse lem:collapse (R central elementary abelian, K^4 = 1, via the odd Hall-lift coprime action + three-subgroup lemma), the radical identification T = rad_{𝔽₂[C]} M and (M^∨)^C = 0 of lem:simplehead, and the cohomology vanishing H¹(H_V, V^∨) = 0 used in prop:simpleheaddet — are isolated as documented fields of MinimalBlock (the "genuine local inputs"), exactly as FourierBranchData isolates the pre-Fourier obstruction realization. The block's existence for a non-scalar target is the single bridge axiom minimalBlock_of_nonScalar. See the closing report for the precise §8/bridge decomposition handed to the follow-up agents.

Part 1 — Abstract 𝔽₂ quadratic descent (the algebra of prop:simpleheaddet)

The simple-head determinant proposition says that the square map q_λ : M → 𝔽₂ of the central pushout K_λ annihilates the radical T (both q_λ|_T = 0 and b_λ(T, M) = 0), so it descends to a quadratic form on the head V = M/T, which is nonsingular because the polar radical is exactly T. This Part proves that descent abstractly for any QuadF2 over 𝔽₂ — pure linear algebra, sorry-free.

structure Q2Presentation.Induction.Annihilates {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (q : Quadratic.QuadF2 M) (T : Submodule (ZMod 2) M) : Prop

A QuadF2 M annihilates the submodule T when its quadratic map vanishes on T and its polar form kills T against all of M. These are exactly the two conclusions q_λ|_T = 0 and b_λ(T, M) = 0 of prop:simpleheaddet.

• form_zero_on (t : M) : t ∈ T → q.form t = 0

  q_λ|_T = 0.

• polar_zero_on (t : M) : t ∈ T → ∀ (m : M), (q.polar t) m = 0

  b_λ(T, M) = 0.

theorem Q2Presentation.Induction.Annihilates.form_add_mem {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (m : M) {t : M} (ht : t ∈ T) : q.form (m + t) = q.form m

The quadratic map is constant on T-cosets (q(m + t) = q(m) for t ∈ T): this is what makes q descend to M / T.

theorem Q2Presentation.Induction.Annihilates.form_eq_of_sub_mem {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) {a b : M} (hab : a - b ∈ T) : q.form a = q.form b

Equal quadratic values on T-congruent vectors.

def Q2Presentation.Induction.Annihilates.descendForm {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) : M ⧸ T → ZMod 2

The descended quadratic map q̄ : M / T → 𝔽₂, q̄(m + T) = q(m) (well-defined by form_add_mem).

Equations

• h.descendForm x = Quotient.liftOn' x q.form ⋯

@[simp]

theorem Q2Presentation.Induction.Annihilates.descendForm_mk {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (m : M) : h.descendForm (Submodule.Quotient.mk m) = q.form m

def Q2Presentation.Induction.Annihilates.descendPolar {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) : M ⧸ T →ₗ[ZMod 2] M ⧸ T →ₗ[ZMod 2] ZMod 2

The descended polar form b̄ : (M / T) × (M / T) → 𝔽₂, descended from q.polar (which kills T on both sides), via LinearMap.liftQ₂.

Equations

• h.descendPolar = LinearMap.liftQ₂ T T q.polar ⋯ ⋯

@[simp]

theorem Q2Presentation.Induction.Annihilates.descendPolar_mk {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (m m' : M) : (h.descendPolar (Submodule.Quotient.mk m)) (Submodule.Quotient.mk m') = (q.polar m) m'

def Q2Presentation.Induction.Annihilates.descend {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) : Quadratic.QuadF2 (M ⧸ T)

The descended quadratic form q̄ : QuadF2 (M / T) of prop:simpleheaddet: the square map of the pushout descends to the simple head, with polar form the descended commutator pairing.

Equations

• h.descend = { form := h.descendForm, polar := h.descendPolar, form_zero := ⋯, form_add := ⋯ }

@[simp]

theorem Q2Presentation.Induction.Annihilates.descend_form_mk {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (m : M) : h.descend.form (Submodule.Quotient.mk m) = q.form m

@[simp]

theorem Q2Presentation.Induction.Annihilates.descend_polar_mk {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (m m' : M) : (h.descend.polar (Submodule.Quotient.mk m)) (Submodule.Quotient.mk m') = (q.polar m) m'

theorem Q2Presentation.Induction.Annihilates.descend_nonsingular {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] {q : Quadratic.QuadF2 M} {T : Submodule (ZMod 2) M} (h : Annihilates q T) (hrad : ∀ (m : M), (∀ (m' : M), (q.polar m) m' = 0) → m ∈ T) : h.descend.Nonsingular

Nonsingularity of the descended form (prop:simpleheaddet, last paragraph): if the polar radical of q lies inside T (every vector orthogonal to all of M already lies in T), then the descended form q̄ on V = M / T is nonsingular. For the simple head this is automatic since T is the polar radical.

Smart-constructor toolkit: the pushout square map is the proven extraspecial form

The manuscript's central-pushout square map q_λ(m) = λ(m̃²) (l.3724) is the class-2 Heisenberg square diagonal Quadratic.Extraspecial.extraspecialForm φ_λ — form c = φ_λ(c)(c), polar the commutator pairing bcl (extraspecialForm_eq_heisSquare, extraspecialForm_polar_eq_bcl, both proven in Quadratic/GaussSign.lean) — for the self-duality φ_λ : M → M^∨ of the pushout. These three helpers discharge the MinimalBlock.pushout_* fields from φ_λ, so a block can take pushout λ := extraspecialForm φ_λ and the pushout field is the genuine manuscript object, not an opaque black box. (Over 𝔽₂ the polar of extraspecialForm φ is the symmetrized pairing φ m m' + φ m' m, so the hypotheses are stated on that.)

theorem Q2Presentation.Induction.extraspecial_annihilates {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (T : Submodule (ZMod 2) M) (φ : M →ₗ[ZMod 2] Module.Dual (ZMod 2) M) (hform : ∀ t ∈ T, (φ t) t = 0) (hpolar : ∀ t ∈ T, ∀ (m : M), (φ t) m + (φ m) t = 0) : Annihilates (Quadratic.Extraspecial.extraspecialForm φ) T

The extraspecial square map annihilates T (prop:simpleheaddet(1,2)) when its self-duality φ has φ|_T diagonal-zero and T-symmetrically-orthogonal.

theorem Q2Presentation.Induction.extraspecial_radical_subset {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (T : Submodule (ZMod 2) M) (φ : M →ₗ[ZMod 2] Module.Dual (ZMod 2) M) (hrad : ∀ (m : M), (∀ (m' : M), (φ m) m' + (φ m') m = 0) → m ∈ T) (m : M) : (∀ (m' : M), ((Quadratic.Extraspecial.extraspecialForm φ).polar m) m' = 0) → m ∈ T

The extraspecial polar radical lands in T (prop:simpleheaddet nonsingularity input) when the symmetrized pairing of φ has radical ⊆ T.

theorem Q2Presentation.Induction.extraspecial_nonzero {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (φ : M →ₗ[ZMod 2] Module.Dual (ZMod 2) M) (hnz : ∃ (m : M), (φ m) m ≠ 0) : ∃ (m : M), (Quadratic.Extraspecial.extraspecialForm φ).form m ≠ 0

The extraspecial descended form is nonzero (prop:simpleheaddet) when the diagonal of φ is nonzero somewhere.

Part 2 — The §7 minimal non-scalar block as data (manuscript sec:block)

The block is packaged as a structure MinimalBlock p, parallel to FourierBranchData p of Induction/Recursion.lean. It carries the module-level outputs of the §7 tower Y ↠ B ↠ C ↠ H and the exact sequence 0 → T → M → V → 0 (eq:targettower):

• the central elementary-abelian Frattini quotient R = Φ(K) (an 𝔽₂-space by lem:collapse), with the C = Y/K action actR;
• the elementary module layer M = K/R with its C-action actM and the radical submodule T = (K∩S)/R; the simple head is V = M/T (lem:simplehead);
• the deep lem:simplehead/lem:collapse/cohomology inputs as documented fields (dualInv_zero for (M^∨)^C = 0; the pushout_* fields for prop:simpleheaddet).

From this data, Part 3 constructs and proves W = O_R = (R^∨)^C, dimExp, zR and the descended nonzero nonsingular head form headForm (prop:simpleheaddet).

structure Q2Presentation.Induction.MinimalBlock (p : FramedPair) : Type 1

The §7 minimal non-scalar block. Source-uniform module-level data of the manuscript tower (eq:targettower), with the deep group/representation inputs of lem:simplehead/lem:collapse/prop:simpleheaddet isolated as documented fields.

• nonScalar : ¬ScalarTerminal p

  §7 entry condition: the target is not scalar-terminal — L_Y has a non-scalar chief factor (sec:block, l.3616). A MinimalBlock exists only for a genuinely non-scalar target, so this ties the block to p (Nonempty (MinimalBlock p) characterizes non-scalarity, nonempty_minimalBlock_iff).

• R : Type

  The central elementary-abelian Frattini quotient R = Φ(K) (lem:collapse: an 𝔽₂-vector space, since R is central of exponent 2 in K).

• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type

  The elementary module layer M = K/R (lem:simplehead).

• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M

  The radical submodule T = (K∩S)/R ◁ M (lem:simplehead: T = rad_{𝔽₂[C]} M).

• C : Type

  The lower target C = Y/K (eq:targettower), acting 𝔽₂-linearly on R and M.

• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R

  The C-action on R (used to cut out the invariants 𝒳_R = (R^∨)^C).

• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M

  The C-action on M (the 𝔽₂[C]-module structure of lem:simplehead).

• head_nontrivial : Nontrivial (self.M ⧸ self.T)

  Non-vacuity of the simple head: V = M/T is a genuine nonzero simple head, not the zero quotient. This is part of lem:simplehead; without it the current interface admits a one-point dummy block whose determinant conditions are all vacuous.

• exists_nonzero_invariant : ∃ (lam : Module.Dual (ZMod 2) self.R), lam ≠ 0 ∧ ∀ (c : self.C), lam ∘ₗ ↑(self.actR c) = lam

  Non-vacuity of the determinant character space: 𝒳_R = (R^∨)^C contains a nonzero character. This is the character 0 ≠ λ ∈ 𝒳_R ranged over in prop:simpleheaddet and the §8 Fourier sum.

• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T

  T is a C-submodule, so the head V = M/T inherits a C-action.

• dualInv_zero (φ : Module.Dual (ZMod 2) self.M) : (∀ (c : self.C), φ ∘ₗ ↑(self.actM c) = φ) → φ = 0

  lem:simplehead: (M^∨)^C = 0 — the unique simple head is the nontrivial simple module V, so no C-equivariant functional M → 𝔽₂ survives. (A documented representation-theoretic input, fed to the §8 cover construction.)

• pushout : Module.Dual (ZMod 2) self.R → Quadratic.QuadF2 self.M

  The central-pushout square map q_λ : M → 𝔽₂ of K_λ = K/ker λ, for λ ∈ R^∨ (manuscript l.3724; realised by Quadratic.Extraspecial.extraspecialForm).

• pushout_annih (lam : Module.Dual (ZMod 2) self.R) : lam ≠ 0 → (∀ (c : self.C), lam ∘ₗ ↑(self.actR c) = lam) → Annihilates (self.pushout lam) self.T

  prop:simpleheaddet(1,2): for 0 ≠ λ ∈ 𝒳_R, q_λ|_T = 0 and b_λ(T, M) = 0. (From Hom_C(T, M^∨) = 0 and the cohomology-vanishing shear argument; documented.)

• pushout_radical (lam : Module.Dual (ZMod 2) self.R) : lam ≠ 0 → (∀ (c : self.C), lam ∘ₗ ↑(self.actR c) = lam) → ∀ (m : self.M), (∀ (m' : self.M), ((self.pushout lam).polar m) m' = 0) → m ∈ self.T

  prop:simpleheaddet (nonsingularity): the polar radical of q_λ is exactly T (every M-orthogonal vector lies in T), so the descended head form is nonsingular. (From Φ(K_λ) = R/ker λ ≠ 1 + simplicity of V; documented.)

• pushout_nonzero (lam : Module.Dual (ZMod 2) self.R) : lam ≠ 0 → (∀ (c : self.C), lam ∘ₗ ↑(self.actR c) = lam) → ∃ (m : self.M), (self.pushout lam).form m ≠ 0

  prop:simpleheaddet (nonzero): the descended head form is nonzero (K_λ is not elementary abelian, Φ(K_λ) ≠ 1); documented.

• pushout_invariant (lam : Module.Dual (ZMod 2) self.R) : lam ≠ 0 → (∀ (c : self.C), lam ∘ₗ ↑(self.actR c) = lam) → ∀ (c : self.C) (m : self.M), (self.pushout lam).form ((self.actM c) m) = (self.pushout lam).form m

  prop:simpleheaddet (C-invariance): for 0 ≠ λ ∈ 𝒳_R, the square map q_λ is C-invariant (λ ∈ (R^∨)^C and the pushout is natural in C). Combined with T_stable this makes the descended head form a C-invariant quadratic form on V (manuscript: a "nonzero nonsingular C-invariant quadratic form q̄_λ"). Documented.

@[reducible, inline]

abbrev Q2Presentation.Induction.MinimalBlock.head {p : FramedPair} (B : MinimalBlock p) : Type

The simple head V = M / T (lem:simplehead: M/T ≅ V, the first non-scalar simple factor); the exact sequence 0 → T → M → V → 0 is T.subtype/T.mkQ.

Equations

• B.head = (B.M ⧸ B.T)

def Q2Presentation.Induction.MinimalBlock.XR {p : FramedPair} (B : MinimalBlock p) : Submodule (ZMod 2) (Module.Dual (ZMod 2) B.R)

The determinant character space 𝒳_R = (R^∨)^C (manuscript l.3722/l.4211: 𝒳_R = (R^∨)^B = (R^∨)^C): the C-invariants of the dual of R, cut out as a genuine 𝔽₂-submodule of Module.Dual (ZMod 2) R. By lem:obstructionseparation (l.4213) this is canonically Ŵ, the character group of the obstruction space O_R = obstructionSpace; prop:simpleheaddet and the §8 Fourier inversion both range over 0 ≠ λ ∈ 𝒳_R (= ↥XR).

Equations

• B.XR = { carrier := {χ : Module.Dual (ZMod 2) B.R | ∀ (c : B.C), χ ∘ₗ ↑(B.actR c) = χ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

instance Q2Presentation.Induction.MinimalBlock.instFiniteDualR {p : FramedPair} (B : MinimalBlock p) : Finite (Module.Dual (ZMod 2) B.R)

instance Q2Presentation.Induction.MinimalBlock.instFiniteXR {p : FramedPair} (B : MinimalBlock p) : Finite ↥B.XR

theorem Q2Presentation.Induction.MinimalBlock.exists_nonzero_XR {p : FramedPair} (B : MinimalBlock p) : ∃ (lam : ↥B.XR), lam ≠ 0

The determinant character space 𝒳_R has a nonzero character. This is the Lean-facing non-vacuity witness used by the §7/§8 interface.

@[reducible, inline]

abbrev Q2Presentation.Induction.MinimalBlock.obstructionSpace {p : FramedPair} (B : MinimalBlock p) : Type

The R-valued obstruction space W = O_R (prop:finalfourier). By lem:obstructionseparation (l.4213, 𝒳_R = (R^∨)^B = (R^∨)^C is canonically the dual of the R-valued obstruction space), O_R = (𝒳_R)^∨, so O_R = Module.Dual (ZMod 2) 𝒳_R. This is the finite 𝔽₂ space FourierBranchData.W the §8 Fourier branch consumes: the R-valued lifting obstruction o_Γ lands in O_R, and its character group Ŵ = Dual O_R ≅ 𝒳_R is the index of the Fourier sum eq:recursionR1.

Equations

• B.obstructionSpace = Module.Dual (ZMod 2) ↥B.XR

instance Q2Presentation.Induction.MinimalBlock.instFiniteObstruction {p : FramedPair} (B : MinimalBlock p) : Finite B.obstructionSpace

def Q2Presentation.Induction.MinimalBlock.dimExp {p : FramedPair} (B : MinimalBlock p) : ℕ

dimExp = 2·dim R (manuscript: the lift-torsor exponent 2 dim R, prop:finalfourier, z_R = 2^{2 dim R + dim 𝒳_R}).

Equations

• B.dimExp = 2 * Module.finrank (ZMod 2) B.R

def Q2Presentation.Induction.MinimalBlock.zR {p : FramedPair} (B : MinimalBlock p) : ℕ

zR = 2^{2 dim R}·|𝒳_R| = 2^{dimExp}·|Ŵ| (manuscript prop:finalfourier, z_R = |Z¹_{Γ,ρ}(R)| = 2^{2 dim R + dim 𝒳_R}, l.4244). Since 𝒳_R = Ŵ is the character group of W = O_R, this is exactly the value FourierBranchData.hzR demands for the common lift-torsor size.

Equations

• B.zR = 2 ^ B.dimExp * Nat.card (Module.Dual (ZMod 2) B.obstructionSpace)

instance Q2Presentation.Induction.MinimalBlock.instFiniteObstructionDual {p : FramedPair} (B : MinimalBlock p) : Finite (Module.Dual (ZMod 2) B.obstructionSpace)

noncomputable instance Q2Presentation.Induction.MinimalBlock.instFintypeObstructionDual {p : FramedPair} (B : MinimalBlock p) : Fintype (Module.Dual (ZMod 2) B.obstructionSpace)

Equations

• B.instFintypeObstructionDual = Fintype.ofFinite (Module.Dual (ZMod 2) B.obstructionSpace)

theorem Q2Presentation.Induction.MinimalBlock.dimExp_eq {p : FramedPair} (B : MinimalBlock p) : B.dimExp = 2 * Module.finrank (ZMod 2) B.R

dimExp is 2·dim R (the manuscript exponent), by definition.

theorem Q2Presentation.Induction.MinimalBlock.zR_eq {p : FramedPair} (B : MinimalBlock p) : B.zR = 2 ^ B.dimExp * Nat.card (Module.Dual (ZMod 2) B.obstructionSpace)

zR is 2^{dimExp}·|Ŵ| with Ŵ = Dual (O_R), O_R = obstructionSpace (manuscript z_R = 2^{2 dim R + dim 𝒳_R}; Ŵ ≅ 𝒳_R, so the value is 2^{2 dim R}·|𝒳_R|).

theorem Q2Presentation.Induction.MinimalBlock.zR_eq_fintype {p : FramedPair} (B : MinimalBlock p) : B.zR = 2 ^ B.dimExp * Fintype.card (Module.Dual (ZMod 2) B.obstructionSpace)

zR in exactly FourierBranchData.hzR's shape (Fintype.card, not just Nat.card). Setting FourierBranchData.W := obstructionSpace (= O_R), the §8 agent gets hzR : zR = 2^{dimExp}·|Ŵ| directly from this, with Ŵ = Module.Dual W.

Part 3 — prop:simpleheaddet assembled: the descended head form headForm

theorem Q2Presentation.Induction.MinimalBlock.coe_ne_zero {p : FramedPair} (B : MinimalBlock p) {lam : ↥B.XR} (hlam : lam ≠ 0) : ↑lam ≠ 0

A nonzero C-invariant λ ∈ 𝒳_R has nonzero underlying functional λ ∈ R^∨.

theorem Q2Presentation.Induction.MinimalBlock.annih_of {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) : Annihilates (B.pushout ↑lam) B.T

The prop:simpleheaddet Annihilates witness for 0 ≠ λ ∈ 𝒳_R.

def Q2Presentation.Induction.MinimalBlock.headForm {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) : Quadratic.QuadF2 B.head

prop:simpleheaddet — the simple-head determinant form q̄_λ : V → 𝔽₂. For 0 ≠ λ ∈ 𝒳_R, the central-pushout square map q_λ (which annihilates T by prop:simpleheaddet(1,2)) descends to a quadratic form on the simple head V = M/T.

Equations

• B.headForm lam hlam = ⋯.descend

@[simp]

theorem Q2Presentation.Induction.MinimalBlock.headForm_form_mk {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) (m : B.M) : (B.headForm lam hlam).form (Submodule.Quotient.mk m) = (B.pushout ↑lam).form m

def Q2Presentation.Induction.MinimalBlock.headAut {p : FramedPair} (B : MinimalBlock p) (c : B.C) : B.head →ₗ[ZMod 2] B.head

The induced C-action on the simple head V = M/T: T_stable makes T a C-submodule, so actM c descends to V (headAut c (m + T) = (actM c) m + T).

Equations

• B.headAut c = B.T.mapQ B.T ↑(B.actM c) ⋯

@[simp]

theorem Q2Presentation.Induction.MinimalBlock.headAut_mk {p : FramedPair} (B : MinimalBlock p) (c : B.C) (m : B.M) : (B.headAut c) (Submodule.Quotient.mk m) = Submodule.Quotient.mk ((B.actM c) m)

theorem Q2Presentation.Induction.MinimalBlock.headForm_invariant {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) (c : B.C) (v : B.head) : (B.headForm lam hlam).form ((B.headAut c) v) = (B.headForm lam hlam).form v

prop:simpleheaddet (C-invariance), proven: the descended head form q̄_λ is invariant under the induced C-action headAut on V, from pushout_invariant + T_stable. This is the third prop:simpleheaddet conclusion ("nonzero nonsingular C-invariant quadratic form q̄_λ").

theorem Q2Presentation.Induction.MinimalBlock.headForm_nonsingular {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) : (B.headForm lam hlam).Nonsingular

prop:simpleheaddet (nonsingularity): the descended head form q̄_λ is nonsingular (its polar form is perfect on V).

theorem Q2Presentation.Induction.MinimalBlock.headForm_ne_zero {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) : ∃ (v : B.head), (B.headForm lam hlam).form v ≠ 0

prop:simpleheaddet (nonzero): the descended head form q̄_λ is nonzero (Φ(K_λ) ≠ 1), so it is a genuine nonsingular quadratic form on the simple head.

theorem Q2Presentation.Induction.MinimalBlock.simpleHeadDet {p : FramedPair} (B : MinimalBlock p) (lam : ↥B.XR) (hlam : lam ≠ 0) : (B.headForm lam hlam).Nonsingular ∧ (∃ (v : B.head), (B.headForm lam hlam).form v ≠ 0) ∧ ∀ (c : B.C) (v : B.head), (B.headForm lam hlam).form ((B.headAut c) v) = (B.headForm lam hlam).form v

prop:simpleheaddet, packaged: for every 0 ≠ λ ∈ 𝒳_R the simple head V carries a nonzero, nonsingular, C-invariant quadratic form q̄_λ — exactly the three manuscript conclusions (l.3737–3741). This determinant-pushout output is consumed by the §8 central-cover / phase-class construction.

Part 4 — The §7 block existence bridge (the single isolated §7 axiom)

The construction of the minimal non-scalar block from a non-terminal target is the genuinely deep finite-group theory of sec:block: the existence of the chief-series configuration S ◁ P ≤ L_Y, the minimal K, and the Frattini–centralizer collapse lem:collapse. These are not finite linear algebra; they are isolated here as the single §7 bridge axiom, strictly more atomic than the monolith boundaryFramed_nonterminal_fourier_branch (which additionally requires the §8 central-cover / Fourier data).

axiom Q2Presentation.Induction.minimalBlock_of_nonScalar (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

AXIOM (the §7 block bridge, sec:block). A boundary-framed target that is not scalar-terminal — i.e. whose marked 2-kernel L_Y has a non-scalar chief factor — admits a minimal non-scalar block. This isolates only the deep finite-group existence of sec:block: the chief-series choice S ◁ P ≤ L_Y with first non-scalar simple factor V, the minimal Y-normal K ≤ P with KS = P, and the Frattini–centralizer collapse lem:collapse (R = Φ(K) central elementary abelian, K^4 = 1). The module-level consequences (lem:simplehead's exact sequence and the descent of prop:simpleheaddet) are then proven from the block (Part 1/3). To be discharged by future formalization of the sec:block group theory.

theorem Q2Presentation.Induction.MinimalBlock.not_scalarTerminal {p : FramedPair} (B : MinimalBlock p) : ¬ScalarTerminal p

A MinimalBlock exists only for a non-scalar target (the nonScalar field): the block witnesses non-scalarity. This is the tightness half ensuring the structure is not free-floating data.

theorem Q2Presentation.Induction.nonempty_minimalBlock_iff (p : FramedPair) : Nonempty (MinimalBlock p) ↔ ¬ScalarTerminal p

Non-scalarity is exactly block-existence (sec:block entry/exit): combining the tightness projection with the §7 bridge axiom, a target admits a minimal non-scalar block iff it is not scalar-terminal. This pins the bridge axiom to the manuscript dichotomy (thm:closedrecursion ∨ lem:scalarterminal) and rules out a vacuous block.

Acceptance checks