Route43 minimal-block pushout/determinant provider

Route42 leaves the Section 7 pushout branch at two bundled actual packet boundaries:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

The manuscript's construction is more specific: for every nonzero invariant scalar character lambda : R -> F_2, it forms the actual central extension pushout K_lambda = K / ker lambda, records the square map and its diagonal and polar identities, and proves prop:simpleheaddet for that same square map.

The older split actual-central-extension API already exposes exactly those same-family pieces. Route43 reassembles them to the broad actual central-extension packet and then projects to the Route42 interface. Thus the Route42 actual scalar and actual determinant leaves disappear from the Route43 provider closure and are replaced by the stricter manuscript-shaped split:

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

No new axiom is introduced here.

Route43 packet

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

Route43 data: the actual scalar central-extension pushout family retained as one coherent manuscript object, but constructed below from its seven split same-family packets.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The actual scalar central-pushout packet selected by Route43.

Equations

• P.actualScalar = P.actual.toActualScalarData

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

The semantic central-pushout family selected by Route43.

Equations

• P.semantic = P.actual.toSemanticData

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

The actual simple-head determinant packet for the same Route43 semantic central-pushout family.

Equations

• ⋯ = ⋯

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

Route43 projected to the Route39 packet shape.

Equations

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

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

Route43 projected to the Route42 packet shape.

Equations

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

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

Route43 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLower = P.toRoute42Data.toPushoutRouteLower

Route-compatible hooks

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

Construct Route43 data from the seven split actual central-extension packets.

This theorem is the refinement point: its closure contains the seven split actual-central-extension residuals and not the two Route42 actual packet residuals.

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

Route43 replacement for the Route42 actual scalar packet.

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

Route43 supplies the Route42 same-family packet without using the two Route42 actual packet residuals.

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

Audit hook: the selected Route43 semantic central-pushout family carries an actual simple-head determinant packet, again without using the Route42 bundled determinant residual.

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

Drop-in Route43 lower pushout provider.

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

Determinant packet projection through the Route43 lower pushout provider.

Acceptance checks / exact residual report