Route30 minimal-block pushout/determinant provider

Route29 replaced the two live Section 7 pushout residuals

• minimalBlock_preheadCentralPushoutSemanticData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData

by one actual central-extension pushout packet assembled from seven split actual K_lambda = K / ker lambda packets.

This route30 sidecar keeps the route29 downstream shape but supplies its actual central-extension packet through MinimalBlockActualCentralExtensionClosers2. Thus a future route swap can use the same semantic family and same-family determinant packet while avoiding the seven route29 split actual central-extension packet axioms. The remaining pushout floor is the narrower self-duality/extraspecial determinant interface used by Closers2.

Route30 provider through the extraspecial actual central-extension closer

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

Route30 pushout data.

The single field is the broad actual central-extension pushout packet, but the constructor below obtains it from MinimalBlockActualCentralExtensionClosers2, not from route29's seven split actual central-extension packet axioms.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The route30 semantic central-pushout family.

Equations

• P.semantic = P.actual.toSemanticData

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

The route30 same-family actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute30ActualCentralExtensionClosedData.toRoute29Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute30ActualCentralExtensionClosedData D) : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D

Repackage route30 data in route29's provider structure.

Equations

• P.toRoute29Data = { actual := P.actual }

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

Route28-compatible packet inherited from the route29 projection chain.

Equations

• P.toRoute28Data = P.toRoute29Data.toRoute28Data

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

Lower pushout route inherited from the route29 downstream shape.

Equations

• P.toPushoutRouteLower = P.toRoute29Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route30 actual central-extension data through Closers2.

Residual report: this theorem avoids route29's seven split actual central-extension packet axioms

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionSquareData;
• minimalBlock_preheadActualCentralExtensionDiagonalData;
• minimalBlock_preheadActualCentralExtensionPolarData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

Its remaining nonstandard closure is the narrower extraspecial/self-duality floor of MinimalBlockActualCentralExtensionClosers2.

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

Route29-compatible split-provider data, but supplied by route30's Closers2 path instead of route29's split packet constructor.

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

Route30 supplies the semantic central-pushout residual target from the same actual central-extension family.

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

Route30 supplies the live determinant residual target for the same semantic family selected by its actual central-extension packet.

This is the route-relevant same-family form of the residual; it does not assert the old arbitrary-family axiom.

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

Supervisor hook: route29-shaped lower pushout provider from the route30 Closers2 path.

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

Determinant packet projection through the route30 lower pushout provider.

Acceptance checks / exact residual report