Route146 Section 7 pushout/determinant lowering

This sidecar leaves the Route145 integrated file untouched. It exports the same determinant-packet consumer shape as Section7PushoutRoute145ActualClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute145ActualClosers, but routes the proof through the split actual central-extension packet from MinimalBlockActualCentralExtensionPushoutProofs.

Route145's pushout/determinant frontier consists of one square/polar atom and four semantic determinant atoms. Route146 replaces those five atoms by the actual scalar central-extension split:

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

The projections below show explicitly that the Route145 square/polar and semantic determinant surfaces are theorem-level consequences of that split.

Actual central-extension source

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

Route146 actual central-extension packet, assembled from the split atoms.

Projections to the Route145 atom surfaces

theorem Q2Presentation.Induction.Section7PushoutRoute146DeterminantClosers.minimalBlock_preheadCentralPushoutSquarePolarData_from_section7PushoutRoute146DeterminantClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutSquarePolarData D)

The Route145 square/polar atom is a projection of the Route146 split actual central-extension packet.

theorem Q2Presentation.Induction.Section7PushoutRoute146DeterminantClosers.minimalBlock_preheadCentralPushoutSemanticDeterminantPackets_from_section7PushoutRoute146DeterminantClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The four Route145 semantic determinant atoms for the selected central pushout family are projections of the same Route146 split actual central-extension packet.

theorem Q2Presentation.Induction.Section7PushoutRoute146DeterminantClosers.minimalBlock_preheadRoute145PushoutAtoms_from_section7PushoutRoute146DeterminantClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSquarePolarData D) ∧ Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

Audit-facing packet: all five Route145 pushout/determinant surfaces are available from the Route146 split actual central-extension packet, without using the five Route145 atoms as axioms.

Drop-in determinant-packet replacement

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

Route146 lower pushout packet through the split actual central-extension route.

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

Drop-in replacement for Section7PushoutRoute145ActualClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute145ActualClosers.