Route15 semantic central-pushout reduction

This sidecar is deliberately local: it creates a route15 replacement hook for the §7 determinant/central-pushout cluster without editing the integrated route files.

The route14 pushout theorem currently bottoms out in seven route12 residuals:

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

Manuscript §7 constructs the scalar pushout K_lambda = K / ker lambda. Once the central-pushout pairing phi_lambda is available, the square used by the route is the extraspecial square form attached to that same pairing, so the quadratic family, square-diagonal identity, and polar-symmetry identity are already theorem-level projections from MinimalBlockPreheadCentralPushoutSemanticData.

The resulting route15 floor is therefore strictly smaller than the route12 cluster: it still needs the missing semantic phi_lambda family and the same-family prop:simpleheaddet semantic facts, but it does not assume the separate square/diagonal/polar packets.

One same-family route15 packet

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

Route15 central-pushout data.

The determinant field is indexed by the same semantic family as semantic. This prevents the route from mixing a phi_lambda family from one residual with simple-head determinant facts for another family.

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

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

The route15 semantic family already determines the split quadratic family: the square is the extraspecial form attached to phi_lambda.

Equations

• P.quadraticFamily = P.semantic.toQuadraticFamily

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

The square-diagonal identity is definitional for the extraspecial square.

Equations

• ⋯ = ⋯

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

The polar-symmetry identity is definitional for the extraspecial square.

Equations

• ⋯ = ⋯

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

Convert the same-family split determinant pieces to the current actual simple-head determinant packet.

Equations

• ⋯ = ⋯

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

Project route15 data to the existing lower pushout packet consumed by route14.

Equations

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

Route15 constructors and projection hooks

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

Assemble the same-family route15 packet.

The only non-local inputs used here are the semantic central-pushout family and the four same-family semantic determinant facts from prop:simpleheaddet. Notably, this does not call the route12 quadratic-family, square-diagonal, or polar-symmetry residuals.

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

Route15 replacement for the three square/polar packet residuals.

It exposes the square family, square-diagonal identity, and polar-symmetry identity as projections from the route15 semantic family.

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

Route15 lower pushout packet compatible with the route14 consumption site.

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

Determinant packet projection from the route15 lower pushout theorem.

Acceptance checks / residual report