Coherent semantic determinant packet for Section 7

This sidecar leaves every routed file untouched. It narrows the four current final-closure determinant semantic packets

• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData;

to one same-family prop:simpleheaddet packet for the actual central-pushout family S. The projections below are theorem-level, and the route-ready hooks have the same conclusions as the existing actual determinant semantic closers.

Manuscript anchor: reference/q2_manuscript.tex, Section 7, prop:simpleheaddet, pages 41--42: naturality of the scalar pushout, diagonal vanishing on T, polar vanishing on T x M, and polar-radical containment.

One coherent semantic determinant packet

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

A same-family semantic determinant packet for one actual central-pushout family S.

The current final path asks for the four fields below as independent residuals. This packet records the manuscript-shaped assertion that all four conclusions come from the same scalar pushout K_lambda = K / ker lambda.

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

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

Closed coherent packet: prop:simpleheaddet for one actual central-pushout family, assembled from the four same-family semantic determinant packets.

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

Convert the coherent semantic packet to the split actual determinant packet already used by MinimalBlockActualDeterminantProofs.

Equations

• ⋯ = ⋯

Projections to the four current semantic packets

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

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

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

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

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

All four current semantic determinant packets, tied to one central-pushout family and one residual.

Route-ready replacements for the current actual determinant semantic closers

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

Route-ready replacement for minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualSplitData_from_semanticClosers.

Its closure uses one coherent determinant semantic residual instead of the four independent semantic packet residuals.

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

Route-ready replacement for minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_semanticClosers.

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

Route-ready replacement for minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual_from_actualSemanticClosers.

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

Lower pushout route using the actual scalar central-pushout family and the coherent determinant semantic packet.

This is the sidecar replacement hook for minimalBlock_preheadPushoutRouteLowerData_from_actualDeterminantSemanticClosers.

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

Determinant packet projection from the coherent semantic determinant route.