Route40 minimal-block pushout/determinant provider

Route39's Section 7 pushout provider replaces the old bundled residuals by the seven actual central-extension packet leaves:

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

This Route40 sidecar keeps Route39's downstream shape, but obtains the broad actual central-extension packet from MinimalBlockExtraspecialClosers3. That closer reassembles the actual K_lambda = K / ker lambda pushout data from the manuscript-shaped square/polar construction and the same-family prop:simpleheaddet determinant packet (manuscript §7.1, Proposition 7.4, with the determinant background from §6).

Thus the provider below is drop-in compatible with Route39 while removing all seven Route39 split actual-central-extension residual names from its axiom closure. No new axiom is introduced here.

Route40 packet

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

Route40 data: the broad actual central-extension pushout packet, supplied by the coherent extraspecial closer rather than Route39's seven split packet axioms.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

def Q2Presentation.Induction.MinimalBlockPushoutRoute40Data.toRoute39Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute40Data D) : MinimalBlockPushoutRoute39Data D

Route40 projected to the Route39 provider structure.

Equations

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

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

The semantic central-pushout family selected by Route40.

Equations

• P.semantic = P.toRoute39Data.semantic

def Q2Presentation.Induction.MinimalBlockPushoutRoute40Data.actualScalar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute40Data D) : MinimalBlockPreheadActualScalarCentralPushoutData D

The actual scalar central-pushout packet selected by Route40.

Equations

• P.actualScalar = P.toRoute39Data.actualScalar

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

The same-family determinant packet selected by Route40.

Equations

• ⋯ = ⋯

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

Route40 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLower = P.toRoute39Data.toPushoutRouteLower

Route-compatible hooks

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

Construct Route40 data through the coherent extraspecial central-extension closer.

Residual report: the axiom closure of this theorem avoids all seven Route39 split actual-central-extension packet names. Its remaining pushout frontier is the MinimalBlockExtraspecialClosers3 floor:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

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

Audit hook: Route40 recovers the broad actual central-extension packet without using the seven Route39 split packet axioms.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_route40 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi), Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q)

The seven actual central-extension packet targets, tied to one Route40 same-family construction. This proves the Route39 packet shapes from the coherent extraspecial closer, not from the seven Route39 residual axioms.

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

Drop-in Route40 lower pushout provider.

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

Determinant packet projection through the Route40 lower pushout provider.

Acceptance checks / exact residual report