Route46 minimal-block pushout/determinant provider

Route44 leaves the Section 7 pushout branch at two broad packets:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

Route45 avoids those names by expanding them into seven split square/polar and semantic simple-head determinant packets. Route46 keeps the final-route surface small instead: it uses the manuscript-shaped actual central-extension pushout packet from MinimalBlockCentralPushoutFinalClosers, recording the construction of the scalar central pushouts K_lambda = K / ker lambda, their square/polar identities, naturality, and the same-family prop:simpleheaddet conclusions.

The exported hook minimalBlock_preheadPushoutRouteLowerData_from_route46 is a drop-in replacement for minimalBlock_preheadPushoutRouteLowerData_from_route44. Its nonstandard closure is the single actual-pushout residual minimalBlock_preheadActualCentralExtensionPushoutData, rather than Route44's two broad residuals or Route45's seven expanded semantic residuals.

Route46 packet

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

Route46 data: the actual Section 7 central-extension pushout packet.

This one packet is the manuscript step that simultaneously supplies the scalar central-pushout square/polar family and the same-family simple-head determinant facts.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The actual scalar central-pushout family selected by Route46.

Equations

• P.actualScalar = P.actual.toActualScalarData

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

The semantic central-pushout family selected by Route46.

Equations

• P.semantic = P.actual.toSemanticData

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

The same-family actual determinant packet selected by Route46.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute46Data.toRoute45Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute46Data D) : MinimalBlockPushoutRoute45Data D

Route46 projected to the Route45 packet shape, without using Route45's expanded semantic residuals.

Equations

• P.toRoute45Data = { actualScalar := P.actualScalar, determinant := ⋯ }

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

Route46 projected to the Route44 packet shape.

Equations

• P.toRoute44Data = { extraspecial := P.toRoute45Data.toExtraspecialActual }

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

Route46 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLower = P.toRoute45Data.toPushoutRouteLower

Route-compatible hooks

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

Construct Route46 data from the one actual central-extension pushout packet.

Residual report: this theorem does not use Route44's two broad pushout leaves and does not expose Route45's seven split semantic leaves.

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

Route46 replacement for the old square/polar leaf, using the selected actual pushout packet.

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

Route46 replacement for the route-relevant actual determinant packet.

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

Route46 supplies the Route45 packet shape without Route45's seven split semantic residuals.

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

Route46 supplies the Route44 packet shape with a sharper one-packet closure than minimalBlock_pushoutRoute44Data_from_extraspecialActual.

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

Route46 replacement for the Route44 actual scalar packet.

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

Drop-in Route46 lower pushout provider.

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

Determinant packet projection through the Route46 lower pushout provider.

Acceptance checks / exact residual report