Route20 minimal-block pushout sidecar

Route19 exposes seven independent Section 7 pushout/determinant residuals: three central-pushout square/polar packets and four extraspecial determinant packets.

Route20 routes the same lower pushout target through the actual central-extension pushout packet from MinimalBlockCentralPushoutFinalClosers. That packet is the manuscript-shaped object for the scalar pushouts K_lambda = K / ker lambda: it carries the same-family pairing, square map, diagonal/polar identifications, naturality, annihilation on T, and radical containment. The theorem-level projections below recover the route19-facing standard, actual determinant, and lower pushout packets from that one packet.

One actual-pushout route packet

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

Route20 actual determinant data.

This keeps the scalar central-extension pushout construction and the simple-head determinant assertions tied to one actual same-family pushout packet. It is deliberately a wrapper around the final closer's actual pushout data, so route20 introduces no new axiom declaration of its own.

• actualPushout : MinimalBlockPreheadActualCentralExtensionPushoutData D

def Q2Presentation.Induction.MinimalBlockPushoutRoute20ActualDeterminantData.standard {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute20ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutStandardData D

The standard same-family square/polar packet projected from Route20.

Equations

• P.standard = P.actualPushout.toStandardData

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

The semantic family underlying the Route20 determinant packet.

Equations

• P.semantic = P.actualPushout.toSemanticData

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

The actual scalar pushout packet projected from Route20.

Equations

• P.actualScalar = P.actualPushout.toActualScalarData

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

The actual determinant packet for the same Route20 semantic family.

Equations

• ⋯ = ⋯

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

Route20 data repackaged as the lower pushout route packet consumed by the integrated nonterminal branch.

Equations

• P.toPushoutRouteLower = { selfDuality := P.semantic.toSelfDuality, simpleHeadDeterminant := ⋯ }

Assembly and route-compatible hooks

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

Assemble Route20 data from the actual central-extension pushout packet.

The nonstandard axiom closure of this theorem is the single existing residual minimalBlock_preheadActualCentralExtensionPushoutData, not the seven Route19 pushout/determinant packet residuals.

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

Route20 replacement for the route19 standard square/polar source.

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

Route20 replacement for the route-relevant actual determinant packet.

As in route19, this supplies the actual packet for the semantic family selected by the same coherent construction, rather than for an arbitrary pre-existing semantic family.

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

Route20 lower pushout packet, suitable for supervisor integration in place of minimalBlock_preheadPushoutRouteLowerData_from_route19ActualDeterminant.

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

Determinant packet projection from the Route20 lower pushout theorem.

Acceptance checks / residual report