Route45 minimal-block pushout/determinant provider

Route44 reduces the Section 7 pushout branch to two actual central-pushout leaves:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar removes both names from the route provider closure. The square/polar target is reconstructed from the split standard central-pushout packets (phi_lambda, q_lambda), diagonal, and polar-symmetry data. The determinant target is reconstructed from the same semantic family using the four semantic prop:simpleheaddet packets: naturality, diagonal-zero, polar-zero, and radical-containment.

The resulting lower provider is integration-ready as a replacement for minimalBlock_preheadPushoutRouteLowerData_from_route44; no integrated/root route file imports this sidecar yet.

Route45 packet

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

Route45 data: one actual scalar central-pushout family and the actual simple-head determinant theorem for that same projected semantic family.

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

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

The semantic central-pushout family selected by Route45.

Equations

• P.semantic = P.actualScalar.toSemanticData

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

The selected square/polar packet, reconstructed from actual scalar data.

Equations

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute45Data.selfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute45Data D) : MinimalBlockPreheadCentralPushoutSelfDualityData D

The selected self-duality packet.

Equations

• P.selfDuality = P.semantic.toSelfDuality

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

The selected actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute45Data.extraspecialDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute45Data D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality P.selfDuality)

The selected extraspecial simple-head determinant packet.

Equations

• ⋯ = ⋯

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

The coherent actual extraspecial packet induced by Route45 data.

Equations

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute45Data.toRoute44Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute45Data D) : MinimalBlockPushoutRoute44Data D

Route45 projected to the Route44 packet shape.

Equations

• P.toRoute44Data = { extraspecial := P.toExtraspecialActual }

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

Route45 projected to the lower pushout packet consumed by integration.

Equations

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

Route-compatible hooks

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

Route45 replacement for the old square/polar leaf.

Residual report: this theorem avoids minimalBlock_preheadCentralPushoutSquarePolarData; it exposes the split standard square/polar packets instead.

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

Route45 replacement for the old actual determinant leaf.

Residual report: this theorem avoids minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData; it exposes the four semantic same-family determinant packets instead.

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

Construct Route45 data without using the two Route44 pushout leaves.

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

Route45 supplies the Route44 packet shape, with a strictly smaller closure than minimalBlock_pushoutRoute44Data_from_extraspecialActual.

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

Route45 replacement for the Route44 actual scalar packet.

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

Audit hook: the selected Route45 semantic family carries an actual simple-head determinant packet.

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

Drop-in Route45 lower pushout provider.

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

Determinant packet projection through the Route45 lower pushout provider.

Acceptance checks / exact residual report