Actual lower Section 7 pushout route

This sidecar closes the current coherent route packet MinimalBlockPreheadPushoutRouteLowerData from the existing lower Section 7 API.

The construction remains manuscript-shaped: one central-pushout self-duality family supplies the scalar pushouts, and the simple-head determinant packet is assembled from naturality plus diagonal, polar, and radical-containment conclusions for the same extraspecial family. The quadratic form is the genuine Quadratic.Extraspecial.extraspecialForm; no dummy or zero pushout is introduced.

Simple-head determinant from the existing concrete pushout packets

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_from_actualPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S))

The lower simple-head determinant packet follows from the existing concrete central-pushout/extraspecial packets, all on the same self-duality family.

This is the formal prop:simpleheaddet reassembly: naturality gives the C-equivariance field, diagonal and polar vanishing give q_lambda|_T = 0 and b_lambda(T,M)=0 for the actual extraspecial square map, and radical containment gives the nonsingularity input after descent to the simple head.

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

The coherent lower route packet is theorem-level from the existing concrete pushout/extraspecial API.

This removes the aggregate axiom minimalBlock_preheadPushoutRouteLowerData from the axiom closure of this sidecar theorem. The remaining closure exposes the finer manuscript residuals: central-pushout self-duality, naturality, diagonal zero, polar zero, and radical containment for one family.