Finer residuals for the Section 7 minimal block

This file continues the strengthened Section 7 work. It does not use the retired one-point diagnostic from MinimalBlockExistence.lean, and it does not weaken the MinimalBlock interface. Instead, it proves the exact statement of minimalBlock_of_nonScalar from smaller manuscript-shaped residuals.

Manuscript anchors: reference/q2_manuscript.tex, Section 7 sec:block:

• non-scalar chief factor: the paragraph choosing S triangleleft P <= L_Y;
• lem:simplehead: the exact sequence 0 → T → M → V → 0, nontrivial simple head, T = rad M, and (M^vee)^C = 0;
• lem:collapse: the Frattini-centralizer collapse giving the elementary central quotient R = Phi(K) and the character space used below;
• prop:simpleheaddet: the determinant pushout square maps and their annihilation, radical, nonzero, and invariance properties.

Plan anchor: reference/plan_4turns.md, Stage H, where Section 7 is separated from Section 8 central-cover/Fourier recursion and treated as finite group/module work.

The non-scalar chief factor, extracted from not ScalarTerminal

structure Q2Presentation.Induction.NonScalarChiefFactor (p : FramedPair) : Type

A concrete non-scalar chief factor in the marked wild kernel L_Y.

This is the Lean form of the Section 7 entry point: choose S triangleleft P <= L_Y with P/S the first non-scalar simple factor. Here the existing project predicate ChiefFactorInLY supplies the chief-factor condition, and not ChiefFactorTrivial records non-scalarity.

• lower : Subgroup p.fst.Y
• upper : Subgroup p.fst.Y
• chief : ChiefFactorInLY p.fst self.lower self.upper
• nontrivial_action : ¬ChiefFactorTrivial p.fst self.lower self.upper

theorem Q2Presentation.Induction.exists_nonScalarChiefFactor_of_nonScalar (p : FramedPair) : ¬ScalarTerminal p → Nonempty (NonScalarChiefFactor p)

A non-scalar framed pair has a non-scalar chief factor. This is just the logical unpacking of the current ScalarTerminal definition, not a new axiom.

Residual 1: the Section 7 tower and simple-head package

structure Q2Presentation.Induction.MinimalBlockRawModuleData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

The raw finite objects in the Section 7 quotient tower, before the C-actions are installed.

Manuscript anchor: eq:targettower, namely the elementary Frattini layer R = Phi(K), the elementary quotient M = K/R, the submodule T = (K cap S)/R, and the lower quotient group C = Y/K.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C

structure Q2Presentation.Induction.MinimalBlockRawActionData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawModuleData p chief) : Type

The C-module structures on the raw Section 7 tower.

Manuscript anchor: lem:simplehead, where 0 -> T -> M -> V -> 0 is an exact sequence of F_2[C]-modules, and X_R = (R^vee)^C uses the induced C-action on the Frattini quotient R.

• actR : D.C →* D.R ≃ₗ[ZMod 2] D.R
• actM : D.C →* D.M ≃ₗ[ZMod 2] D.M
• T_stable (c : D.C) (m : D.M) : m ∈ D.T → (self.actM c) m ∈ D.T

structure Q2Presentation.Induction.MinimalBlockRawTowerData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

The raw module-level quotient tower supplied by the Section 7 choice of the minimal normal subgroup K.

This deliberately stops before the simple-head representation input, determinant characters, and pushouts. It records only the finite F_2 modules R = Phi(K), M = K/R, the submodule T, the quotient group C = Y/K, the two actions, and stability of T.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R
• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M
• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T

def Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawModuleData p chief) (A : MinimalBlockRawActionData D) : MinimalBlockRawTowerData p chief

Reassemble the raw tower from the smaller finite-object and action packets.

Equations

• One or more equations did not get rendered due to their size.

structure Q2Presentation.Induction.MinimalBlockPreheadTowerData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

The Section 7 tower before the nonzero simple-head field is installed.

This is useful because M/T being nonzero can also be recovered from a nonzero determinant square map that annihilates T: a vector with nonzero square cannot lie in T. The resulting final assembly therefore does not need a separate head-nontrivial residual.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R
• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M
• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T
• dualInv_zero (phi : Module.Dual (ZMod 2) self.M) : (∀ (c : self.C), phi ∘ₗ ↑(self.actM c) = phi) → phi = 0

structure Q2Presentation.Induction.MinimalBlockSimpleHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

The simple-head representation input over a raw Section 7 tower.

This is the Lean form of the non-vacuous part of lem:simplehead: the head M/T is genuinely nontrivial, and the unique non-scalar simple head gives (M^vee)^C = 0.

