Coherent Section 7 extraspecial central-extension closer

This sidecar targets the current final-route Section 7 central-extension / extraspecial determinant packets:

• minimalBlock_preheadCentralPushoutSelfDualityData;
• minimalBlock_preheadExtraspecialNaturalityData;
• minimalBlock_preheadExtraspecialDiagonalZeroData;
• minimalBlock_preheadExtraspecialPolarZeroData;
• minimalBlock_preheadExtraspecialRadicalContainmentData.

The API cannot yet construct the actual quotient groups K_lambda = K / ker lambda. The remaining floor below is therefore the manuscript-shaped actual construction packet: one central-pushout self-duality family phi_lambda, naturality for that same family, annihilation of the actual extraspecial square on T, and containment of the actual polar radical in T.

This is not a zero-data shortcut. The square map is always the proven extraspecial form Extraspecial.extraspecialForm (phi lambda), whose diagonal and polar are the class-two determinant square/commutator formulas from Quadratic/GaussSign.lean and MinimalBlock.lean.

One coherent remaining floor

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

Coherent actual Section 7 central-pushout/extraspecial determinant data.

For every nonzero invariant lambda : R -> F_2, this records the actual central-pushout pairing phi_lambda, its conjugation naturality, the prop:simpleheaddet annihilation statement for the extraspecial square map, and the radical-containment statement which makes the descended head form nonsingular.

This packet is deliberately indexed only by the pre-head tower D: all projection theorems below derive their families from this same phi, so the current residuals cannot drift onto unrelated arbitrary families.

• 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.

• 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 actual 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 (Quadratic.Extraspecial.extraspecialForm (self.phi lam)) D.T

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

• 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), ((Quadratic.Extraspecial.extraspecialForm (self.phi lam)).polar m) m' = 0) → m ∈ D.T

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

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

Remaining Section 7 floor after this sidecar, now discharged from the actual semantic split: construct the actual scalar central-pushout square/polar family and prove prop:simpleheaddet for the same projected family.

Projections to the current extraspecial packets

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadCentralPushoutSelfDualityData D

Forget to the current central-pushout self-duality packet.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialFamilyData D

The bare extraspecial family induced by the same actual phi_lambda.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialNaturalityData P.toFamily

Naturality for the induced bare extraspecial family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toEquivariantFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

The equivariant extraspecial family induced by naturality of the actual central-pushout pairing.

Equations

• P.toEquivariantFamily = { phi := P.phi, diagonal_invariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toDiagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialDiagonalZeroData P.toEquivariantFamily

Diagonal vanishing on T, projected from annihilation of the actual extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toPolarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialPolarZeroData P.toEquivariantFamily

Polar vanishing on T x M, projected from annihilation of the actual extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toRadicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialRadicalContainmentData P.toEquivariantFamily

Radical containment for the symmetrized phi_lambda polar form, projected from radical containment of the actual extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toSimpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData P.toFamily

The same data as the lower same-family simple-head determinant packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.descended_nonsingular {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) (lam : Module.Dual (ZMod 2) D.R) (hlam : lam ≠ 0) (hinv : ∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) : ⋯.descend.Nonsingular

The descended simple-head form is nonsingular. This is the formal prop:simpleheaddet nonsingularity step, derived from Annihilates.descend and the radical-containment field.

Projections to the actual-central-extension split packets

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualPhi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionPhiData D

The split actual central-extension PhiData packet.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualSquare {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionSquareData P.toActualPhi

The split actual square map, fixed to the extraspecial determinant square.

Equations

• P.toActualSquare = { square := fun (lam : Module.Dual (ZMod 2) D.R) => Q2Presentation.Quadratic.Extraspecial.extraspecialForm (P.phi lam) }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.toActualSquare

The actual square is the diagonal of the same phi_lambda.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualPolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionPolarData P.toActualSquare

The actual polar is the symmetrized same-family pairing.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.toActualPhi

Actual central-extension naturality for the same phi_lambda.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualAnnihilation {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.toActualSquare

Actual central-extension annihilation from the actual extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutExtraspecialActualData.toActualRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutExtraspecialActualData D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.toActualSquare

Actual central-extension radical containment from the actual extraspecial square.

Equations

• ⋯ = ⋯

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

Reassemble the broad actual central-extension pushout packet from the coherent extraspecial construction packet.

Equations

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

Route-ready theorem replacements

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

Replacement for the self-duality packet on the actual central-pushout family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPackets_from_extraspecialClosers3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (F : MinimalBlockPreheadExtraspecialFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialNaturalityData F) ∧ ∃ (E : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData E) ∧ Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData E) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData E)

The four extraspecial determinant packets for the coherent actual central-pushout family produced by this sidecar.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_extraspecialClosers3 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi), Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q)

Split actual central-extension packets, all tied to the same actual extraspecial central-pushout construction.

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

Route-ready replacement for the broad actual central-extension pushout packet. Its axiom closure contains the one coherent Closers3 packet rather than the five current self-duality/naturality/zero/radical packet axioms.

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

Lower pushout route through the coherent actual extraspecial construction.

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

Determinant packet projection through MinimalBlockExtraspecialClosers3.

Acceptance checks / exact residual report