Route38 minimal-block pushout/determinant provider

Route37 exposes seven Section 7 pushout residuals:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

The manuscript's determinant pushout is not seven independent choices. It is one actual scalar central-pushout family K_lambda = K / ker lambda, together with the simple-head determinant theorem for the same family.

This Route38 sidecar records exactly that boundary:

• actual scalar central-pushout data on the pre-head tower;
• prop:simpleheaddet for the semantic family obtained from that actual scalar pushout.

The old seven packets are projections from these two same-family packets. This does not claim the quotient groups K_lambda have been constructed in Lean; it strictly lowers the Route37 residuals to the manuscript-shaped actual scalar pushout and actual simple-head determinant packets already present in the API.

Route38 pushout packet

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

Route38 same-family pushout/determinant data.

The determinant packet is indexed by the semantic central-pushout family projected from actualScalar, so all square/polar and determinant projections below use the same scalar pushout family.

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

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

The semantic central-pushout family selected by Route38.

Equations

• P.semantic = P.actualScalar.toSemanticData

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

The actual simple-head determinant packet, reindexed by P.semantic.

Equations

• ⋯ = ⋯

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

The split quadratic family projected from the actual scalar pushout.

Equations

• P.quadraticFamily = P.actualScalar.toQuadraticFamily

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

The square-diagonal packet for the same Route38 family.

Equations

• ⋯ = ⋯

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

The polar-symmetry packet for the same Route38 family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute38Data.naturalitySemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute38Data D) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semantic

Semantic naturality projected from the actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute38Data.diagonalZeroSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute38Data D) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semantic

Semantic diagonal vanishing on T, projected from actual annihilation.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute38Data.polarZeroSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute38Data D) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semantic

Semantic polar vanishing on T x M, projected from actual annihilation.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute38Data.radicalContainmentSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute38Data D) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semantic

Semantic radical containment, projected from actual determinant radical data.

Equations

• ⋯ = ⋯

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

Route38 projected to the coherent lower pushout packet consumed downstream.

Equations

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

Residual lowering hooks

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

Route38 central-pushout data from the actual scalar pushout and actual simple-head determinant packets.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquarePolarPackets_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

The three split square/polar Route37 packets, tied to the Route38 actual scalar pushout family.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSemanticDeterminantPackets_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The four semantic determinant Route37 packets, tied to the Route38 actual simple-head determinant packet.

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

Drop-in Route38 lower pushout provider, analogous to the Route37 provider.

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

Determinant packet projection through the Route38 lower pushout provider.

Acceptance checks / exact residual report