Route53 minimal-block pushout/determinant narrowing

Route52 closes the determinant side from one semantic central-pushout family plus four semantic prop:simpleheaddet packets:

• minimalBlock_preheadCentralPushoutSemanticData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

This sidecar keeps the Route52 provider surface but routes it through the same-family actual determinant packet already present in the Section 7 API. The remaining determinant obligations are the concrete square/polar central-pushout packets and the actual simple-head determinant theorem for that same projected semantic family.

Route53 determinant data

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

Route53 determinant data for one pre-head tower.

The semantic family is produced from the concrete scalar central-pushout square/polar data, and actualDeterminant is prop:simpleheaddet for exactly that same family. Route52's four semantic determinant pieces are theorem-level projections from this single actual packet.

• semantic : MinimalBlockPreheadCentralPushoutSemanticData D
• actualDeterminant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData self.semantic

def Q2Presentation.Induction.MinimalBlockPreheadDeterminantRoute53Data.route52DeterminantPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadDeterminantRoute53Data D) : MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces P.semantic

Route52's four semantic determinant fields, projected from Route53's one actual determinant packet for the same semantic central-pushout family.

Equations

• ⋯ = ⋯

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

Repackage Route53 data as the Route52 determinant packet shape.

Equations

• P.toRoute52Data = { semantic := P.semantic, determinantPieces := ⋯ }

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

Repackage Route53 data as the old Route50 packet shape.

Equations

• P.toRoute50Data = P.toRoute52Data.toRoute50Data

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

Repackage Route53 data directly as the lower pushout route packet.

Equations

• P.toPushoutRouteLowerData = P.toRoute52Data.toPushoutRouteLowerData

Route-compatible hooks

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

Construct Route53 determinant data from the concrete square/polar pushout family and the actual simple-head determinant packet for the same semantic family.

The axiom closure avoids all five Route52 semantic pushout leaves.

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

Route52-shaped determinant data supplied by Route53's narrower actual packet route.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSemanticPackets_from_route53 {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 five Route52 semantic leaves, narrowed to one same-family actual determinant packet plus the concrete square/polar pushout family.

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

Lower pushout route from Route53's actual determinant packet.

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

Route53 determinant-packet projection.

This is the drop-in replacement for minimalBlock_preheadDeterminantPackets_from_route52; its closure avoids the five semantic Route52 pushout leaves.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_from_route52_via_route53 {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 Route52 provider surface.