Route55 minimal-block pushout/determinant refinement

Route54 leaves one bundled non-local packet:

• minimalBlock_preheadCentralPushoutActualDeterminantRoute54Data.

This sidecar proves that packet from the existing split actual central-extension pushout packets. The split packets are exactly the manuscript-shaped Section 7 data around prop:simpleheaddet: the actual phi_lambda family, the actual square maps q_lambda, the diagonal and polar identities, naturality, annihilation on T, and polar-radical containment.

No routed file imports this sidecar yet. The theorem minimalBlock_preheadCentralPushoutActualDeterminantRoute54Data_from_route55SplitPackets is the drop-in Route55 provider for the old Route54 leaf, with no use of the Route54 bundled axiom.

Projection from actual central-extension data to the Route54 packet

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

Repackage one actual central-extension pushout construction as the Route54 same-family actual scalar/determinant packet.

Equations

• P.toRoute54Data = { actualScalar := P.toActualScalarData, actualDeterminant := ⋯ }

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

Theorem-level projection from an already constructed actual central-extension pushout to the Route54 bundled packet.

Route55 split-packet provider

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

Route55 replacement for the Route54 bundled residual.

Its axiom closure uses the existing split actual central-extension packets:

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

It does not use minimalBlock_preheadCentralPushoutActualDeterminantRoute54Data.

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

Route53-shaped determinant data supplied by Route55 split packets.

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

Route52-shaped determinant data supplied by Route55 split packets.

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

Route50-shaped determinant data supplied by Route55 split packets.

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

Lower pushout route supplied by Route55 split packets.

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

Determinant-packet provider supplied by Route55 split packets.

This is the Route54 provider surface with the single Route54 bundled leaf refined to the split actual central-extension pushout packets above.

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

Explicit drop-in replacement name for auditing the Route54 provider surface.