• head_nontrivial : Nontrivial (D.M ⧸ D.T)
• dualInv_zero (phi : Module.Dual (ZMod 2) D.M) : (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) → phi = 0

structure Q2Presentation.Induction.MinimalBlockHeadNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

The nonzero simple-head part of lem:simplehead: M/T is the first genuine non-scalar simple head, not a zero quotient.

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

structure Q2Presentation.Induction.MinimalBlockDualInvariantVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

The dual-invariant vanishing part of lem:simplehead: (M^vee)^C = 0.

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

def Q2Presentation.Induction.MinimalBlockPreheadTowerData.ofRaw {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (V : MinimalBlockDualInvariantVanishesData D) : MinimalBlockPreheadTowerData p chief

Assemble the pre-head tower from the raw tower and the dual-invariant vanishing part of lem:simplehead, without assuming M/T is already known nonzero.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.MinimalBlockSimpleHeadData.ofPieces {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (H : MinimalBlockHeadNontrivialData D) (V : MinimalBlockDualInvariantVanishesData D) : MinimalBlockSimpleHeadData D

Reassemble the simple-head packet from its two representation-theoretic conclusions.

Equations

• ⋯ = ⋯

structure Q2Presentation.Induction.MinimalBlockTowerData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

The module-level target tower supplied by the Section 7 choice of the minimal normal subgroup K and lem:simplehead.

This deliberately stops before determinant characters and pushouts. It records only the finite F_2 modules R = Phi(K), M = K/R, the radical T, the quotient group C = Y/K, the two actions, the nontrivial simple head M/T, stability of T, and the representation-theoretic input (M^vee)^C = 0.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C
• actR : self.C →* self.R ≃ₗ[ZMod 2] self.R
• actM : self.C →* self.M ≃ₗ[ZMod 2] self.M
• head_nontrivial : Nontrivial (self.M ⧸ self.T)
• T_stable (c : self.C) (m : self.M) : m ∈ self.T → (self.actM c) m ∈ self.T
• dualInv_zero (phi : Module.Dual (ZMod 2) self.M) : (∀ (c : self.C), phi ∘ₗ ↑(self.actM c) = phi) → phi = 0

def Q2Presentation.Induction.MinimalBlockTowerData.ofRaw {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (S : MinimalBlockSimpleHeadData D) : MinimalBlockTowerData p chief

Assemble the old tower packet from the finer raw-tower and simple-head packets.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.MinimalBlockTowerData.ofPrehead {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) (hhead : Nontrivial (D.M ⧸ D.T)) : MinimalBlockTowerData p chief

Install a proved nonzero-head witness on a pre-head tower.

Equations

• One or more equations did not get rendered due to their size.

axiom Q2Presentation.Induction.minimalBlock_rawModuleData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockRawModuleData p chief)

Residual Section 7 axiom: raw finite quotient objects.

Manuscript anchors: the construction of K minimal subject to KS = P, eq:targettower, and the Frattini quotient definitions R = Phi(K), M = K/R, T = (K cap S)/R, C = Y/K. This packet does not assert the C-actions, the simple-head representation facts, determinant characters, or pushout forms.

axiom Q2Presentation.Induction.minimalBlock_rawActionData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawModuleData p chief) : Nonempty (MinimalBlockRawActionData D)

Residual Section 7 axiom: quotient-tower actions.

Manuscript anchors: eq:targettower and lem:simplehead, where the raw objects are acted on by C = Y/K and T is a C-submodule of M.

theorem Q2Presentation.Induction.minimalBlock_rawTowerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockRawTowerData p chief)

The former raw-tower residual is assembled from the smaller finite-object and action packets.

axiom Q2Presentation.Induction.minimalBlock_headNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockHeadNontrivialData D)

Residual Section 7 axiom: nontrivial simple head.

Manuscript anchor: lem:simplehead, specifically that M/T is the first non-scalar simple head.

axiom Q2Presentation.Induction.minimalBlock_dualInvariantVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData D)

Residual Section 7 axiom: dual-invariant vanishing.

Manuscript anchor: lem:simplehead, specifically (M^vee)^C = 0.

theorem Q2Presentation.Induction.minimalBlock_preheadTowerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockPreheadTowerData p chief)

The pre-head tower is assembled without the old head-nontrivial residual.

theorem Q2Presentation.Induction.minimalBlock_simpleHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockSimpleHeadData D)

The former simple-head residual is assembled from the nontrivial-head and dual-invariant-vanishing packets.

theorem Q2Presentation.Induction.minimalBlock_towerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockTowerData p chief)

The former tower/simple-head residual is now a theorem assembled from two narrower Section 7 facts.

