Route21 minimal-block actual central-extension pushout sidecar

Route20 exposes the Section 7 pushout/determinant step through the single broad residual

• minimalBlock_preheadActualCentralExtensionPushoutData.

The older split-packet API in MinimalBlockActualCentralExtensionPushoutProofs already separates that manuscript construction into the same-family pieces used in the paper:

• the scalar central-pushout pairing phi_lambda;
• the actual square map q_lambda;
• the diagonal identity q_lambda(m) = phi_lambda(m,m);
• the polar identity;
• equivariance/naturality;
• annihilation on T;
• polar-radical containment in T.

This sidecar gives route21-named hooks for later integration. It reassembles the route20-facing lower pushout packet from those strictly finer residuals and does not use minimalBlock_preheadActualCentralExtensionPushoutData.

Route21 split actual-pushout packet

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

Route21 actual central-extension data, stored as split manuscript-shaped packets rather than as the broad route20 residual.

All fields are tied to the same phi_lambda/q_lambda family, so the projected route packet uses one coherent scalar central-extension pushout construction.

• phiData : MinimalBlockPreheadActualCentralExtensionPhiData D
• squareData : MinimalBlockPreheadActualCentralExtensionSquareData self.phiData
• diagonalData : MinimalBlockPreheadActualCentralExtensionDiagonalData self.squareData
• polarData : MinimalBlockPreheadActualCentralExtensionPolarData self.squareData
• naturalityData : MinimalBlockPreheadActualCentralExtensionNaturalityData self.phiData
• annihilationData : MinimalBlockPreheadActualCentralExtensionAnnihilationData self.squareData
• radicalContainmentData : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData self.squareData

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

Reassemble the broad packet from route21 split data. This is a definition, not an appeal to the old broad residual axiom.

Equations

• P.toActualPushout = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.ofSplitPackets P.phiData P.squareData ⋯ ⋯ ⋯ ⋯ ⋯

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

Route20-shaped determinant wrapper projected from the route21 split data. This lets the new hook reuse the already verified route20 projection code.

Equations

• P.toRoute20ActualDeterminant = { actualPushout := P.toActualPushout }

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

Standard same-family square/polar data projected from the split actual central-extension packet.

Equations

• P.standard = P.toRoute20ActualDeterminant.standard

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

Actual scalar central-pushout data projected from the split packet.

Equations

• P.actualScalar = P.toRoute20ActualDeterminant.actualScalar

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

The route-relevant actual determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

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

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

Equations

• P.toPushoutRouteLower = P.toRoute20ActualDeterminant.toPushoutRouteLower

Assembly and route-compatible hooks

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

Assemble route21 data from the split actual central-extension packets.

The nonstandard closure of this theorem is the seven split residuals from MinimalBlockActualCentralExtensionPushoutProofs, not the route20 broad packet.

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

Broad actual central-extension packet recovered from route21 split packets. This theorem exists for audits; the integration hook below consumes the lower route packet directly.

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

Route21 replacement for minimalBlock_preheadPushoutRouteLowerData_from_route20ActualDeterminant.

It has the same conclusion as the route20 hook, but replaces route20's broad actual-pushout residual by the finer split central-extension packets.

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

Alias with the route20 naming convention, for a one-line later integration swap.

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

Determinant packet projection from the route21 lower pushout theorem.

Acceptance checks / residual report