Route36 minimal-block pushout/determinant provider

Route35 exposes five independent Section 7 pushout/determinant residuals:

• minimalBlock_preheadCentralPushoutSelfDualityData;
• minimalBlock_preheadExtraspecialNaturalityData;
• minimalBlock_preheadExtraspecialDiagonalZeroData;
• minimalBlock_preheadExtraspecialPolarZeroData;
• minimalBlock_preheadExtraspecialRadicalContainmentData.

This sidecar exports a route-compatible lower pushout provider whose closure does not use those five residuals. It routes through the coherent actual extraspecial construction in MinimalBlockExtraspecialClosers3, where the old five packet boundaries are projections from one same-family central-pushout square/polar family and one simple-head determinant theorem for that family.

The remaining nonlocal floor for this route is therefore strictly lower and smaller:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

No routed file imports this sidecar yet.

Route36 pushout hooks

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

Route36 actual central-extension packet.

This has the same conclusion as the route35 audit hook, but its axiom closure is the coherent actual extraspecial floor from MinimalBlockExtraspecialClosers3 rather than the five Route35 pushout residuals.

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

Supervisor hook: route36 lower pushout data from the coherent actual extraspecial construction.

The theorem has the same shape as minimalBlock_preheadPushoutRouteLowerData_from_route35ActualCentralExtension, but it avoids the five route35 pushout residual axioms.

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

Determinant packet projection through the route36 lower pushout provider.

Acceptance checks / exact residual report