Lower Section 7 pushout packet reductions

This sidecar is intentionally not routed into PresentationCorrect. It records the next lower proof boundary for the final-closure Section 7 PREHEAD PUSHOUT / EXTRASPECIAL residuals.

The central-pushout square and polar packets are theorem-level consequences of a single self-duality family: the square is the extraspecial form Quadratic.Extraspecial.extraspecialForm.

The extraspecial vanishing/radical packets are reduced to one coherent simple-head determinant packet on the same bare family. That lower packet states prop:simpleheaddet on the actual extraspecial quadratic form, using the proven Annihilates abstraction from MinimalBlock.lean, rather than postulating the diagonal and polar identities independently.

Central-pushout square and polar packets from self-duality

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

The scalar central-pushout quadratic family determined by a self-duality family. The square map is the extraspecial quadratic form attached to the same phi_lambda.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquareDiagonalData.ofSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality S)

For the extraspecial square attached to phi_lambda, the square value is definitionally the diagonal value phi_lambda(m,m).

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarSymmData.ofSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadCentralPushoutPolarSymmData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality S)

The polar form of the extraspecial square is the symmetrized self-duality pairing.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutQuadraticFamilyData_from_selfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadCentralPushoutQuadraticFamilyData D)

Replacement for minimalBlock_preheadCentralPushoutQuadraticFamilyData, reduced to the older self-duality family.

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

Residual-backed version of minimalBlock_preheadCentralPushoutQuadraticFamilyData_from_selfDuality.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquareDiagonalData_from_selfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality S))

Replacement for minimalBlock_preheadCentralPushoutSquareDiagonalData on the quadratic family induced by a self-duality witness.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarSymmData_from_selfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality S))

Replacement for minimalBlock_preheadCentralPushoutPolarSymmData on the quadratic family induced by a self-duality witness.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPackets_from_selfDualityResidual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

Same-family central-pushout replacement triple from one self-duality residual.

This is the usable hook for rerouting the first three PREHEAD PUSHOUT residuals: it supplies the quadratic family together with its square-diagonal and polar-symmetry witnesses from one coherent phi_lambda source.

Extraspecial packets from one simple-head determinant packet

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

Lower same-family determinant packet for the PREHEAD extraspecial residuals.

The annihilates_on_T and radical_subset_T fields are stated on the actual extraspecial quadratic form attached to F.phi lam. They are the formal counterpart of q_lambda|_T = 0, b_lambda(T,M)=0, and polar-radical descent in prop:simpleheaddet.

• 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'
• annihilates_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → Annihilates (Quadratic.Extraspecial.extraspecialForm (F.phi lam)) D.T
• 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), ((Quadratic.Extraspecial.extraspecialForm (F.phi lam)).polar m) m' = 0) → m ∈ D.T

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData.toNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : MinimalBlockPreheadExtraspecialNaturalityData F

Project the lower determinant packet to the existing naturality packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData.toEquivariantFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

The equivariant family induced by the lower determinant packet.

Equations

• P.toEquivariantFamily = { phi := F.phi, diagonal_invariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData.toDiagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : MinimalBlockPreheadExtraspecialDiagonalZeroData P.toEquivariantFamily

Project q_lambda|_T = 0 for the actual extraspecial square to diagonal vanishing of phi_lambda on T.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData.toPolarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : MinimalBlockPreheadExtraspecialPolarZeroData P.toEquivariantFamily

Project b_lambda(T,M)=0 for the actual extraspecial polar form to the symmetrized phi_lambda polar packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData.toRadicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : MinimalBlockPreheadExtraspecialRadicalContainmentData P.toEquivariantFamily

Project polar-radical containment for the actual extraspecial form to the symmetrized phi_lambda radical-containment packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialNaturalityData_from_simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData F)

Replacement for minimalBlock_preheadExtraspecialNaturalityData, reduced to one lower simple-head determinant packet on the same bare family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialDiagonalZeroData_from_simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData P.toEquivariantFamily)

Replacement for minimalBlock_preheadExtraspecialDiagonalZeroData, reduced to the lower determinant packet on the induced equivariant family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPolarZeroData_from_simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData P.toEquivariantFamily)

Replacement for minimalBlock_preheadExtraspecialPolarZeroData, reduced to the lower determinant packet on the induced equivariant family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalContainmentData_from_simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData P.toEquivariantFamily)

Replacement for minimalBlock_preheadExtraspecialRadicalContainmentData, reduced to the lower determinant packet on the induced equivariant family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPackets_from_simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialFamilyData D} (P : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData F) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData P.toEquivariantFamily) ∧ Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData P.toEquivariantFamily) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData P.toEquivariantFamily)

Coherent same-family replacement hook for the four PREHEAD EXTRASPECIAL residuals.