Route49 minimal-block pushout/determinant narrowing

This sidecar records the exact determinant data consumed by the nonterminal Fourier branch, rather than routing through the broader actual central-extension pushout packet.

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

Route49 pre-head determinant packet.

The integrated branch only needs one same-family equivariant extraspecial family together with its annihilation and radical-containment packets.

• equivariantFamily : MinimalBlockPreheadExtraspecialEquivariantFamilyData D
• annihilationData : MinimalBlockPreheadExtraspecialAnnihilationData self.equivariantFamily
• radicalData : MinimalBlockPreheadExtraspecialRadicalData self.equivariantFamily

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

Projection from the older actual central-extension packet to the exact determinant packet consumed downstream.

Equations

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

axiom Q2Presentation.Induction.minimalBlock_preheadDeterminantRoute49Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadDeterminantRoute49Data D)

Route49's single pushout/determinant residual.

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

The Route49 determinant packet is a projection of the older actual-pushout packet; this is an audit theorem, not used by the final route.

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

Route49 determinant-packet projection consumed by the integrated nonterminal branch.