Theorem-level closers for Section 7 minimal-block packets

This sidecar keeps the existing MinimalBlockResidualRefinement API untouched and adds small theorem-level replacements/splits for the remaining manuscript Section 7 packets. The main low-hanging closer is the determinant nonzero field: once the simple head M / T is known nontrivial, the polar-radical containment forces the extraspecial diagonal to be nonzero. This proves the nonzero determinant packet from lem:simplehead's nontrivial-head field plus the radical field of prop:simpleheaddet.

The file also records concrete reassembly lemmas for two other packet boundaries: nonzero invariant characters give scalar quotients over F_2, and the determinant annihilation/invariance packets can be split into diagonal/polar/naturality data.

Scalar quotient from a nonzero invariant character

def Q2Presentation.Induction.MinimalBlockPreheadScalarQuotientData.ofInvariantCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (X : MinimalBlockPreheadInvariantCharacterData D) : MinimalBlockPreheadScalarQuotientData D

A nonzero invariant character is already the scalar quotient packet: over F_2, nonzero linear maps to F_2 are surjective.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadScalarQuotientData.ofInvariantCharacter X = { quotient := Classical.choose ⋯, quotient_surjective := ⋯, quotient_invariant := ⋯ }

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

Exact replacement theorem for the pre-head scalar quotient packet, from the smaller nonzero-invariant-character packet.

Concrete splits for determinant invariance and annihilation

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

Naturality of the pre-head extraspecial self-duality family. This is stronger than diagonal invariance and matches the manuscript's central-pushout naturality.

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

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialInvariantData.ofNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (N : MinimalBlockPreheadExtraspecialNaturalityData F) : MinimalBlockPreheadExtraspecialInvariantData F

Diagonal invariance follows from naturality by evaluating both variables on the same vector.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialInvariantData_from_naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) (hN : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData F)) : Nonempty (MinimalBlockPreheadExtraspecialInvariantData F)

Exact replacement theorem for the pre-head diagonal-invariance packet, from the more concrete self-duality naturality packet.

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

The diagonal-vanishing half of determinant annihilation on T.

• 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

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

The polar-vanishing half of determinant annihilation on T × M.

• 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

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialAnnihilationData.ofDiagonalPolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D} (Z : MinimalBlockPreheadExtraspecialDiagonalZeroData F) (P : MinimalBlockPreheadExtraspecialPolarZeroData F) : MinimalBlockPreheadExtraspecialAnnihilationData F

Reassemble the current annihilation packet from its diagonal and polar halves.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialAnnihilationData_from_diagonalPolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) (hZ : Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData F)) (hP : Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData F)) : Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F)

Exact replacement theorem for the pre-head annihilation packet, from the two concrete diagonal and polar vanishing packets.

Determinant nonzero from nontrivial head plus radical containment

theorem Q2Presentation.Induction.MinimalBlockPreheadExtraspecialNonzeroData.ofHeadRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (hhead : Nontrivial (D.M ⧸ D.T)) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) (R : MinimalBlockPreheadExtraspecialRadicalData F) : MinimalBlockPreheadExtraspecialNonzeroData F

If every extraspecial diagonal value vanished, the quadratic identity would make every vector polar-radical. Radical containment would then force M = T, contradicting nontriviality of the head.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialNonzeroData_from_headRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (hhead : Nontrivial (D.M ⧸ D.T)) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) (hR : Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)) : Nonempty (MinimalBlockPreheadExtraspecialNonzeroData F)

Exact replacement theorem for the pre-head determinant-nonzero packet, using the nontrivial simple head and the polar-radical packet.

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

Alternative exact replacement for minimalBlock_of_nonScalar, removing the pre-head determinant-nonzero residual by deriving it from the simple-head nontrivial packet plus radical containment. This is a sidecar theorem: it does not modify the current CountsEqualDeaxiom route.

Acceptance checks