Residual 2: nonzero determinant character

structure Q2Presentation.Induction.MinimalBlockInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Prop

Nonzero invariant determinant characters for the Section 7 tower.

This is separated from MinimalBlockTowerData because the old vacuity bug was exactly that the character space could be empty of nonzero elements. The strengthened MinimalBlock requires this witness explicitly.

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

axiom Q2Presentation.Induction.minimalBlock_nonzeroInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockInvariantCharacterData D)

Residual Section 7 axiom: nonzero invariant determinant character.

Manuscript anchor: the nonempty determinant character space X_R = (R^vee)^B = (R^vee)^C ranged over in prop:simpleheaddet. This is strictly smaller than a chosen scalar quotient: the quotient surjectivity is proved below from nonzeroness over F_2.

structure Q2Presentation.Induction.MinimalBlockScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Type

A scalar quotient of the Frattini layer R.

This is the finite-module form of saying that the scalar factors below the first non-scalar layer leave a nonzero trivial quotient of R. A surjection R -> F_2 fixed by C is exactly a nonzero invariant determinant character, but this formulation rules out the one-point shortcut by surjectivity rather than by a bare nonzero witness.

• quotient : Module.Dual (ZMod 2) D.R
• quotient_surjective : Function.Surjective ⇑self.quotient
• quotient_invariant (c : D.C) : self.quotient ∘ₗ ↑(D.actR c) = self.quotient

theorem Q2Presentation.Induction.minimalBlock_scalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockScalarQuotientData D)

Residual Section 7 axiom: scalar quotient of the Frattini layer.

Manuscript anchor: X_R = (R^vee)^B = (R^vee)^C and the quantification over 0 != lambda in X_R in prop:simpleheaddet. This is the precise non-vacuity condition needed by the strengthened interface, stated as a fixed scalar quotient of R.

theorem Q2Presentation.Induction.minimalBlock_invariantCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockInvariantCharacterData D)

The former invariant-character residual follows from the scalar quotient packet.

structure Q2Presentation.Induction.MinimalBlockPreheadInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Prop

Nonzero invariant determinant characters over a pre-head Section 7 tower.

This is the same Frattini-character input as MinimalBlockInvariantCharacterData, but stated before M/T has been proved nonzero.

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

structure Q2Presentation.Induction.MinimalBlockPreheadScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

A scalar quotient of the Frattini layer over a pre-head Section 7 tower.

This is the pre-head form of the manuscript's nonzero determinant-character input: instead of asking for an abstract nonzero lambda in (R^vee)^C, it supplies the actual scalar pushout quotient R -> F_2 used to form K_lambda.

• quotient : Module.Dual (ZMod 2) D.R
• quotient_surjective : Function.Surjective ⇑self.quotient
• quotient_invariant (c : D.C) : self.quotient ∘ₗ ↑(D.actR c) = self.quotient

axiom Q2Presentation.Induction.minimalBlock_preheadScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadScalarQuotientData D)

Residual Section 7 axiom: scalar quotient of the Frattini layer, pre-head form.

Manuscript anchor: the nonempty determinant character space X_R = (R^vee)^B = (R^vee)^C ranged over in prop:simpleheaddet, now stated as the scalar quotient that defines the central pushout K_lambda.

theorem Q2Presentation.Induction.minimalBlock_preheadNonzeroInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadInvariantCharacterData D)

The former pre-head nonzero-character residual follows from the more concrete scalar quotient packet.

Residual 3: determinant pushout on the simple head

structure Q2Presentation.Induction.MinimalBlockPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Type

The determinant pushout data and prop:simpleheaddet inputs over a fixed Section 7 tower. These are exactly the remaining pushout fields of MinimalBlock, separated from the tower/simple-head construction.

