Final semantic central-pushout closers

This sidecar targets the remaining Section 7 prehead central-pushout semantic packet

• minimalBlock_preheadCentralPushoutSemanticData.

Manuscript anchor: reference/q2_manuscript.tex, Section 7 pages 40--42 (eq:targettower, lem:simplehead, lem:collapse, and prop:simpleheaddet), as consumed in Section 8 by the radical-edge/descent and Fourier packets.

The existing group-tower/provenance APIs expose the tower R, M, T, C and the actions, but they do not expose an actual quotient object K_lambda = K / ker lambda or its square/commutator maps. The residual below is therefore the missing central-extension pushout construction itself. It is strictly stronger than the current semantic packet: it records one same-family phi_lambda, the actual square map q_lambda, its diagonal and polar identification with phi_lambda, naturality, and the simple-head determinant annihilation/radical conclusions.

The current semantic packet is then just the projection forgetting everything except phi.

Residual report for this file:

• New nonlocal residual: minimalBlock_preheadActualCentralExtensionPushoutData.
• Theorem-level projections: MinimalBlockPreheadActualCentralExtensionPushoutData.square_eq_extraspecial, MinimalBlockPreheadActualCentralExtensionPushoutData.toSemanticData, MinimalBlockPreheadActualCentralExtensionPushoutData.toActualScalarData, and MinimalBlockPreheadActualCentralExtensionPushoutData.toActualDeterminantData.
• The closure theorem minimalBlock_preheadCentralPushoutSemanticData_from_finalClosers should have exactly that new residual in its nonstandard axiom closure, not the old minimalBlock_preheadCentralPushoutSemanticData axiom.

Actual central-extension pushout packet

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

Actual scalar central-extension pushout data over a pre-head Section 7 tower.

For every invariant nonzero lambda : R -> F_2, the manuscript forms the central pushout K_lambda = K / ker lambda. The current Lean tower does not carry K_lambda as a quotient group object, so this packet records the exact semantic data used downstream:

• phi is the self-duality/polar pairing induced by the commutator pairing;
• square is the square map q_lambda;
• square_diagonal and polar_symm identify that square and polar with the same phi_lambda;
• phi_natural, square_annihilates_on_T, and square_radical_subset_T are the same-family prop:simpleheaddet conclusions.

This is not a zero-map shortcut: the square map is an explicit field tied to phi by diagonal and polar identities, and the extraspecial comparison below is proved by quadratic-form extensionality from those identities.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

  The self-duality pairing induced by the scalar central pushouts.

• square : Module.Dual (ZMod 2) D.R → Quadratic.QuadF2 D.M

  The actual square map of the same scalar central pushout family.

• square_diagonal (lam : Module.Dual (ZMod 2) D.R) (m : D.M) : (self.square lam).form m = ((self.phi lam) m) m

  The actual square map evaluates on the diagonal of phi_lambda.

• polar_symm (lam : Module.Dual (ZMod 2) D.R) (m m' : D.M) : ((self.square lam).polar m) m' = ((self.phi lam) m) m' + ((self.phi lam) m') m

  The actual polar map is the symmetrized phi_lambda pairing.

• phi_natural (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m m' : D.M), ((self.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((self.phi lam) m) m'

  Naturality/equivariance of the same central-pushout pairing.

• square_annihilates_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → Annihilates (self.square lam) D.T

  q_lambda|_T = 0 and b_lambda(T,M)=0 for the actual square map.

• square_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((self.square lam).polar m) m' = 0) → m ∈ D.T

  The polar radical of the actual square map is contained in T.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData D)

Final Section 7 residual: construct the actual scalar central-extension pushouts and their square/polar/naturality/simple-head determinant data.

This is the exact residual left by this sidecar. It replaces the broad minimalBlock_preheadCentralPushoutSemanticData axiom by the manuscript-shaped actual pushout construction.

theorem Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.square_eq_extraspecial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) (lam : Module.Dual (ZMod 2) D.R) : P.square lam = Quadratic.Extraspecial.extraspecialForm (P.phi lam)

The actual square is the extraspecial square attached to the same phi_lambda. This is theorem-level from the diagonal and polar identities, not an additional residual.

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.toQuadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

Repackage the actual pushout square/polar family as the existing split quadratic-family packet.

Equations

• P.toQuadraticFamily = { phi := P.phi, square := P.square }

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.toSquareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData P.toQuadraticFamily

Repackage the actual pushout diagonal identity as the existing packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.toPolarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) : MinimalBlockPreheadCentralPushoutPolarSymmData P.toQuadraticFamily

Repackage the actual pushout polar identity as the existing packet.

Equations

• ⋯ = ⋯

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

Repackage the actual pushout family as the existing standard same-family square/polar packet.

Equations

• P.toStandardData = { quadraticFamily := P.toQuadraticFamily, squareDiagonal := ⋯, polarSymm := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.toSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) : MinimalBlockPreheadCentralPushoutSemanticData D

Forget the actual square map and retain the current semantic central-pushout packet.

Equations

• P.toSemanticData = { phi := P.phi }

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

Repackage the actual pushout data as the current actual-scalar packet. Surjectivity of nonzero scalar characters is the elementary F_2 theorem from MinimalBlockActualScalarPushoutProofs; no extra residual is used.

Equations

• P.toActualScalarData = { phi := P.phi, square := P.square, scalar_quotient_surjective := ⋯, square_is_extraspecial := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.toActualDeterminantData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionPushoutData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.toSemanticData

Repackage the same data as the current actual simple-head determinant packet for the projected semantic family.

Equations

• ⋯ = ⋯

Closure and projection hooks

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

Closure of the current semantic central-pushout packet from the actual central-extension pushout residual in this file.

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

The standard square/polar packet from the same actual central-extension pushout residual.

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

The current actual-scalar packet from the same actual central-extension pushout residual.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_finalClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadActualCentralExtensionPushoutData D) : Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S.toSemanticData)

The current actual determinant packet from the same actual central-extension pushout residual.

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

Lower pushout route using one actual central-extension pushout residual for both the semantic central family and the simple-head determinant packet.

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

Determinant packets obtained from the final central-pushout closer.

Acceptance checks / exact residual report