Square/polar central-pushout proof hooks

This sidecar closes the MinimalBlockPreheadCentralPushoutSquarePolarData conclusion without using the old combined residual minimalBlock_preheadCentralPushoutSquarePolarData.

There are two route-ready sources:

• a standard same-family determinant packet MinimalBlockPreheadCentralPushoutStandardData, whose fields are exactly a shared (phi_lambda, q_lambda) family plus the diagonal and polar identities;
• the narrower actual scalar central-pushout packet, which records the scalar quotient and identifies its square with the extraspecial square of the same phi_lambda.

No routed/root file imports this sidecar yet.

Reconstruct the combined square/polar packet from split standard data

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofStandardData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) : MinimalBlockPreheadCentralPushoutSquarePolarData D

Reassemble the old combined square/polar packet from the standard same-family square/diagonal/polar packet.

This is theorem-level glue: it only forgets that the three fields were split apart, and introduces no new mathematical assumption.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofActualScalar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualScalarCentralPushoutData D) : MinimalBlockPreheadCentralPushoutSquarePolarData D

Project actual scalar central-pushout data to the combined square/polar packet.

The diagonal and polar identities follow by rewriting the actual scalar square as the extraspecial form attached to the same phi_lambda.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofActualScalar P = { phi := P.phi, square := P.square, square_diagonal := ⋯, polar_symm := ⋯ }

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

The combined square/polar packet is a theorem-level projection of the standard same-family square/diagonal/polar packet.

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

Residual-backed replacement for the old combined minimalBlock_preheadCentralPushoutSquarePolarData axiom, using only the split standard square/diagonal/polar packets.

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

The combined square/polar packet is a theorem-level projection of actual scalar central-pushout data.

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

Residual-backed square/polar closure from the actual scalar central-pushout packet. This replaces the old combined square/polar residual by the narrower actual scalar-pushout residual.

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

Route-ready square/polar closure through the current actual-scalar proof split. Its closure avoids the old combined square/polar axiom and instead uses the split standard packets plus the actual-scalar/extraspecial comparison packet from MinimalBlockActualScalarPushoutProofs.

Downstream hooks that avoid the old square/polar axiom

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

Actual scalar central-pushout data via the standard packet projection and the comparison theorem proved in MinimalBlockScalarPushoutComparisonProofs.

This is the same target as minimalBlock_preheadActualScalarCentralPushoutData_proven, but the theorem name records that the old combined square/polar residual is not used in the projection chain.

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

Semantic central-pushout data through the square/polar proof hooks, avoiding the old combined square/polar residual.

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

Lower pushout route through the square/polar proof hooks. The determinant side still uses the existing actual-packet projection; this theorem only removes the combined square/polar residual from the scalar central-pushout square/polar frontier.

Acceptance checks