Route147 Section 7 actual central-extension closers

This sidecar leaves the integrated Route147 file and root imports untouched.

Route147 currently exposes the Section 7 pushout/determinant boundary as the seven split actual central-extension atoms from MinimalBlockActualCentralExtensionPushoutProofs:

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

The route below reassembles those seven packet targets from a smaller manuscript-shaped boundary:

• the central-pushout quadratic family;
• its square-diagonal identity;
• its polar-symmetry identity;
• the actual simple-head determinant theorem for the selected semantic family.

This is the Lean shape of the manuscript's Section 7 pushout construction: q_lambda is the scalar central-extension square map on the same phi_lambda family, and prop:simpleheaddet supplies naturality, annihilation on T, and polar-radical containment.

Selected actual central-extension packets from semantic determinant data

def Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.MinimalBlockPreheadActualCentralExtensionPhiData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadActualCentralExtensionPhiData D

Select the actual central-extension phi packet from a semantic central-pushout family.

Equations

• Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.MinimalBlockPreheadActualCentralExtensionPhiData.ofSemantic S = { phi := S.phi }

def Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.MinimalBlockPreheadActualCentralExtensionNaturalityData.ofActualSemanticDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (H : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadActualCentralExtensionNaturalityData (MinimalBlockPreheadActualCentralExtensionPhiData.ofSemantic S)

Naturality of the selected actual central-extension family, projected from the actual simple-head determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.MinimalBlockPreheadActualCentralExtensionAnnihilationData.ofActualSemanticDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (H : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadActualCentralExtensionAnnihilationData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi (MinimalBlockPreheadActualCentralExtensionPhiData.ofSemantic S))

Annihilation on T for the selected actual central-extension square map, projected from the actual simple-head determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.MinimalBlockPreheadActualCentralExtensionRadicalContainmentData.ofActualSemanticDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (H : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi (MinimalBlockPreheadActualCentralExtensionPhiData.ofSemantic S))

Polar-radical containment for the selected actual central-extension square map, projected from the actual simple-head determinant packet.

Equations

• ⋯ = ⋯

Four-atom lowering of the seven Route147 actual central-extension atoms

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

The seven Route147 actual central-extension packet targets, reassembled from the smaller actual semantic determinant plus quadratic-family boundary.

The axiom closure of this theorem avoids all seven Route147 actual central-extension packet axioms.

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

Route147 actual central-extension pushout packet reconstructed from the four-atom semantic determinant/quadratic-family boundary.

theorem Q2Presentation.Induction.Section7PushoutRoute147CentralExtensionClosers.minimalBlock_preheadQuadraticFamilyActualDeterminantPackets_from_section7PushoutRoute147CentralExtensionClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData S.toQuadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData S.toQuadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Audit-facing projection to the quadratic-family and actual determinant semantics used to rebuild the actual central-extension packet.

Drop-in determinant-packet provider

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

Lower pushout packet through the Route147 central-extension closer.

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

Drop-in provider for the Route147 Fourier branch.

This has the same consumer shape as Section7PushoutRoute146DeterminantClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute146DeterminantClosers, but its nonstandard axiom closure replaces the seven split actual central-extension packet axioms by the four quadratic-family/actual determinant atoms listed in the module header.

Alternate lowering already present in the project

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

Comparison hook: the older extraspecial/self-duality route also avoids the seven actual central-extension packet axioms, but leaves five older residuals instead of the four semantic determinant/quadratic-family residuals above.