Route88 minimal-block determinant/pushout closer

This sidecar lowers the seven Route88 determinant/pushout frontier leaves that were still exposed by the Route83 provider:

• the three central-pushout square/polar split packets minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, and minimalBlock_preheadCentralPushoutPolarSymmData;
• the four same-family determinant packets minimalBlock_preheadCentralPushoutNaturalitySemanticData, minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData, minimalBlock_preheadCentralPushoutPolarZeroSemanticData, and minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

The replacement packet is manuscript-shaped: one actual scalar central pushout family supplies the scalar quotients and square/extraspecial comparison, and one actual simple-head determinant theorem for the semantic projection of that same family supplies naturality, vanishing on T, and radical containment.

Manuscript anchors: Section 7, especially the scalar pushouts K_lambda = K / ker lambda, their square maps q_lambda, and prop:simpleheaddet.

Route88 actual-pushout / actual-determinant packet

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

Route88 coherent pushout datum.

Compared with Route83, this packet does not prove the scalar central pushout by opening the three split square/polar packets, and it does not prove the coherent determinant packet by opening the four split determinant-semantic packets. Instead it records the two manuscript-level facts that remain:

• the actual scalar central-pushout construction;
• the actual simple-head determinant theorem for the semantic projection of that same scalar pushout family.

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.quadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

The actual scalar-pushout quadratic family selected by Route88.

Equations

• P.quadraticFamily = P.actualScalar.toQuadraticFamily

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.squareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily

The square-diagonal identity for the actual scalar-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.polarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily

The polar-symmetry identity for the actual scalar-pushout family.

Equations

• ⋯ = ⋯

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

The semantic central-pushout family obtained from the same actual scalar pushout.

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semantic

Project semantic naturality from the actual determinant theorem.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.diagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semantic

Project diagonal vanishing on T from the actual determinant theorem.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.polarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semantic

Project polar vanishing on T x M from the actual determinant theorem.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.radicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semantic

Project polar-radical containment from the actual determinant theorem.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.coherentDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData P.semantic

The coherent determinant packet recovered theorem-level from the actual simple-head determinant theorem.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.toRoute83 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data D

Route88 projected to the Route83 packet shape consumed by the existing Route83 theorem-level projections.

Equations

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data.toRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute88Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D

Route88 projected to the Route82 coherent packet.

Equations

• P.toRoute82 = P.toRoute83.toRoute82

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

Route88 projected directly to the lower pushout packet consumed downstream.

Equations

• P.toPushoutRouteLower = P.toRoute83.toPushoutRouteLower

Constructors and drop-in provider

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.minimalBlock_preheadPushoutRoute88Data_from_actualPushoutAndActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadPushoutRoute88Data D)

Assemble the Route88 packet from the two manuscript-shaped residual packets.

Axiom-closure effect: the seven Route88 leaves named in the module header are replaced by the two smaller same-family packets minimalBlock_preheadActualScalarCentralPushoutData and minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.minimalBlock_preheadPushoutRoute83Data_from_route88 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data D)

Route88 projected to the Route83 coherent actual-scalar packet.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute88Closers.minimalBlock_preheadPushoutRoute82Data_from_route88 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D)

Route88 projected to the Route82 coherent packet.

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

Route88 lower pushout packet.

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

Drop-in determinant-packet replacement for the next integrated route.

This theorem has the same conclusion as MinimalBlockPushoutRoute83Closers.minimalBlock_preheadDeterminantPackets_from_route83, but routes through Route88's actual-pushout / actual-determinant packet.