• pushout : Module.Dual (ZMod 2) D.R → Quadratic.QuadF2 D.M
• pushout_annih (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → Annihilates (self.pushout lam) D.T
• pushout_radical (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((self.pushout lam).polar m) m' = 0) → m ∈ D.T
• pushout_nonzero (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∃ (m : D.M), (self.pushout lam).form m ≠ 0
• pushout_invariant (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m : D.M), (self.pushout lam).form ((D.actM c) m) = (self.pushout lam).form m

structure Q2Presentation.Induction.MinimalBlockExtraspecialPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Type

Extraspecial self-duality data for the determinant pushouts.

Instead of postulating an arbitrary family of quadratic forms, this packet supplies the self-duality phi_lambda : M -> M^vee whose extraspecial square map is the central-pushout form. The remaining hypotheses are the manuscript facts needed by prop:simpleheaddet, stated on the diagonal and symmetrized polar pairing of phi_lambda.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M
• diagonal_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ((self.phi lam) t) t = 0
• symm_polar_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ∀ (m : D.M), ((self.phi lam) t) m + ((self.phi lam) m) t = 0
• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((self.phi lam) m) m' + ((self.phi lam) m') m = 0) → m ∈ D.T
• diagonal_nonzero (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∃ (m : D.M), ((self.phi lam) m) m ≠ 0
• diagonal_invariant (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m : D.M), ((self.phi lam) ((D.actM c) m)) ((D.actM c) m) = ((self.phi lam) m) m

structure Q2Presentation.Induction.MinimalBlockExtraspecialPushoutFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Type

The family of extraspecial self-dualities underlying the determinant pushouts.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

structure Q2Presentation.Induction.MinimalBlockExtraspecialAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Prop

The two annihilation conclusions of prop:simpleheaddet for the extraspecial square maps: diagonal zero on T and polar zero on T x M.

• diagonal_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ((F.phi lam) t) t = 0
• symm_polar_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ∀ (m : D.M), ((F.phi lam) t) m + ((F.phi lam) m) t = 0

structure Q2Presentation.Induction.MinimalBlockExtraspecialRadicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Prop

The polar-radical containment conclusion of prop:simpleheaddet.

• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((F.phi lam) m) m' + ((F.phi lam) m') m = 0) → m ∈ D.T

structure Q2Presentation.Induction.MinimalBlockExtraspecialNonzeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Prop

The nonzero diagonal conclusion of prop:simpleheaddet, equivalent to the descended simple-head form being nonzero.

• diagonal_nonzero (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∃ (m : D.M), ((F.phi lam) m) m ≠ 0

structure Q2Presentation.Induction.MinimalBlockExtraspecialInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Prop

The C-invariance conclusion of the determinant square maps.

• diagonal_invariant (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m : D.M), ((F.phi lam) ((D.actM c) m)) ((D.actM c) m) = ((F.phi lam) m) m

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialEquivariantFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

Equivariant extraspecial self-duality data over a pre-head tower.

This is now an assembled packet: the bare central-pushout self-duality family and its C-naturality/diagonal-invariance proof are separated below, then reassembled here for the existing downstream pre-head determinant interfaces.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M
• diagonal_invariant (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m : D.M), ((self.phi lam) ((D.actM c) m)) ((D.actM c) m) = ((self.phi lam) m) m

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

The bare extraspecial self-duality family over a pre-head tower, before its C-equivariance/naturality is installed.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) : Prop

The diagonal-invariance/naturality conclusion for a pre-head extraspecial family.

• diagonal_invariant (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m : D.M), ((F.phi lam) ((D.actM c) m)) ((D.actM c) m) = ((F.phi lam) m) m

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialEquivariantFamilyData.ofFamilyInvariant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) (I : MinimalBlockPreheadExtraspecialInvariantData F) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

Reassemble the equivariant family packet from a bare family and its invariance property.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadExtraspecialEquivariantFamilyData.ofFamilyInvariant F I = { phi := F.phi, diagonal_invariant := ⋯ }

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Prop

The two annihilation conclusions of prop:simpleheaddet, stated over the pre-head equivariant determinant family.

• diagonal_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ((F.phi lam) t) t = 0
• symm_polar_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ∀ (m : D.M), ((F.phi lam) t) m + ((F.phi lam) m) t = 0

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialRadicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Prop

The polar-radical containment conclusion of prop:simpleheaddet, stated before the head-nontrivial field is installed.

• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((F.phi lam) m) m' + ((F.phi lam) m') m = 0) → m ∈ D.T

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialNonzeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Prop

The nonzero diagonal conclusion of prop:simpleheaddet, stated before the head-nontrivial field is installed.

• diagonal_nonzero (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∃ (m : D.M), ((F.phi lam) m) m ≠ 0

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadExtraspecialFamilyData D)

Residual Section 7 axiom: bare extraspecial determinant family.

Manuscript anchor: the central pushouts K_lambda of prop:simpleheaddet, before the separate C-invariance/naturality proof is installed.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialInvariantData F)

Residual Section 7 axiom: determinant square-map invariance, pre-head form.

Manuscript anchor: the C-invariance/naturality of the scalar central pushouts in prop:simpleheaddet, separated from the existence of the extraspecial family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialEquivariantFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadExtraspecialEquivariantFamilyData D)

The former equivariant-family residual is assembled from a bare extraspecial family and its diagonal-invariance packet.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F)

