Route42 minimal-block pushout/determinant provider

Route41 exposes the Section 7 pushout/determinant frontier as seven split same-family packet leaves:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

This sidecar routes the same lower pushout interface through the actual scalar central-pushout packet and the actual simple-head determinant packet for the semantic family projected from that same scalar pushout. Thus the seven Route41 leaf names disappear from the lower-provider closure, replaced by the two manuscript-shaped actual packets already present in the local Section 7 API:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

No new axiom is introduced here.

Route42 packet

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

Route42 same-family pushout/determinant data.

The determinant packet is indexed by the semantic family induced from actualScalar, so the scalar square/polar and determinant sides cannot drift to different central-pushout families.

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute42Data.standard {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute42Data D) : MinimalBlockPreheadCentralPushoutStandardData D

The standard square/polar packet projected from the actual scalar pushout.

Equations

• P.standard = P.actualScalar.toStandardData

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

The semantic family selected by Route42.

Equations

• P.semantic = P.standard.semanticData

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

The actual determinant packet reindexed by P.semantic.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute42Data.coherentDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute42Data D) : MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData P.semantic

The coherent Route41 determinant packet projected from the actual simple-head determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute42Data.toRoute41Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute42Data D) : MinimalBlockPushoutRoute41Data D

Route42 projected to the Route41 data shape.

Equations

• P.toRoute41Data = { standard := P.standard, determinant := ⋯ }

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

The combined square/polar packet recovered from the actual scalar pushout.

Equations

• P.squarePolar = Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofActualScalar P.actualScalar

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

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

Equations

• ⋯ = ⋯

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

Route42 projected to the lower pushout packet consumed by integration.

Equations

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

Route-compatible hooks

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

Construct Route42 data from the actual scalar pushout and actual same-family simple-head determinant packets.

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

Route42 supplies the Route41 packet shape without using the seven Route41 split packet leaves.

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

Route42 replacement for the Route40 combined square/polar packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquarePolarPackets_from_route42 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

The three Route41 square/polar packets, tied to the Route42 actual scalar central-pushout family.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSemanticDeterminantPackets_from_route42 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The four Route41 determinant semantic packets, tied to the Route42 actual scalar central-pushout family and projected from the actual determinant packet.

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

Drop-in Route42 lower pushout provider.

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

Determinant packet projection through the Route42 lower pushout provider.

Acceptance checks / exact residual report