Route37 minimal-block pushout/determinant provider

Route36 leaves two Section 7 prehead central-pushout/determinant residuals:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

The manuscript separates these into smaller assertions. The scalar pushout first supplies one shared quadratic family together with the square-diagonal and polar-symmetry identities. The simple-head determinant theorem then asserts, for that same family, naturality, diagonal vanishing on T, polar vanishing on T x M, and polar-radical containment.

This Route37 sidecar does not claim a full proof of prop:simpleheaddet. Instead, it routes through the existing semantic split:

• the combined square/polar packet is recovered from the standard shared-family, square-diagonal, and polar-symmetry packets;
• the bundled actual simple-head determinant packet is recovered from the coherent semantic determinant packet, which itself consists of the four manuscript-shaped same-family determinant assertions above.

Thus the exported lower-route provider has the same conclusion as the Route36 provider while avoiding both Route36 residual names.

Route37 pushout hooks

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

Route37 replacement for the combined central-pushout square/polar packet.

This closes the old combined residual over the stricter standard determinant packets: one quadratic family, square diagonal, and polar symmetry.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_route37 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Route37 replacement for the bundled actual simple-head determinant packet.

This avoids the old bundled residual by using the coherent semantic determinant packet for the same central-pushout family.

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

Supervisor hook: route37 lower pushout data from the square/polar and determinant semantic proof splits.

This is drop-in compatible with minimalBlock_preheadPushoutRouteLowerData_from_route36ActualSemanticPushout, but its axiom closure replaces the two Route36 pushout residuals by the smaller standard square/polar packets and coherent simple-head determinant semantic packets.

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

Determinant packet projection through the Route37 lower pushout provider.

Acceptance checks / exact residual report