Route25 minimal-block pushout/determinant refinement

Route24's coordinator hook

• minimalBlock_preheadPushoutRouteLowerData_from_route24ActualDeterminant

has the desired lower-route output shape, but its proof bottoms out at the broad actual central-extension residual

• minimalBlock_preheadActualCentralExtensionPushoutData.

This sidecar keeps the same route-lower output shape while rebuilding the route23 same-family packet from narrower manuscript-shaped pieces:

• an actual scalar central-pushout family, obtained from the standard square/diagonal/polar packets plus the scalar comparison packet;
• the split prop:simpleheaddet pieces for that same projected semantic family: naturality, diagonal zero, polar zero, and radical containment.

The result is route24-compatible for the nonterminal Fourier branch: it returns MinimalBlockPreheadPushoutRouteLowerData D, but its axiom closure no longer contains minimalBlock_preheadActualCentralExtensionPushoutData.

Route25 same-family actual central-extension packet

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

Route25 actual central-extension data.

The scalar pushout family and determinant pieces are indexed by the same semantic family actualScalar.toSemanticData, matching the manuscript's K_lambda = K / ker lambda pushout and prop:simpleheaddet conclusions for that same family.

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

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

The semantic central-pushout family selected by the route25 scalar pushout.

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute25ActualCentralExtensionData.determinantSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute25ActualCentralExtensionData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData P.semantic

The route23 split determinant packet carried by route25.

Equations

• ⋯ = ⋯

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

The actual determinant packet for the same route25 semantic family.

Equations

• ⋯ = ⋯

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

Route25 data repackaged in route23's same-family structure.

Equations

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

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

Broad actual central-extension pushout data recovered theorem-level from the route25 same-family packet.

Equations

• P.toActualPushout = P.toRoute23Data.toActualPushout

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

Route25 data projected to the lower pushout route through route23's provider shape.

Equations

• P.toPushoutRouteLower = P.toRoute23Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route25 actual central-extension data from the finer current APIs.

The nonstandard closure of this theorem avoids the route24 broad residual minimalBlock_preheadActualCentralExtensionPushoutData. Its remaining Section 7 floor is the standard actual-scalar pushout construction plus the four same-family split determinant pieces.

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

Route23-compatible packet, constructed through route25's finer same-family central-extension packet.

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

Broad actual central-extension pushout packet recovered through route25.

This theorem has the old broad packet as its conclusion only for compatibility; its proof does not call minimalBlock_preheadActualCentralExtensionPushoutData.

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

Supervisor hook: route24-shaped lower pushout provider from route25 actual central-extension data.

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

Determinant packet projection through the route25 lower pushout theorem.

Acceptance checks / exact residual report