Route41 minimal-block pushout/determinant provider

Route40 lowers the Section 7 determinant-pushout branch to two coherent leaves:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar routes the same lower pushout interface through the finer packet split already present in the Section 7 API. The scalar central pushout is recorded by the standard same-family square/polar packet MinimalBlockPreheadCentralPushoutStandardData: a shared phi_lambda, q_lambda, the square-diagonal identity, and polar-symmetry. The simple-head determinant side is recorded by MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData: the four same-family conclusions of manuscript Section 7.1, Proposition 7.4 (naturality, q_lambda|_T = 0, b_lambda(T,M) = 0, and polar-radical containment). The determinant square/polar background is the Section 6 construction of central double covers and extraspecial square forms.

No new axiom is introduced here. The checkpoints at the bottom should avoid both Route40 residual names and expose the finer standard/coherent packet floor.

Route41 packet

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

Route41 data for the Section 7 pushout branch.

The two fields are tied to the same semantic central-pushout family: determinant is indexed by standard.semanticData, so the later lower-route projection cannot combine square/polar data and determinant data from unrelated families.

• standard : MinimalBlockPreheadCentralPushoutStandardData D
• determinant : MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData self.standard.semanticData

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

The semantic central-pushout family selected by Route41.

Equations

• P.semantic = P.standard.semanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute41Data.squarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute41Data D) : MinimalBlockPreheadCentralPushoutSquarePolarData D

The combined square/polar packet recovered from the finer standard packet.

Equations

• P.squarePolar = Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofStandardData P.standard

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

The actual simple-head determinant packet recovered from the coherent semantic determinant packet, without using the Route40 bundled residual.

Equations

• ⋯ = ⋯

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

Route41 projected to the extraspecial simple-head determinant packet.

Equations

• ⋯ = ⋯

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

Route41 projected to the lower pushout packet consumed by integration.

Equations

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

Route-compatible hooks

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

Construct Route41 data from the finer standard square/polar packets and the coherent semantic determinant packet.

Residual report: this theorem replaces the two Route40 leaves by the standard same-family square/polar packet floor and the four coherent semantic determinant pieces from Proposition 7.4.

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

Route41 replacement for the Route40 combined square/polar leaf.

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

Route41 replacement for the Route40 bundled actual simple-head determinant leaf. This hook works for any already selected semantic central-pushout family.

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

Drop-in Route41 lower pushout provider.

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

Determinant packet projection through the Route41 lower pushout provider.

Acceptance checks / exact residual report