Route39 minimal-block pushout/determinant provider

Route38 leaves two Section 7 pushout residuals:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

The manuscript's Section 7 construction is more specific than either bundled packet: for each nonzero invariant scalar character it forms the actual central pushout K_lambda = K / ker lambda, records the square map and its diagonal and polar identities, and then proves prop:simpleheaddet for the same square map.

This Route39 sidecar keeps the Route38-facing conclusion but obtains both Route38 packets from the existing split actual-central-extension packets in MinimalBlockActualCentralExtensionPushoutProofs. Thus the exported provider does not depend on the two Route38 residual names. Its remaining nonlocal frontier is the strictly smaller same-family split:

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

No integration or root file imports this sidecar yet.

Route39 packet

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

Route39 data: the split actual central-extension pushout reassembled as one coherent manuscript object, then projected to the Route38 interface.

• actual : MinimalBlockPreheadActualCentralExtensionPushoutData D

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

The actual scalar central-pushout packet selected by Route39.

Equations

• P.actualScalar = P.actual.toActualScalarData

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

The semantic central-pushout family selected by Route39.

Equations

• P.semantic = P.actual.toSemanticData

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

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

Equations

• ⋯ = ⋯

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

Route39 projected to the Route38 same-family packet.

Equations

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

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

Route39 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLower = P.toRoute38Data.toPushoutRouteLower

Route-compatible hooks

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

Construct the Route39 packet from the split actual central-extension pushout packets.

The axiom closure of this theorem contains the seven split packets listed in the module comment, not the two Route38 bundled residuals.

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

Route39 replacement for the Route38 actual scalar residual.

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

Route38-compatible same-family packet, supplied by Route39.

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

The Route38 lower pushout provider supplied through the Route39 split actual central-extension packets.

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

Determinant packet projection through the Route39 lower pushout provider.

Acceptance checks / exact residual report