Residual Section 7 axiom: determinant annihilation on T, pre-head form.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Residual Section 7 axiom: determinant polar radical, pre-head form.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialNonzeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialNonzeroData F)

Residual Section 7 axiom: nonzero determinant square map, pre-head form.

theorem Q2Presentation.Induction.minimalBlock_headNontrivial_from_determinant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (X : MinimalBlockPreheadInvariantCharacterData D) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (N : MinimalBlockPreheadExtraspecialNonzeroData F) : Nontrivial (D.M ⧸ D.T)

A nonzero determinant square map that annihilates T proves that the quotient M/T is nontrivial. This removes the old head-nontrivial packet from the final closure while preserving the strengthened MinimalBlock interface.

def Q2Presentation.Induction.MinimalBlockExtraspecialPushoutData.ofPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) (A : MinimalBlockExtraspecialAnnihilationData F) (R : MinimalBlockExtraspecialRadicalData F) (N : MinimalBlockExtraspecialNonzeroData F) (I : MinimalBlockExtraspecialInvariantData F) : MinimalBlockExtraspecialPushoutData D

Reassemble the old extraspecial pushout packet from its component determinant properties.

Equations

• One or more equations did not get rendered due to their size.

axiom Q2Presentation.Induction.minimalBlock_extraspecialPushoutFamilyData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockExtraspecialPushoutFamilyData D)

Residual Section 7 axiom: extraspecial determinant self-duality family.

Manuscript anchor: the central pushouts K_lambda of prop:simpleheaddet; this packet supplies only the family whose extraspecial square maps are evaluated.

axiom Q2Presentation.Induction.minimalBlock_extraspecialAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Nonempty (MinimalBlockExtraspecialAnnihilationData F)

Residual Section 7 axiom: determinant annihilation on T.

Manuscript anchor: prop:simpleheaddet, including the cohomology-vanishing shear argument used to prove q_lambda|_T = 0 and b_lambda(T,M)=0.

axiom Q2Presentation.Induction.minimalBlock_extraspecialRadicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Nonempty (MinimalBlockExtraspecialRadicalData F)

Residual Section 7 axiom: determinant polar radical.

Manuscript anchor: the final paragraph of prop:simpleheaddet, where the polar radical on the simple module is forced to be zero, equivalently the radical upstairs is contained in T.

axiom Q2Presentation.Induction.minimalBlock_extraspecialNonzeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Nonempty (MinimalBlockExtraspecialNonzeroData F)

Residual Section 7 axiom: nonzero determinant square map.

Manuscript anchor: Phi(K_lambda) = R / ker lambda != 1, which makes the descended quadratic form nonzero.

axiom Q2Presentation.Induction.minimalBlock_extraspecialInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockTowerData p chief} (F : MinimalBlockExtraspecialPushoutFamilyData D) : Nonempty (MinimalBlockExtraspecialInvariantData F)

Residual Section 7 axiom: determinant square-map invariance.

Manuscript anchor: the C-invariance of the descended determinant form on the simple head.

theorem Q2Presentation.Induction.minimalBlock_extraspecialPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockExtraspecialPushoutData D)

The former extraspecial-pushout residual is assembled from the smaller determinant-family, annihilation, radical, nonzero, and invariance packets.

theorem Q2Presentation.Induction.minimalBlock_pushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockTowerData p chief) : Nonempty (MinimalBlockPushoutData D)

The former determinant-pushout residual follows from extraspecial self-duality data and the already-proven extraspecial quadratic-form helpers.

Reassembly into the strengthened MinimalBlock interface

def Q2Presentation.Induction.minimalBlock_of_preheadRefinedData {p : FramedPair} (h : ¬ScalarTerminal p) (chief : NonScalarChiefFactor p) (D : MinimalBlockPreheadTowerData p chief) (X : MinimalBlockPreheadInvariantCharacterData D) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) (N : MinimalBlockPreheadExtraspecialNonzeroData F) : MinimalBlock p

Assemble the strengthened MinimalBlock from pre-head tower data and determinant packets. The simple-head nontriviality field is proved from determinant nonzeroness and annihilation, and determinant invariance comes from the equivariant family.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.minimalBlock_of_refinedData {p : FramedPair} (h : ¬ScalarTerminal p) (chief : NonScalarChiefFactor p) (D : MinimalBlockTowerData p chief) (X : MinimalBlockInvariantCharacterData D) (P : MinimalBlockPushoutData D) : MinimalBlock p

Assemble the strengthened MinimalBlock from the finer Section 7 residuals.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_refined (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

The exact statement of the strengthened minimalBlock_of_nonScalar residual, proved from finer Section 7 facts and not from the old monolithic axiom.

Acceptance checks