Actual Section 7 determinant-pushout proof boundary

This sidecar narrows the current coherent residual minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual.

The current residual is indexed by an arbitrary projected self-duality family. The packet below is smaller and more manuscript-shaped: it is indexed by the actual semantic central-pushout family used in Section 7, so the annihilation and radical statements are made for the same square map S.toQuadraticFamily.square whose diagonal and polar are definitionally the extraspecial determinant pushout. This is the Lean counterpart of prop:simpleheaddet for K_lambda = K / ker lambda.

Actual central-pushout determinant packet

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

The smallest remaining semantic determinant packet for the Section 7 extraspecial residual.

For the actual semantic central-pushout family S, this states exactly the prop:simpleheaddet conclusions needed by the existing lower route:

• naturality of the determinant pairing;
• annihilation of T by the scalar square map and its polar form;
• containment of the polar radical in T.

The square map is S.toQuadraticFamily.square, not a separately chosen extraspecial packet, so all downstream projections use one actual pushout family.

• 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), ((S.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((S.phi lam) m) m'
• square_annihilates_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → Annihilates (S.toQuadraticFamily.square lam) D.T
• 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), ((S.toQuadraticFamily.square lam).polar m) m' = 0) → m ∈ D.T

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Residual narrowed to the actual semantic central-pushout square family.

Manuscript anchor: prop:simpleheaddet, pages 41-42. This is intentionally semantic: it does not assert an arbitrary extraspecial determinant packet, only the determinant theorem for the central-pushout family S.

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData.toExtraspecialSimpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData S.toExtraspecialFamily

Project the actual semantic determinant packet to the current extraspecial simple-head determinant structure.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual_from_actualSemanticPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S.toSelfDuality))

The current extraspecial simple-head determinant residual, proved for the self-duality family coming from an actual semantic central pushout.

This is the route-ready replacement for minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual: it has the same conclusion, but only for S.toSelfDuality, the self-duality projection of the actual central-pushout family.

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

The lower pushout route closed from the actual semantic determinant packet.

Its axiom closure replaces minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual by the narrower minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData, while retaining the existing semantic central-pushout family residual.

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

Determinant packet projection from the narrowed actual semantic determinant route.