Central-pushout self-duality proof boundary

This sidecar closes the old phi-only Section 7 packet MinimalBlockPreheadCentralPushoutSelfDualityData from the current semantic central-pushout API.

The present API still does not expose a literal normalized extension cocycle for the scalar central pushout. The narrowest available coherent source is MinimalBlockPreheadCentralPushoutSemanticData: one family phi_lambda, with the extraspecial square and polar maps induced from that same family by toQuadraticFamily, squareDiagonalData, and polarSymmData. The theorem below therefore replaces the old final-closure self-duality residual by that semantic central-pushout family, without introducing a dummy or zero pushout.

Self-duality from the semantic central-pushout family

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

Forget only the semantic square/polar interface, retaining the self-duality family consumed by the older extraspecial route.

The source S is the coherent Section 7 semantic central-pushout family. Its square map is still available as S.toQuadraticFamily; this projection merely adapts to the older phi-only packet boundary.

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

Preferred closure of the old central-pushout self-duality packet.

The remaining residual is the semantic central-pushout family, not the old minimalBlock_preheadCentralPushoutSelfDualityData axiom. This is the strongest closure available in the current API, because no field yet records the actual normalized extension cocycle of K_lambda = K / ker lambda.

Downstream route hook

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

Route-level reassembly using the new self-duality proof boundary.

This is the same construction as minimalBlock_preheadPushoutRouteLowerData_proven, but its self-duality field is supplied by minimalBlock_preheadCentralPushoutSelfDualityData_proven. Its axiom closure should therefore expose minimalBlock_preheadCentralPushoutSemanticData instead of the old minimalBlock_preheadCentralPushoutSelfDualityData axiom.