Route31 minimal-block pushout/determinant provider

Route30 supplies the lower Section 7 pushout route through the extraspecial self-duality interface. Its provider closure is the five route32 residuals

• minimalBlock_preheadCentralPushoutSelfDualityData;
• minimalBlock_preheadExtraspecialNaturalityData;
• minimalBlock_preheadExtraspecialDiagonalZeroData;
• minimalBlock_preheadExtraspecialPolarZeroData;
• minimalBlock_preheadExtraspecialRadicalContainmentData.

This sidecar keeps the route30 downstream shape, but rebuilds the actual central-extension packet from a same-family semantic determinant route:

• the concrete central-pushout quadratic family;
• its square-diagonal and polar-symmetry identities;
• one actual simple-head determinant packet on the semantic square induced by that same family.

Thus the route-compatible hook below should make the five route30 residual names disappear from the provider closure, replacing them by the four more concrete same-family packets.

Route31 actual semantic determinant packet

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

Route31 data: one concrete central-pushout square/polar family, plus the actual simple-head determinant theorem for the semantic extraspecial square attached to that same family.

• standard : MinimalBlockPreheadCentralPushoutStandardData D
• actualDeterminant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData self.standard.semanticData

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

The semantic central-pushout family selected by route31.

Equations

• P.semantic = P.standard.semanticData

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

The self-duality projection of the route31 semantic family.

Equations

• P.selfDuality = P.semantic.toSelfDuality

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

The extraspecial determinant packet for the self-duality projection selected by route31.

Equations

• ⋯ = ⋯

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

Rebuild the broad actual central-extension packet from route31's same-family standard square/polar data and actual semantic determinant packet.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.MinimalBlockPushoutRoute31ActualSemanticDeterminantData.toRoute30Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute31ActualSemanticDeterminantData D) : MinimalBlockPushoutRoute30ActualCentralExtensionClosedData D

Route30-compatible data, but supplied through route31's actual semantic determinant path.

Equations

• P.toRoute30Data = { actual := P.actualCentralExtension }

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

Lower pushout route inherited from the rebuilt actual central-extension packet.

Equations

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

Route-compatible hooks

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

Construct route31 data from the concrete square/polar packet and actual semantic simple-head determinant packet.

Residual report: this theorem avoids all five route30 pushout residual names. Its remaining nonstandard pushout closure is:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

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

Route30-compatible actual central-extension data from the route31 provider.

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

Broad actual central-extension packet from the route31 provider.

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

Semantic central-pushout data from the route31 provider.

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

Same-family actual determinant packet selected by the route31 provider.

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

Supervisor hook: lower pushout route from the route31 provider.

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

Determinant packet projection through the route31 lower pushout provider.

Acceptance checks / exact residual report