Route12 central-pushout residual refinement

This sidecar leaves the routed files untouched. It refines the two route12 Section 7 residuals

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData;

into one same-family packet: an actual scalar central-pushout square/polar family, plus the simple-head determinant pieces for the semantic family induced by that exact scalar pushout.

The route-ready theorem exported below has the same lower-pushout conclusion used by IntegratedCurrentRouteProofs12, so integration only needs an import and a theorem-name swap in the route file.

One route12 central-pushout packet

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

Same-family route12 central-pushout data.

The actualScalar field supplies the concrete scalar pushout square/polar family. The determinant pieces are indexed by actualScalar.toSemanticData, so the square/polar and determinant sides cannot drift to unrelated central-pushout families.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• determinantPieces : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData self.actualScalar.toSemanticData

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

Project the route12 packet to the current combined square/polar target.

Equations

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

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

The semantic central-pushout family attached to the actual scalar packet.

Equations

• P.toSemanticData = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute12Data.toActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute12Data D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.toSemanticData

Project the route12 determinant pieces to the current actual determinant target for the route12 semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute12Data.toExtraspecialActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute12Data D) : MinimalBlockPreheadCentralPushoutExtraspecialActualData D

Project route12 data to the coherent actual extraspecial packet consumed by the route10 actual-central-extension interface.

Equations

• P.toExtraspecialActual = { phi := P.toSemanticData.phi, phi_natural := ⋯, square_annihilates_on_T := ⋯, square_radical_subset_T := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute12Data.toRoute10Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute12Data D) : MinimalBlockPreheadActualCentralExtensionRoute10Data D

Package the route12 extraspecial actual packet as route10 data.

Equations

• P.toRoute10Data = { actual := P.toExtraspecialActual }

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

Lower pushout data projected through the route10 interface.

Equations

• P.toPushoutRouteLower = P.toRoute10Data.toPushoutRouteLower

Theorem-level route12 closures

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

Construct the same-family route12 packet from refined square/polar and determinant sidecars.

This theorem does not use the old combined square/polar axiom or the old bundled actual determinant axiom.

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

Current square/polar target projected from the route12 same-family packet.

This is the route12 replacement for minimalBlock_preheadCentralPushoutSquarePolarData.

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

Route-relevant actual determinant target for the same semantic family induced by the route12 scalar pushout.

This refines the old arbitrary-family residual minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData to the family actually used by the lower pushout route.

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

Coherent actual extraspecial central-pushout packet through route12, avoiding the old square/polar and actual determinant residual names.

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

Route10 actual-central-extension data through route12.

This is the direct replacement for minimalBlock_preheadActualCentralExtensionRoute10Data when auditing the two route12 central-pushout residuals.

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

Route-ready lower pushout packet compatible with IntegratedCurrentRouteProofs12.

To integrate, import this module in IntegratedCurrentRouteProofs12 and replace the current call to minimalBlock_preheadPushoutRouteLowerData_from_route10Proofs with this theorem.

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

Determinant packet projection from the route12 lower pushout theorem.

Acceptance checks / residual report