Route44 minimal-block pushout/determinant provider

Route43 exposes the Section 7 actual central-extension pushout as seven split same-family leaves:

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

The manuscript Section 7 determinant-pushout argument is more coherent than that frontier: it fixes one actual scalar central-pushout/extraspecial family phi_lambda, uses the extraspecial square attached to that family, and proves prop:simpleheaddet for the same family.

This sidecar keeps the Route43 downstream shape but obtains all seven split targets from MinimalBlockExtraspecialClosers3's coherent actual extraspecial packet. Thus Route44 removes the seven Route43 split residual names from the provider closure. Its remaining pushout frontier is the lower two-piece extraspecial floor:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

No integrated/root route file imports this sidecar yet.

Route44 packet

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

Route44 data: one coherent Section 7 actual extraspecial central-pushout packet, projected below to the Route43 actual central-extension interface.

• extraspecial : MinimalBlockPreheadCentralPushoutExtraspecialActualData D

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

The broad actual central-extension pushout packet selected by Route44.

Equations

• P.actual = P.extraspecial.toActualCentralExtensionPushoutData

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

The split actual central-extension phi_lambda packet selected by Route44.

Equations

• P.actualPhi = P.extraspecial.toActualPhi

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualSquare {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionSquareData P.actualPhi

The split actual square packet selected by Route44.

Equations

• P.actualSquare = P.extraspecial.toActualSquare

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.actualSquare

The split actual diagonal packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualPolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionPolarData P.actualSquare

The split actual polar packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.actualPhi

The split actual naturality packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualAnnihilation {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.actualSquare

The split actual annihilation packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.actualRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.actualSquare

The split actual radical-containment packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.toRoute43Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPushoutRoute43Data D

Route44 projected to the Route43 provider structure.

Equations

• P.toRoute43Data = { actual := P.actual }

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

The actual scalar central-pushout packet selected by Route44.

Equations

• P.actualScalar = P.toRoute43Data.actualScalar

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPreheadCentralPushoutSemanticData D

The semantic central-pushout family selected by Route44.

Equations

• P.semantic = P.toRoute43Data.semantic

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

The same-family actual determinant packet selected by Route44.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute44Data.toRoute42Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute44Data D) : MinimalBlockPushoutRoute42Data D

Route44 projected to the Route42 packet shape.

Equations

• P.toRoute42Data = P.toRoute43Data.toRoute42Data

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

Route44 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLower = P.toRoute43Data.toPushoutRouteLower

Route-compatible hooks

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

Construct Route44 data from the coherent extraspecial actual packet.

Residual report: this theorem does not use the seven Route43 actual central-extension split axioms. Its pushout closure is the two-piece MinimalBlockExtraspecialClosers3 floor documented in the module comment.

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

Route44 replacement for the broad actual central-extension pushout packet.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_route44 {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 Route43 split actual-central-extension packet targets, tied to one Route44 actual extraspecial construction.

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

Route44 supplies the Route43 packet shape without using the seven Route43 split actual-central-extension residuals.

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

Route44 replacement for the Route42 actual scalar packet.

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

Route44 supplies the Route42 same-family packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_route44 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Audit hook: the selected Route44 semantic family carries an actual simple-head determinant packet.

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

Drop-in Route44 lower pushout provider.

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

Determinant packet projection through the Route44 lower pushout provider.

Acceptance checks / exact residual report