Route54 minimal-block pushout/determinant narrowing

Route53 replaces the older semantic pushout family by the split square/polar packets

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;

and keeps the actual simple-head determinant packet for the semantic family projected from those split packets.

This sidecar keeps Route53's provider surface, but replaces those four leaves by one same-family actual packet. The packet records the actual scalar central-pushout construction and the simple-head determinant theorem for its own semantic projection. Thus the square map, diagonal identity, polar identity, semantic family, and determinant theorem cannot come from unrelated choices.

Route54 coherent actual packet

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

Route54 actual pushout/determinant data for one pre-head tower.

Manuscript anchor: Section 7, prop:simpleheaddet. The actual scalar central-pushout data supplies the same-family phi_lambda and q_lambda; the determinant field states the simple-head determinant theorem for the semantic family obtained from exactly that actual scalar pushout.

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

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutActualDeterminantRoute54Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D)

Route54 residual: one coherent actual scalar-pushout plus same-family simple-head determinant packet.

This is the intended replacement for Route53's four independent pushout leaves.

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

The semantic central-pushout family selected by Route54.

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.quadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

The split quadratic family selected by the same actual scalar pushout.

Equations

• P.quadraticFamily = P.actualScalar.toQuadraticFamily

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.squareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily

The square-diagonal projection for the selected quadratic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.polarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily

The polar-symmetry projection for the selected quadratic family.

Equations

• ⋯ = ⋯

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

The selected actual determinant packet, reindexed to the semantic projection.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.toRoute53Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadDeterminantRoute53Data D

Route54 projected to the Route53 determinant data shape.

Equations

• P.toRoute53Data = { semantic := P.semantic, actualDeterminant := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.toRoute52Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadDeterminantRoute52Data D

Route54 projected to the Route52 determinant data shape.

Equations

• P.toRoute52Data = P.toRoute53Data.toRoute52Data

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data.toRoute50Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D) : MinimalBlockPreheadSimpleHeadDeterminantRoute50Data D

Route54 projected to the Route50 determinant packet shape.

Equations

• P.toRoute50Data = P.toRoute53Data.toRoute50Data

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

Route54 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLowerData = P.toRoute53Data.toPushoutRouteLowerData

Compatibility with the Route53 residual surface

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

The Route54 packet is also constructible from the current Route53 residuals.

This is a compatibility theorem: it shows Route54's coherent packet has exactly the same current mathematical content as Route53's selected split square/polar family plus actual determinant, but tied into one structure.

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

Route54 supplies the three Route53 square/polar residual targets from one coherent actual scalar-pushout packet.

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

Route54 supplies the selected semantic family and actual determinant packet used by Route53.

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

Route53-shaped determinant data supplied by the Route54 coherent packet.

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

Route52-shaped determinant data supplied by Route54.

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

Route50-shaped determinant data supplied by Route54.

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

Lower pushout route supplied by Route54.

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

Route54 determinant-packet provider.

This is the Route53 provider surface with the four Route53 pushout leaves replaced by the single coherent Route54 actual determinant leaf.

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

Explicit drop-in replacement name for auditing the Route53 provider surface.