Route19 minimal-block pushout square-polar/determinant sidecar

Route18 left two coherent Section 7 pushout residuals:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar replaces that two-residual surface by the stricter finite linear-algebra packets already exposed by the Section 7 API:

• one standard same-family square/polar packet;
• extraspecial naturality, diagonal-zero, polar-zero, and radical-containment packets for that same family.

The supervisor-facing hook is minimalBlock_preheadPushoutRouteLowerData_from_route19ActualDeterminant.

Route19 same-family determinant packet

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

Route19 pushout data.

The standard field carries the concrete square/polar family, while determinantSplit carries the simple-head determinant assertions for standard.semanticData. This keeps the square-polar and determinant sides on the same phi_lambda family.

• standard : MinimalBlockPreheadCentralPushoutStandardData D
• determinantSplit : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData self.standard.semanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute19ActualDeterminantData.squarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute19ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutSquarePolarData D

The Route18 square/polar packet projected from Route19 standard data.

Equations

• P.squarePolar = Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofStandardData P.standard

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

The semantic family underlying the Route19 determinant packet.

Equations

• P.semantic = P.standard.semanticData

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

The actual determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute19ActualDeterminantData.toRoute18ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute19ActualDeterminantData D) : MinimalBlockPushoutRoute18ActualDeterminantData D

Route19 data repackaged as the Route18 coherent packet.

Equations

• P.toRoute18ActualDeterminant = { squarePolar := P.squarePolar, determinantActual := ⋯ }

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

Route19 lower pushout packet, via the existing Route18 projection code.

Equations

• P.toPushoutRouteLower = P.toRoute18ActualDeterminant.toPushoutRouteLower

Assembly from stricter manuscript-shaped packets

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

Assemble Route19 data from the lower standard square/polar and extraspecial determinant packets.

The axiom closure of this theorem avoids both Route18 residuals and avoids the four broad semantic simple-head determinant residuals.

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

Route19 replacement for the Route18 square/polar residual.

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

Route19 replacement for the route-relevant actual determinant residual.

As in Route18, this supplies the actual packet for the semantic family selected by the same coherent square/polar construction, rather than for an arbitrary pre-existing semantic family.

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

Route19 lower pushout packet, suitable for supervisor integration.

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

Determinant packet projection from the Route19 lower pushout theorem.

Acceptance checks / residual report