Route106 minimal-block pushout/determinant closer

IntegratedCurrentRouteProofs106 still consumes the Route101 pushout provider

• MinimalBlockPushoutRoute101Closers.minimalBlock_preheadDeterminantPackets_from_route101,

whose current pushout frontier is the five older self-duality/extraspecial packets:

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

This sidecar leaves every routed file untouched and supplies a Route106-named drop-in provider with the same output shape. It routes through the manuscript level actual packets instead:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

These are the scalar pushouts K_lambda = K / ker lambda and the simple-head determinant theorem of manuscript Section 7, prop:simpleheaddet.

Route106 drop-in pushout provider

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

Route106 lower pushout packet from the actual scalar central-pushout family and the actual simple-head determinant theorem for its semantic projection.

The axiom closure replaces the five Route101 pushout leaves by the two manuscript-shaped actual packets named in the module header.

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

Drop-in determinant-packet replacement for the Route106 pushout line.

This has the same conclusion as MinimalBlockPushoutRoute101Closers.minimalBlock_preheadDeterminantPackets_from_route101, but its closure no longer contains the five Route106 pushout residual leaves.