Route17 actual central-pushout / determinant sidecar

Route16 exposes two Section 7 pushout leaves:

• minimalBlock_preheadCentralPushoutSemanticData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar replaces the route-relevant use of both leaves by one coherent actual central-extension pushout packet, itself supplied by the narrower split packets in MinimalBlockActualCentralExtensionPushoutProofs:

• actual phi_lambda;
• actual square map;
• diagonal identity;
• polar identity;
• naturality;
• annihilation on T;
• radical containment.

The bundled Route17 theorem has the same conclusion as Route16's lower pushout hook, so it can be used at the Route16 consumption site without changing any shared closer.

Route17 same-family actual packet

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

Route17 central-pushout data.

The semantic family and actual simple-head determinant packet are both projected from one actual central-extension pushout construction. This rules out drift between the semantic phi_lambda family and the determinant square used on the simple head.

• actualPushout : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The semantic central-pushout family projected from the actual pushout.

Equations

• P.semantic = P.actualPushout.toSemanticData

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

The actual simple-head determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute17ActualDeterminantData.extraspecialSimpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute17ActualDeterminantData D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality P.semantic.toSelfDuality)

The extraspecial simple-head determinant packet consumed by the lower route.

Equations

• ⋯ = ⋯

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

Convert Route17 data to the lower pushout packet consumed by the route.

Equations

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

Route17 constructors and projections

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

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

The axiom closure of this theorem should contain only the split actual-central-extension residuals, not either Route16 pushout residual.

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

Route17 replacement for the semantic central-pushout residual.

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

Route17 actual determinant packet for the route-relevant semantic family.

This deliberately proves the bundled actual packet for the same S constructed from the actual pushout, rather than for an arbitrary pre-existing semantic family.

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

Route17 lower pushout packet compatible with the Route16 consumption site.

This is the preferred replacement hook for minimalBlock_preheadPushoutRouteLowerData_from_route16ActualDeterminant.

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

Determinant packet projection from the Route17 lower pushout theorem.

Acceptance checks / residual report