Pushout-side Section 7 semantic proof reductions

This sidecar focuses only on the determinant/extraspecial pre-head pushout packets from manuscript Section 7, pages 40-42. It leaves the routed capstone untouched.

The current semantic route uses five axioms over one central-pushout family:

• minimalBlock_preheadCentralPushoutSemanticData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

This file gives theorem-level replacements for those five packet boundaries from the narrower standard determinant/extraspecial packets already present in the Section 7 API:

• the concrete central-pushout quadratic family, square diagonal, and polar symmetry packets;
• the extraspecial naturality, diagonal-zero, polar-zero, and radical-containment packets.

The aggregate theorem at the end is the intended replacement hook for the determinant half of minimalBlock_preheadDeterminantPackets_from_semanticClosers.

Concrete pushout family to semantic pushout family

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

The standard determinant pushout data behind the semantic family.

The semanticData projection below uses quadraticFamily.phi, while the two identity fields certify that the semantic extraspecial square has the same diagonal and polar pairing as the concrete square packet.

• quadraticFamily : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D
• squareDiagonal : MinimalBlockPreheadCentralPushoutSquareDiagonalData self.quadraticFamily
• polarSymm : MinimalBlockPreheadCentralPushoutPolarSymmData self.quadraticFamily

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutStandardData.semanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) : MinimalBlockPreheadCentralPushoutSemanticData D

Forget the concrete square while retaining the central-pushout self-duality family. The semantic square is then definitionally the extraspecial form of the same pairing.

Equations

• P.semanticData = { phi := P.quadraticFamily.phi }

theorem Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutStandardData.semantic_square_form_eq_actual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) (lam : Module.Dual (ZMod 2) D.R) (m : D.M) : (P.semanticData.toQuadraticFamily.square lam).form m = (P.quadraticFamily.square lam).form m

The semantic extraspecial square has the same diagonal as the concrete central-pushout square packet.

theorem Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutStandardData.semantic_square_polar_eq_actual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) (lam : Module.Dual (ZMod 2) D.R) (m m' : D.M) : ((P.semanticData.toQuadraticFamily.square lam).polar m) m' = ((P.quadraticFamily.square lam).polar m) m'

The semantic extraspecial polar form has the same polar pairing as the concrete central-pushout square packet.

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

Assemble the standard pushout data from the existing lower-level determinant packets.

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

Replacement theorem for the semantic central-pushout family packet, reduced to the standard concrete determinant square/polar packets.

Extraspecial packets to semantic naturality/zero/radical packets

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalitySemanticData.ofExtraspecialNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadExtraspecialNaturalityData S.toExtraspecialFamily) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S

Convert the standard extraspecial naturality packet to semantic central-pushout naturality for the same phi family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData.ofExtraspecialDiagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) (Z : MinimalBlockPreheadExtraspecialDiagonalZeroData N.toEquivariantFamily) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S

Convert the standard extraspecial diagonal-zero packet to semantic diagonal zero on T for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarZeroSemanticData.ofExtraspecialPolarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) (P : MinimalBlockPreheadExtraspecialPolarZeroData N.toEquivariantFamily) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S

Convert the standard extraspecial polar-zero packet to semantic polar zero on T x M for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData.ofExtraspecialRadicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) (R : MinimalBlockPreheadExtraspecialRadicalContainmentData N.toEquivariantFamily) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S

Convert the standard extraspecial radical-containment packet to semantic radical containment for the same central-pushout family.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutNaturalitySemanticData_from_standardPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData)

Replacement theorem for semantic naturality, reduced to the standard extraspecial naturality packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData_from_standardPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {P : MinimalBlockPreheadCentralPushoutStandardData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData) : Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semanticData)

Replacement theorem for semantic diagonal zero, reduced to the standard extraspecial diagonal-zero packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarZeroSemanticData_from_standardPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {P : MinimalBlockPreheadCentralPushoutStandardData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData) : Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semanticData)

Replacement theorem for semantic polar zero, reduced to the standard extraspecial polar-zero packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData_from_standardPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {P : MinimalBlockPreheadCentralPushoutStandardData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData) : Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semanticData)

Replacement theorem for semantic radical containment, reduced to the standard extraspecial radical-containment packet.

Aggregate replacement hooks

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSemanticPackets_from_standardPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The five semantic pushout packets, all supplied from standard determinant and extraspecial packets rather than from the five semantic axioms.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_from_standardPushoutPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Drop-in determinant-packet replacement for the determinant half of minimalBlock_preheadDeterminantPackets_from_semanticClosers.

This theorem avoids the five current semantic pushout axioms and closes over the standard determinant/extraspecial packets listed in this file's module comment.