Routed lower Section 7 pushout proof packet

This sidecar is the route-ready layer above MinimalBlockPushoutLowerProofs. It replaces the seven independent final-closure PREHEAD PUSHOUT / EXTRASPECIAL packets by one coherent same-family residual:

• a central-pushout self-duality family phi;
• the simple-head determinant theorem for the extraspecial square form built from that same phi.

The old square, polar, naturality, diagonal-zero, polar-zero, and radical containment packets are then projections from that one packet.

One coherent lower packet

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

Coherent route packet for the Section 7 determinant pushout.

The determinant field is deliberately indexed by the extraspecial family induced from selfDuality, so every downstream projection uses the same scalar pushout pairing. This is stronger than the previous final route, where the central pushout family, square/polar identities, and extraspecial determinant conditions were seven independent residual axioms.

• selfDuality : MinimalBlockPreheadCentralPushoutSelfDualityData D
• simpleHeadDeterminant : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality self.selfDuality)

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

The remaining coherent Section 7 pushout residual.

Manuscript anchor: Section 7, prop:simpleheaddet, applied to the scalar central pushouts K_lambda = K / ker lambda of the realized pre-head tower.

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

The central-pushout quadratic family obtained from the route packet's self-duality family.

Equations

• P.quadraticFamily = Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutQuadraticFamilyData.ofSelfDuality P.selfDuality

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

The square-diagonal projection for the same quadratic family.

Equations

• ⋯ = ⋯

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

The polar-symmetry projection for the same quadratic family.

Equations

• ⋯ = ⋯

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

The bare extraspecial family induced by the route packet's self-duality family.

Equations

• P.extraspecialFamily = Q2Presentation.Induction.MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality P.selfDuality

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialNaturalityData P.extraspecialFamily

The naturality projection from the same simple-head determinant packet.

Equations

• ⋯ = ⋯

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

The equivariant extraspecial family built from the determinant packet.

Equations

• P.equivariantFamily = ⋯.toEquivariantFamily

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.diagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialDiagonalZeroData P.equivariantFamily

The diagonal-zero projection on the equivariant family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.polarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialPolarZeroData P.equivariantFamily

The polar-zero projection on the equivariant family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.radicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialRadicalContainmentData P.equivariantFamily

The polar-radical containment projection on the equivariant family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.annihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialAnnihilationData P.equivariantFamily

Determinant annihilation assembled from the diagonal and polar projections.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRouteLowerData.radicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : MinimalBlockPreheadExtraspecialRadicalData P.equivariantFamily

Determinant radical data assembled from the radical-containment projection.

Equations

• ⋯ = ⋯

Projection theorems for the seven old packet boundaries

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

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquareDiagonalData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily)

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarSymmData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily)

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialNaturalityData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData P.extraspecialFamily)

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialDiagonalZeroData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData P.equivariantFamily)

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPolarZeroData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData P.equivariantFamily)

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalContainmentData_from_routeLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRouteLowerData D) : Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData P.equivariantFamily)

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

Residual-backed coherent projection of the central-pushout triple.

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

Residual-backed coherent projection of the extraspecial determinant packet.

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

Route-ready replacement for minimalBlock_preheadDeterminantPackets_from_standardPushoutPackets.

The axiom closure contains one coherent lower pushout residual instead of the seven independent central-pushout/extraspecial residuals.