Route26 minimal-block pushout/determinant refinement

Route25 exposes the Section 7 pushout frontier as seven same-family leaves:

• the scalar pushout square/polar side: minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, and minimalBlock_preheadCentralPushoutPolarSymmData;
• the determinant side of prop:simpleheaddet: minimalBlock_preheadCentralPushoutNaturalitySemanticData, minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData, minimalBlock_preheadCentralPushoutPolarZeroSemanticData, and minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

This sidecar keeps route25's lower-route output shape, but replaces the four determinant semantic leaves by the stricter same-family actual determinant packet

• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

The actual determinant packet is indexed by the semantic family projected from the same actual scalar central pushout used for the square/polar side, so the route26 data still has the same K_lambda = K / ker lambda family on both sides.

Route26 same-family actual determinant packet

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

Route26 actual determinant data.

The square/polar side is the actual scalar central-pushout family. The determinant side is the actual simple-head determinant packet for exactly the semantic family projected from that scalar pushout.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• actualDeterminant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData self.actualScalar.toSemanticData

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

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

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semantic

Project semantic naturality from the same-family actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.diagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semantic

Project diagonal vanishing on T from the same-family actual determinant annihilation packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.polarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semantic

Project polar vanishing on T x M from the same-family actual determinant annihilation packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.radicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semantic

Project polar-radical containment from the same-family actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.determinantSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData P.semantic

Route25's split determinant packet, projected from route26's actual determinant packet without using the four route25 semantic determinant axioms.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute26ActualDeterminantData.toRoute25Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute26ActualDeterminantData D) : MinimalBlockPushoutRoute25ActualCentralExtensionData D

Route26 data repackaged in route25's exact provider structure.

Equations

• P.toRoute25Data = { actualScalar := P.actualScalar, determinantPieces := ⋯ }

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

Broad actual central-extension pushout data recovered theorem-level through route25's projection chain.

Equations

• P.toActualPushout = P.toRoute25Data.toActualPushout

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

Route26 data projected to the lower pushout route in route25's output shape.

Equations

• P.toPushoutRouteLower = P.toRoute25Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route26 actual determinant data.

The square/polar side uses the current standard scalar-pushout proof split. The determinant side is left as the stricter actual determinant packet for that same projected semantic family, replacing the four independent route25 determinant semantic leaves.

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

Route25-compatible packet, constructed through route26's actual determinant packet.

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

Broad actual central-extension packet recovered through route26.

This theorem is compatibility glue only; the proof does not call the broad actual central-extension pushout axiom.

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

Supervisor hook: route25-shaped lower pushout provider from route26 actual determinant data.

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

Determinant packet projection through the route26 lower pushout theorem.

Acceptance checks / exact residual report