Route34 minimal-block pushout/determinant provider

Route33 uses the route31 provider, whose pushout frontier is the four same-family central-pushout leaves

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar gives a route31-compatible provider from one coherent manuscript packet: the actual scalar central-extension family K_lambda = K / ker lambda. That packet already contains the phi_lambda family, the actual square map, the diagonal and polar identities, naturality, and the simple-head determinant annihilation/radical conclusions. The route34 hook projects those fields back into route31's standard square/polar plus actual determinant interface, so the four route33 residual names disappear from the provider closure.

For coordinators who prefer the finer Section 7 split, this file also exports a route34-named hook through the seven split actual central-extension packets from MinimalBlockActualCentralExtensionPushoutProofs.

Route34 actual central-extension packet

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

Route34 data: the actual scalar central-extension pushout family, retained as one coherent manuscript-shaped object and then projected to route31's standard determinant interface.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

def Q2Presentation.Induction.MinimalBlockPushoutRoute34ActualCentralExtensionData.standard {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute34ActualCentralExtensionData D) : MinimalBlockPreheadCentralPushoutStandardData D

The route31 standard square/polar packet projected from the actual central-extension family.

Equations

• P.standard = P.actual.toStandardData

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

The route31 semantic family selected by route34.

Equations

• P.semantic = P.standard.semanticData

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

The actual simple-head determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute34ActualCentralExtensionData.toRoute31Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute34ActualCentralExtensionData D) : MinimalBlockPushoutRoute31ActualSemanticDeterminantData D

Route34 repackaged in route31's provider structure.

Equations

• P.toRoute31Data = { standard := P.standard, actualDeterminant := ⋯ }

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

Lower pushout route inherited from route31's downstream projection.

Equations

• P.toPushoutRouteLower = P.toRoute31Data.toPushoutRouteLower

Route-compatible hooks

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

Construct the route34 coherent actual central-extension packet.

Residual report: this theorem replaces the four route33 pushout leaves by the single actual central-extension pushout construction minimalBlock_preheadActualCentralExtensionPushoutData.

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

Route31-compatible provider data from the route34 actual central-extension packet.

theorem Q2Presentation.Induction.minimalBlock_route33CentralPushoutLeaves_from_route34ActualCentralExtension {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute34ActualCentralExtensionData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData P.standard.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData P.standard.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.semantic)

The route33 central-pushout leaves, all projected from the same route34 actual central-extension packet. This is an audit hook showing that the quadratic family, square diagonal, polar symmetry, and actual determinant are same-family consequences of one actual pushout object.

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

Supervisor hook: lower pushout route from the route34 actual central-extension provider.

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

Determinant packet projection through the route34 lower pushout provider.

Finer split-packet fallback

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

Route34-named lower provider through the finer seven-packet actual central-extension split.

This hook is not the main "fewer residuals" route34 provider. It is exported so the supervisor can choose the strictly finer manuscript-shaped frontier if the single coherent actual central-extension packet is considered too broad for the next integration step.

Acceptance checks / exact residual report