Route98 minimal-block pushout/determinant closer

This sidecar is a Route98-facing drop-in for the current integrated pushout provider

• minimalBlock_preheadDeterminantPackets_from_finalClosers.

It does not edit IntegratedCurrentRouteProofs98. Instead it lowers the broad actual-central-extension residual

• minimalBlock_preheadActualCentralExtensionPushoutData

to the Route82 manuscript-shaped simple-head determinant surface:

• construction of the scalar central-pushout pairing family;
• naturality of that family;
• annihilation of T by the extraspecial square;
• nonsingularity after descent to the simple head.

Manuscript anchor: reference/q2_manuscript.tex, Section 7, K_lambda = K / ker lambda and prop:simpleheaddet.

def Q2Presentation.Induction.MinimalBlockPushoutRoute98Closers.actualCentralExtensionPushoutDataOfRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Route82's coherent scalar-pushout packet reassembled as the broad actual central-extension pushout packet expected by the older final closer.

The square family is fixed to the extraspecial square attached to the same phi_lambda. The radical-containment field is recovered from Route82's descended nonsingularity, exactly as in the Route82 projection to Route81.

Equations

• One or more equations did not get rendered due to their size.

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

Route98 lowering of the broad actual central-extension pushout residual.

Its non-local closure is the four Route82 simple-head determinant packets, not minimalBlock_preheadActualCentralExtensionPushoutData.

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

Route98 lower pushout packet, projected through the same Route82 data.

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

Drop-in determinant-packet replacement for Route98 integration.

This has the same conclusion as minimalBlock_preheadDeterminantPackets_from_finalClosers, but its closure routes through Route82's four manuscript-shaped pushout/determinant packets.