Route35 minimal-block pushout/determinant provider

Route34's pushout branch still depends on the broad residual minimalBlock_preheadActualCentralExtensionPushoutData.

This sidecar keeps the route34-facing conclusion, but obtains the actual central-extension packet from the existing extraspecial/self-duality closers in MinimalBlockActualCentralExtensionClosers2. Consequently the route35 lower provider has no dependency on the broad route34 residual and no dependency on the seven split actual-central-extension residuals; its remaining closure is the more explicit extraspecial/self-duality determinant floor.

Route35 actual central-extension packet

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

Route35 data: the actual central-extension pushout packet, supplied through the existing extraspecial/self-duality closer rather than through the broad route34 axiom.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The semantic central-pushout family selected by route35.

Equations

• P.semantic = P.actual.toSemanticData

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

The actual determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

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

Route35 data projected to the lower pushout route consumed by the integrated nonterminal branch.

Equations

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

Route-compatible hooks

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

Construct route35 actual central-extension data from the existing extraspecial/self-duality closers.

Residual report: this theorem avoids minimalBlock_preheadActualCentralExtensionPushoutData and the seven split actual-central-extension packet axioms. Its remaining nonstandard closure is the explicit extraspecial/self-duality floor exposed by MinimalBlockActualCentralExtensionClosers2.

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

Broad actual central-extension packet recovered through route35.

This is exported as an audit hook: the conclusion matches the route34 residual, but the proof does not call the route34 broad residual axiom.

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

Supervisor hook: lower pushout route from route35's actual central-extension provider.

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

Determinant packet projection through the route35 lower pushout provider.

Acceptance checks / exact residual report