Actual central-extension closers from extraspecial determinant packets

This sidecar targets the seven final-route Section 7 packets introduced in MinimalBlockActualCentralExtensionPushoutProofs:

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionSquareData;
• minimalBlock_preheadActualCentralExtensionDiagonalData;
• minimalBlock_preheadActualCentralExtensionPolarData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

It does not call those seven axioms. Instead it rebuilds their targets from the older same-family extraspecial determinant interface:

• a central-pushout self-duality family phi;
• extraspecial naturality for that family;
• diagonal-zero, polar-zero, and radical-containment packets on the equivariant extraspecial family induced by naturality.

The square map is the proven extraspecial square Extraspecial.extraspecialForm (phi lam), so the diagonal and polar packets are definitional and annihilation/radical containment follow from the proven extraspecial_annihilates and extraspecial_radical_subset helpers.

Theorem-level constructors for the seven actual central-extension packets

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPhiData.ofSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadActualCentralExtensionPhiData D

The actual central-extension phi packet is the existing central-pushout self-duality family.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPhiData.ofSelfDuality S = { phi := S.phi }

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

Use the extraspecial square attached to the same phi_lambda family.

Equations

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

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionDiagonalData.ofPhi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : MinimalBlockPreheadActualCentralExtensionDiagonalData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi)

The extraspecial square is definitionally the diagonal of phi_lambda.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPolarData.ofPhi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : MinimalBlockPreheadActualCentralExtensionPolarData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi)

The extraspecial polar form is definitionally the symmetrized pairing.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionNaturalityData.ofExtraspecialNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadExtraspecialNaturalityData { phi := Phi.phi }) : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi

Convert extraspecial naturality for the same phi family to the actual central-extension naturality packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionNaturalityData.toExtraspecialEquivariantFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

The equivariant extraspecial family induced by actual central-extension naturality. This is the family on which the diagonal-zero, polar-zero, and radical-containment packets are requested below.

Equations

• N.toExtraspecialEquivariantFamily = { phi := Phi.phi, diagonal_invariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionAnnihilationData.ofExtraspecialZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) (Z : MinimalBlockPreheadExtraspecialDiagonalZeroData N.toExtraspecialEquivariantFamily) (P : MinimalBlockPreheadExtraspecialPolarZeroData N.toExtraspecialEquivariantFamily) : MinimalBlockPreheadActualCentralExtensionAnnihilationData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi)

Build actual square annihilation from diagonal and polar zero for the same extraspecial family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRadicalContainmentData.ofExtraspecialRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) (R : MinimalBlockPreheadExtraspecialRadicalContainmentData N.toExtraspecialEquivariantFamily) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi)

Build actual polar-radical containment from radical containment for the same symmetrized extraspecial pairing.

Equations

• ⋯ = ⋯

Individual replacement theorems

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

Replacement for the PhiData packet from the existing self-duality packet.

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

Replacement for the SquareData packet once PhiData is fixed.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionDiagonalData_from_phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Replacement for the DiagonalData packet once PhiData is fixed and the square is the extraspecial square attached to it.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPolarData_from_phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Replacement for the PolarData packet once PhiData is fixed and the square is the extraspecial square attached to it.

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

Replacement for the NaturalityData packet from extraspecial naturality for the same phi family.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionAnnihilationData_from_extraspecial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Replacement for the AnnihilationData packet from extraspecial diagonal and polar zero for the family induced by actual naturality.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionRadicalContainmentData_from_extraspecial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadActualCentralExtensionPhiData D} (N : MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) : Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Replacement for the RadicalContainmentData packet from extraspecial radical containment for the family induced by actual naturality.

Aggregate route-ready replacements

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_extraspecial {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)

All seven actual central-extension packet targets, tied to one phi and one extraspecial square family, from the existing extraspecial determinant packets.

The axiom closure of this theorem avoids all seven Parfit packet axioms.

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

Route-ready replacement for the broad actual central-extension pushout packet using the existing extraspecial/simple-head determinant packet API rather than the seven Parfit packet axioms.

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

Lower pushout route obtained through the new actual central-extension closer. This is the coordinator-facing hook for replacing the seven final-route packets by the extraspecial/simple-head determinant packet family used in this file.

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

Determinant packet projection through MinimalBlockActualCentralExtensionClosers2.

Acceptance checks / exact residual report