Route164 Section 7 pushout/determinant actual-atom lowering

Route163's pushout frontier is the two coherent Route161 leaves:

• minimalBlock_preheadCentralPushoutSelfDualityData;
• minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual.

This sidecar lowers them together to actual scalar-pushout atoms. The self-duality family is projected from MinimalBlockPreheadActualScalarCentralPushoutData, and the simple-head determinant packet is projected from MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData for the same actual scalar-pushout family. The exported determinant-packet theorem has the same consumer shape as the Route161 provider.

Manuscript anchors: Section 7, prop:simpleheaddet, and the scalar pushouts K_lambda = K / ker lambda.

Actual scalar-pushout Route164 packet

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

Route164 coherent actual-atom packet.

The determinant field is indexed by the semantic projection of the same actual scalar central-pushout family, so the projected self-duality and determinant families share the same phi_lambda.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• actualSimpleHeadDeterminant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData self.actualScalar.toSemanticData

def Q2Presentation.Induction.Section7PushoutRoute164Closers.MinimalBlockPushoutRoute164ActualDeterminantData.selfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute164ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutSelfDualityData D

The self-duality packet projected from the actual scalar pushout.

Equations

• P.selfDuality = P.actualScalar.toSelfDualityData

def Q2Presentation.Induction.Section7PushoutRoute164Closers.MinimalBlockPushoutRoute164ActualDeterminantData.simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute164ActualDeterminantData D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality P.selfDuality)

The Route161-style simple-head determinant packet projected from the actual determinant theorem for the same scalar-pushout family.

Equations

• ⋯ = ⋯

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

Route-lower packet reassembled from the Route164 actual-atom packet.

Equations

• P.toPushoutRouteLower = { selfDuality := P.selfDuality, simpleHeadDeterminant := ⋯ }

theorem Q2Presentation.Induction.Section7PushoutRoute164Closers.minimalBlock_pushoutRoute164ActualDeterminantData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute164ActualDeterminantData D)

Construct the Route164 actual-atom packet.

Its axiom frontier is the actual scalar central-pushout atom plus the actual simple-head determinant atom for that same scalar-pushout family.

Route-level bridges

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

Supervisor hook: lower the Route163 pushout packet to Route164 actual atoms.

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

Drop-in replacement for Section7PushoutRoute161Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute161Closers.

The statement has the same downstream consumer shape, but its axiom frontier replaces Route163's self-duality and residual determinant leaves by the two Route164 actual scalar-pushout atoms.

Acceptance checks / exact residual report