Route23 minimal-block pushout/determinant close-out

Route22 narrowed the Section 7 determinant/pushout branch to the two broad leaves

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar rebuilds the same route22-facing packet from finer current APIs:

• the standard same-family square/polar packets minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, and minimalBlock_preheadCentralPushoutPolarSymmData;
• the four semantic prop:simpleheaddet packets for the same projected actual scalar family: minimalBlock_preheadCentralPushoutNaturalitySemanticData, minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData, minimalBlock_preheadCentralPushoutPolarZeroSemanticData, and minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

Manuscript anchors: reference/q2_manuscript.tex, Section 7 prop:simpleheaddet and Section 8's Fourier bridge. The route23 packet keeps the square/polar family and determinant assertions tied to the same actual scalar central pushout, matching the paper's scalar quotients K_lambda = K / ker lambda.

Route23 same-family actual determinant packet

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

Route23 actual central-extension data.

The actualScalar field supplies the scalar central-pushout family and its square/polar comparison. The determinant split is indexed by actualScalar.toSemanticData, so the prop:simpleheaddet conclusions are for that same family, not for an arbitrary semantic packet.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• determinantPieces : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData self.actualScalar.toSemanticData

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

The semantic central-pushout family selected by the route23 scalar pushout.

Equations

• P.semantic = P.actualScalar.toSemanticData

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

The actual determinant packet for the same route23 semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute23ActualCentralExtensionData.toExtraspecialActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute23ActualCentralExtensionData D) : MinimalBlockPreheadCentralPushoutExtraspecialActualData D

Route23 data repackaged as the coherent extraspecial actual packet consumed by route22.

Equations

• P.toExtraspecialActual = { phi := P.actualScalar.phi, phi_natural := ⋯, square_annihilates_on_T := ⋯, square_radical_subset_T := ⋯ }

def Q2Presentation.Induction.MinimalBlockPushoutRoute23ActualCentralExtensionData.toRoute22Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute23ActualCentralExtensionData D) : MinimalBlockPushoutRoute22ActualCentralExtensionData D

Route23 data in route22's packet shape.

Equations

• P.toRoute22Data = { actual := P.toExtraspecialActual }

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

Route23 data in route21's split packet shape.

Equations

• P.toRoute21Data = P.toRoute22Data.toRoute21Data

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

Broad actual central-extension pushout data projected from route23.

Equations

• P.toActualPushout = P.toRoute22Data.toActualPushout

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

Route20-shaped actual determinant wrapper projected from route23.

Equations

• P.toRoute20ActualDeterminant = P.toRoute22Data.toRoute20ActualDeterminant

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

Lower pushout route packet projected from route23.

Equations

• P.toPushoutRouteLower = P.toRoute22Data.toPushoutRouteLower

Route23 constructors and route-compatible hooks

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

Construct route23 data from finer current square/polar and determinant APIs.

The nonstandard closure avoids both route22 broad leaves minimalBlock_preheadCentralPushoutSquarePolarData and minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

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

Route22-shaped actual central-extension data built from route23's finer same-family packet.

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

Route21 split actual central-extension data built through route23.

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

Broad actual central-extension packet recovered through route23.

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

The route-relevant actual determinant packet selected by route23.

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

Lower pushout route through route23's actual central-extension packet.

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

Alias using the route20/route22 determinant naming convention for a one-line supervisor swap.

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

Determinant packet projection through the route23 lower pushout theorem.

Acceptance checks / exact residual report