Route22 minimal-block pushout/determinant close-out

Route21 split the former broad Section 7 actual central-extension pushout residual into seven same-family packets:

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

This sidecar gives a route22 hook that constructs the route21 split packet from the existing coherent extraspecial actual-pushout API in MinimalBlockExtraspecialClosers3. All route21 fields are projected from one actual scalar central-pushout/extraspecial family, so the resulting Phi and Q data cannot drift onto independent arbitrary witnesses.

Route22 coherent actual-pushout packet

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

Route22 actual central-extension data.

The single field is the coherent actual extraspecial central-pushout packet from MinimalBlockExtraspecialClosers3. It already contains the same phi_lambda family, its extraspecial square, naturality, annihilation on T, and polar-radical containment.

• actual : MinimalBlockPreheadCentralPushoutExtraspecialActualData D

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

The route21 PhiData packet projected from the route22 family.

Equations

• P.phiData = P.actual.toActualPhi

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.squareData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionSquareData P.phiData

The route21 SquareData packet projected from the same route22 family.

Equations

• P.squareData = P.actual.toActualSquare

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.diagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.squareData

The route21 diagonal identity for the same projected square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.polarData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionPolarData P.squareData

The route21 polar identity for the same projected square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.naturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiData

Naturality for the same projected phi_lambda family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.annihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squareData

Annihilation on T for the same projected square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.radicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squareData

Polar-radical containment for the same projected square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.toRoute21Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPushoutRoute21ActualCentralExtensionData D

Repackage route22 as the route21 split actual central-extension packet.

Equations

• P.toRoute21Data = { phiData := P.phiData, squareData := P.squareData, diagonalData := ⋯, polarData := ⋯, naturalityData := ⋯, annihilationData := ⋯, radicalContainmentData := ⋯ }

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

Broad actual central-extension pushout data recovered through route21's split reassembler.

Equations

• P.toActualPushout = P.toRoute21Data.toActualPushout

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.toRoute20ActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPushoutRoute20ActualDeterminantData D

Route20-shaped determinant wrapper projected from route22 through route21.

Equations

• P.toRoute20ActualDeterminant = P.toRoute21Data.toRoute20ActualDeterminant

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.standard {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadCentralPushoutStandardData D

Standard square/polar data projected from route22.

Equations

• P.standard = P.toRoute21Data.standard

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.actualScalar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadActualScalarCentralPushoutData D

Actual scalar central-pushout data projected from route22.

Equations

• P.actualScalar = P.toRoute21Data.actualScalar

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.actualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.toRoute20ActualDeterminant.semantic

The actual determinant packet for the route22 family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute22ActualCentralExtensionData.toPushoutRouteLower {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute22ActualCentralExtensionData D) : MinimalBlockPreheadPushoutRouteLowerData D

Lower pushout route packet projected from route22.

Equations

• P.toPushoutRouteLower = P.toRoute21Data.toPushoutRouteLower

Route22 construction and route-compatible hooks

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

Construct route22 data from the coherent actual extraspecial pushout API.

The nonstandard closure of this theorem avoids the seven route21 split packet axioms. Its remaining floor is the coherent actual semantic packet used by MinimalBlockExtraspecialClosers3.

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

Route21 split actual central-extension data constructed from route22's one coherent actual extraspecial family.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_route22 {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 route21 split packet targets, tied to one route22 Phi/Q family.

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

Broad actual central-extension packet recovered from route22 data.

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

Route21 lower pushout hook with the seven route21 split residuals replaced by route22's coherent actual extraspecial family.

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

Alias matching the route21 determinant naming convention for later integration swaps.

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

Determinant packet projection through route22.

Acceptance checks / exact residual report