Actual determinant packet from semantic simple-head pieces

This sidecar leaves the routed files untouched and narrows the current residual minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

For a fixed actual semantic central-pushout family S, the current residual is the bundled prop:simpleheaddet packet. The split packet below records the four manuscript-shaped pieces already exposed by the semantic §7 API for the same family:

• naturality of phi_lambda;
• diagonal vanishing on T;
• polar vanishing on T x M;
• radical containment for the symmetrized polar form.

The conversion to the current actual packet is theorem-level. The only algebra used in the conversion is the proven extraspecial square/polar API from MinimalBlock.lean: extraspecial_annihilates and extraspecial_radical_subset.

Split actual determinant packet

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

Smaller, manuscript-shaped simple-head determinant residual for one actual semantic central-pushout family.

This keeps all four fields tied to the same S, but states the vanishing and radical claims directly on the semantic pairing S.phi. The current bundled actual packet for S.toQuadraticFamily.square is recovered below by the proven extraspecial square-map lemmas.

• naturality : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S
• diagonalZero : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S
• polarZero : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S
• radicalContainment : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData.toActualData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData S) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S

Convert the split manuscript-shaped determinant pieces to the current actual central-pushout simple-head determinant packet.

Equations

• ⋯ = ⋯

Theorem-level closures from the narrower semantic pieces

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

The split packet is exactly the four semantic determinant pieces for the same actual central-pushout family.

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

Replacement for the current actual determinant residual, narrowed to the four semantic prop:simpleheaddet pieces for the same central-pushout family.

The axiom closure of this theorem does not use minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual_from_actualSemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S.toSelfDuality))

Route-ready extraspecial simple-head determinant packet from the narrowed actual determinant closure.

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

Lower pushout route using the actual scalar central-pushout family and the narrowed determinant proof above.

This is a sidecar replacement hook only; no routed file imports it yet.

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

Determinant packet projection from the narrowed sidecar route.