Route29 minimal-block pushout/determinant refinement

Route28 exposes the Section 7 pushout/determinant frontier as seven same-family leaves:

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

This sidecar keeps route28's downstream lower-route shape, but replaces those semantic leaves by the actual central-extension split packets from MinimalBlockActualCentralExtensionPushoutProofs. The route28 packets become theorem-level projections from one same-family actual scalar central-extension pushout datum: the phi_lambda family, its square maps, diagonal and polar identities, naturality, annihilation on T, and radical containment.

Manuscript anchors: Section 7, especially prop:simpleheaddet, and the Section 8 radical-edge/Fourier use of the descended scalar pushouts.

Route29 actual central-extension split packet

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

Route29 data assembled from the actual central-extension split packets.

The single field is intentionally the broad actual packet, but the constructor below obtains it through minimalBlock_preheadActualCentralExtensionPushoutData_from_splitPackets, so the provider closure is the exact split-packet frontier and not the broad actual packet axiom.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The route29 semantic central-pushout family.

Equations

• P.semantic = P.actual.toSemanticData

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

The route28 quadratic-family leaf, projected from the route29 actual packet.

Equations

• P.quadraticFamily = P.actual.toQuadraticFamily

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

The route28 square-diagonal leaf, projected from the same route29 actual square map.

Equations

• ⋯ = ⋯

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

The route28 polar-symmetry leaf, projected from the same route29 actual square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute29ActualCentralExtensionSplitData.actualScalar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D) : MinimalBlockPreheadActualScalarCentralPushoutData D

The actual scalar packet selected by route29.

Equations

• P.actualScalar = P.actual.toActualScalarData

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

Route28 semantic naturality, projected from actual central-extension naturality.

Equations

• ⋯ = ⋯

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

Route28 diagonal-zero packet, obtained from actual annihilation on T plus the actual diagonal identity.

Equations

• ⋯ = ⋯

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

Route28 polar-zero packet, obtained from actual annihilation on T plus the actual polar identity.

Equations

• ⋯ = ⋯

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

Route28 radical-containment packet, obtained from the actual polar radical containment after rewriting by the actual polar identity.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute29ActualCentralExtensionSplitData.determinantSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData P.semantic

Route28's split determinant packet, reconstructed without using any route28 semantic determinant leaf axiom.

Equations

• ⋯ = ⋯

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

The bundled actual determinant packet for the same route29 semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute29ActualCentralExtensionSplitData.toRoute28Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D) : MinimalBlockPushoutRoute28ActualScalarSplitDeterminantData D

Route29 data repackaged in route28's provider structure.

Equations

• P.toRoute28Data = { actualScalar := P.actualScalar, determinantPieces := ⋯ }

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

Route29 projected to the lower pushout route in route28's downstream shape.

Equations

• P.toPushoutRouteLower = P.toRoute28Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route29 actual central-extension split data.

Residual report: this theorem uses the split actual central-extension packets from MinimalBlockActualCentralExtensionPushoutProofs; it does not call any of route28's seven semantic pushout leaves.

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

Route28-compatible packet constructed through route29's actual central-extension split.

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

Supervisor hook: route28-shaped lower pushout provider from route29 actual central-extension split data.

theorem Q2Presentation.Induction.minimalBlock_pushoutRoute28Leaves_from_route29ActualCentralExtensionSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semantic)

Explicit route28-leaf projection report through route29.

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

Determinant packet projection through the route29 lower pushout theorem.

Acceptance checks / exact residual report