Scalar central-pushout comparison closers

This sidecar narrows the current Section 7 scalar central-pushout square/polar closure without editing routed files.

Manuscript anchor: Section 7, pages 41--42. For a nonzero scalar character lambda : R -> F_2, the pushout K_lambda = K / ker lambda has square map q_lambda and polar form b_lambda. The existing API exposes this as either:

• one coherent square/polar packet MinimalBlockPreheadCentralPushoutSquarePolarData, or
• the current final-route split into a quadratic family, square diagonal, polar symmetry, and an extra comparison packet.

The comparison packet is theorem-level from the square and polar identities: two QuadF2 objects with the same form and polar map are equal. Consequently the actual scalar-pushout packet can be recovered from the coherent square/polar packet alone, replacing the four independent final-closure packets by one manuscript-shaped residual.

No routed file imports this sidecar yet.

Quadratic-form extensionality

theorem Q2Presentation.Induction.minimalBlock_quadF2_ext_form_polar {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (q r : Quadratic.QuadF2 V) (hform : ∀ (v : V), q.form v = r.form v) (hpolar : ∀ (v w : V), (q.polar v) w = (r.polar v) w) : q = r

A QuadF2 is determined by its form and polar map.

Close the comparison packet from the current square/polar split

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

The actual-scalar/extraspecial comparison is forced by the square diagonal and polar-symmetry fields of the standard pushout packet.

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

Replacement for minimalBlock_preheadActualScalarCentralPushoutData_proven that removes the separate comparison axiom from the closure. It still uses the current three split square/polar packets through minimalBlock_preheadCentralPushoutStandardData_from_packets.

Project the coherent square/polar packet to the current split packets

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSquarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSquarePolarData D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

Project the coherent square/polar packet to the split quadratic-family packet.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSquarePolar S = { phi := S.phi, square := S.square }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquareDiagonalData.ofSquarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSquarePolarData D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSquarePolar S)

Project the coherent square/polar packet to the split square-diagonal packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarSymmData.ofSquarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSquarePolarData D) : MinimalBlockPreheadCentralPushoutPolarSymmData (MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSquarePolar S)

Project the coherent square/polar packet to the split polar-symmetry packet.

Equations

• ⋯ = ⋯

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

Repackage the coherent square/polar packet as the current standard packet.

Equations

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

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

Residual-backed projection of the coherent square/polar packet to the current standard split packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPackets_from_squarePolarData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

Coherent replacement hook for the current split quadratic/square/polar packets.

Actual scalar packet from one coherent square/polar residual

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

Assemble the actual scalar central-pushout packet directly from the coherent square/polar packet. The scalar quotient surjectivity is elementary over F_2; the extraspecial comparison is forced by form/polar extensionality.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadActualScalarCentralPushoutData.ofSquarePolar S = { phi := S.phi, square := S.square, scalar_quotient_surjective := ⋯, square_is_extraspecial := ⋯ }

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

Route-ready replacement for minimalBlock_preheadActualScalarCentralPushoutData_proven.

Its axiom closure replaces the four independent current packets minimalBlock_preheadActualScalarCentralPushoutComparisonData, minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, and minimalBlock_preheadCentralPushoutPolarSymmData by the one coherent residual minimalBlock_preheadCentralPushoutSquarePolarData.

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

Route-ready replacement for minimalBlock_preheadCentralPushoutSemanticData_from_actualScalarPushoutProofs using the coherent square/polar residual.

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

Route-level lower packet through the coherent square/polar residual.