Actual central-extension pushout packet split

This sidecar further decomposes the current Section 7 final-route residual

• minimalBlock_preheadActualCentralExtensionPushoutData.

Manuscript anchor: reference/q2_manuscript.tex, Section 7, eq:targettower, lem:simplehead, lem:collapse, and prop:simpleheaddet. For every invariant nonzero scalar character lambda : R -> F_2, the paper forms the quotient central extension K_lambda = K / ker lambda, with self-duality pairing, square map, diagonal and polar identities, naturality, annihilation on T, and radical containment.

MinimalBlockCentralPushoutFinalClosers packages all of that as one residual. The split below keeps the same semantic target but separates it into narrower, same-family packets:

• PhiData: the scalar pushout pairing phi_lambda;
• SquareData: the actual square map q_lambda;
• DiagonalData: q_lambda(m) = phi_lambda(m,m);
• PolarData: the polar form is the symmetrized pairing;
• NaturalityData: equivariance of phi_lambda;
• AnnihilationData: q_lambda|_T = 0 and b_lambda(T,M)=0;
• RadicalContainmentData: the polar radical is contained in T.

The theorem minimalBlock_preheadActualCentralExtensionPushoutData_from_splitPackets reassembles the old broad residual from these smaller packets without using the old broad residual axiom.

Split packets for the actual scalar central extension

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

The self-duality/polar pairing family induced by the actual scalar central extensions K_lambda = K / ker lambda.

This is only the phi_lambda part of the current broad residual. It deliberately does not include the square map or determinant conclusions.

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

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

The square-map family q_lambda of the same actual scalar central extensions. It is indexed by the phi packet so all later identities are forced to talk about the same scalar pushout family.

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

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Prop

Diagonal identity for the actual square map.

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

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPolarData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Prop

Polar identity for the actual square map.

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

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionNaturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Prop

Naturality/equivariance of the actual scalar central-extension 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), ((Phi.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((Phi.phi lam) m) m'

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Prop

The prop:simpleheaddet annihilation conclusion for the actual square map: q_lambda|_T = 0 and b_lambda(T,M)=0.

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

structure Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Prop

The prop:simpleheaddet radical-containment conclusion 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), ((Q.square lam).polar m) m' = 0) → m ∈ D.T

Narrow residual hooks

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

Construct the actual phi_lambda family of the central pushouts.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionSquareData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionSquareData Phi)

Construct the actual square maps q_lambda for the same central pushouts.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData Q)

Prove the diagonal identity for the split actual square map.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPolarData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData Q)

Prove the polar identity for the split actual square map.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionNaturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData Phi)

Prove naturality for the split actual pairing family.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData Q)

Prove annihilation on T for the split actual square map.

axiom Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q)

Prove polar-radical containment for the split actual square map.

Reassembly of the old broad packet from split packets

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.ofSplitPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi) (Diag : MinimalBlockPreheadActualCentralExtensionDiagonalData Q) (Polar : MinimalBlockPreheadActualCentralExtensionPolarData Q) (Nat : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) (Ann : MinimalBlockPreheadActualCentralExtensionAnnihilationData Q) (Rad : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Reassemble the broad actual central-extension pushout packet from the split same-family packets.

Equations

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

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

Route-ready replacement for the current broad actual central-extension pushout residual. Its axiom closure contains the split packets above and not minimalBlock_preheadActualCentralExtensionPushoutData.

Route-ready projection hooks from the split packets

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

Semantic central-pushout data from the split actual central-extension packets.

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

Standard square/polar data from the split actual central-extension packets.

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

Actual scalar central-pushout data from the split actual central-extension packets.

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

Lower pushout route using the split actual central-extension packets.

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

Determinant packet projection through the split actual central-extension route.

Acceptance checks / exact residual report