Route28 minimal-block pushout/determinant refinement

Route27 exposes the Section 7 pushout/determinant frontier as two coherent residuals:

• minimalBlock_preheadCentralPushoutSemanticData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar keeps the same downstream lower-route shape, but splits those two route27 residuals into the finer manuscript-shaped packets already available in the Section 7 API.

The scalar central-pushout family is built from the standard same-family quadratic packet, square diagonal, and polar symmetry leaves. The determinant side is the split prop:simpleheaddet packet for that same actual scalar family: naturality, diagonal vanishing on T, polar vanishing on T x M, and radical containment. Manuscript anchor: Section 7, pages 41-42, especially prop:simpleheaddet for the scalar pushouts K_lambda = K / ker lambda.

Route28 actual scalar plus split determinant packet

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

Route28 data for the Section 7 central-pushout/determinant branch.

The scalar field is the actual scalar pushout family selected by the standard square/polar proof hooks. The determinant field is deliberately indexed by actualScalar.toSemanticData, so all determinant conclusions refer to the same K_lambda = K / ker lambda family as the scalar square and polar data.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• determinantPieces : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData self.actualScalar.toSemanticData

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

The semantic family selected by the route28 actual scalar pushout.

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData.actualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.semantic

The bundled actual determinant packet recovered theorem-level from the route28 split determinant pieces.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData.toRoute25Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData D) : MinimalBlockPushoutRoute25ActualCentralExtensionData D

Route28 data repackaged in route25's same-family provider structure.

Equations

• P.toRoute25Data = { actualScalar := P.actualScalar, determinantPieces := ⋯ }

def Q2Presentation.Induction.MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData.toActualPushout {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Broad actual central-extension pushout data recovered through route25's projection chain. This is compatibility glue only; it does not call route27's broad semantic or bundled actual determinant residuals.

Equations

• P.toActualPushout = P.toRoute25Data.toActualPushout

def Q2Presentation.Induction.MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData.toPushoutRouteLower {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData D) : MinimalBlockPreheadPushoutRouteLowerData D

Route28 data projected to the lower pushout route in route27's downstream shape.

Equations

• P.toPushoutRouteLower = P.toRoute25Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route28 actual-scalar/split-determinant data.

This replaces route27's two broad pushout residuals by seven narrower leaves:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

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

Route25-compatible packet, constructed through route28's finer same-family central-extension packet.

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

Broad actual central-extension packet recovered through route28.

The conclusion is retained only for compatibility with older route interfaces; the proof does not call minimalBlock_preheadCentralPushoutSemanticData or minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

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

Supervisor hook: route27-shaped lower pushout provider from route28 split actual-scalar determinant data.

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

Determinant packet projection through the route28 lower pushout theorem.

Acceptance checks / exact residual report