Route16 semantic pushout/determinant reduction

Route15 bottoms out in one semantic central-pushout family plus four independent same-family semantic determinant facts:

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

This sidecar keeps route15's central-pushout family, but replaces the four determinant facts by the narrower manuscript-shaped actual simple-head determinant packet for that same family. In manuscript terms this is the prop:simpleheaddet packet for the scalar pushout K_lambda = K / ker lambda: naturality, vanishing on T, polar vanishing on T x M, and polar-radical containment are projected from the actual determinant square.

No routed file imports this sidecar yet.

One same-family route16 packet

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

Route16 central-pushout data.

The determinant field is the actual simple-head determinant packet for the same semantic family. This is strictly smaller than route15's route-ready closure: route15 expands the actual determinant packet through four semantic determinant axioms, while this packet keeps the actual determinant assertion as the next exposed manuscript boundary.

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Convert route16 data to the lower pushout packet consumed by the route.

Equations

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

Route16 constructors and exact semantic target projections

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

Assemble the route16 same-family packet.

The remaining non-local inputs are exactly the semantic central-pushout family and the actual simple-head determinant packet for that family.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutNaturalitySemanticData_from_route16ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S)

Route16 proof of the exact route15 naturality semantic target from the same-family actual determinant packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData_from_route16ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S)

Route16 proof of the exact route15 diagonal-zero semantic target from the same-family actual determinant packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarZeroSemanticData_from_route16ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S)

Route16 proof of the exact route15 polar-zero semantic target from the same-family actual determinant packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData_from_route16ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

Route16 proof of the exact route15 radical-containment semantic target from the same-family actual determinant packet.

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

All five route15 semantic pushout targets, with the four determinant targets projected from one actual determinant packet for the same S.

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

Route16 lower pushout packet compatible with the route15 consumption site.

This has the same conclusion as minimalBlock_preheadPushoutRouteLowerData_from_route15SemanticReduction, but its closure exposes the actual same-family determinant packet instead of the four independent semantic determinant packet axioms.

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

Determinant packet projection from the route16 lower pushout theorem.

Acceptance checks / residual report