Route81 minimal-block determinant/pushout closer

Route80's determinant/pushout provider leaves six Section 7 atoms:

• the split scalar central-pushout square/polar family;
• three Route79 fields for the actual simple-head determinant theorem.

This sidecar keeps the same downstream determinant-packet surface, but routes it through smaller same-family packets. The square/polar family is split into an explicit pairing family, an explicit square family, and the two identities tying them together. The actual simple-head determinant theorem is split into the four manuscript pieces of prop:simpleheaddet: naturality, diagonal vanishing on T, polar vanishing on T x M, and polar-radical containment.

Manuscript anchors: Section 6 for the square/polar determinant context and Section 7, prop:simpleheaddet, for the simple-head pushout theorem.

Route81 split scalar central-pushout family

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

Route81 residual: the scalar-pushout pairing family phi_lambda.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

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

Route81 residual: the scalar-pushout square maps q_lambda.

• square : Module.Dual (ZMod 2) D.R → Quadratic.QuadF2 D.M

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquareDiagonalDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) (Sq : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D) : Prop

Route81 residual: q_lambda(m) is the diagonal of phi_lambda.

• square_diagonal (lam : Module.Dual (ZMod 2) D.R) (m : D.M) : (Sq.square lam).form m = ((Phi.phi lam) m) m

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarSymmDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) (Sq : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D) : Prop

Route81 residual: the polar form is the symmetrized phi_lambda pairing.

• polar_symm (lam : Module.Dual (ZMod 2) D.R) (m m' : D.M) : ((Sq.square lam).polar m) m' = ((Phi.phi lam) m) m' + ((Phi.phi lam) m') m

Route81 split simple-head determinant pieces

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalityDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Prop

Route81 residual: naturality of the same phi_lambda family.

• phi_natural (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m m' : D.M), ((Phi.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((Phi.phi lam) m) m'

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutDiagonalZeroDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Prop

Route81 residual: diagonal vanishing q_lambda|_T = 0, written on phi.

• diagonal_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ((Phi.phi lam) t) t = 0

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarZeroDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Prop

Route81 residual: polar vanishing on T x M, written on phi.

• symm_polar_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ∀ (m : D.M), ((Phi.phi lam) t) m + ((Phi.phi lam) m) t = 0

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRadicalContainmentDataRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Prop

Route81 residual: the symmetrized polar radical is contained in T.

• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((Phi.phi lam) m) m' + ((Phi.phi lam) m') m = 0) → m ∈ D.T

Route81 residual axioms

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

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

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquareDiagonalData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) (Sq : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalDataRoute81 Phi Sq)

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarSymmData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) (Sq : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmDataRoute81 Phi Sq)

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutNaturalityData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalityDataRoute81 Phi)

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutDiagonalZeroData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroDataRoute81 Phi)

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarZeroData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroDataRoute81 Phi)

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRadicalContainmentData_route81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D) : Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentDataRoute81 Phi)

Coherent Route81 packet and projections

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

Coherent Route81 packet tying all split pushout data to the same pairing.

• pairing : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D
• squareFamily : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D
• squareDiagonal : MinimalBlockPreheadCentralPushoutSquareDiagonalDataRoute81 self.pairing self.squareFamily
• polarSymm : MinimalBlockPreheadCentralPushoutPolarSymmDataRoute81 self.pairing self.squareFamily
• naturality : MinimalBlockPreheadCentralPushoutNaturalityDataRoute81 self.pairing
• diagonalZero : MinimalBlockPreheadCentralPushoutDiagonalZeroDataRoute81 self.pairing
• polarZero : MinimalBlockPreheadCentralPushoutPolarZeroDataRoute81 self.pairing
• radicalContainment : MinimalBlockPreheadCentralPushoutRadicalContainmentDataRoute81 self.pairing

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

The Route80 split quadratic-family packet projected from Route81.

Equations

• P.quadraticFamily = { phi := P.pairing.phi, square := P.squareFamily.square }

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

The Route80 square-diagonal packet projected from Route81.

Equations

• ⋯ = ⋯

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

The Route80 polar-symmetry packet projected from Route81.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRoute81Data.standardData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute81Data D) : MinimalBlockPreheadCentralPushoutStandardData D

The standard square/polar packet selected by Route81.

Equations

• P.standardData = { quadraticFamily := P.quadraticFamily, squareDiagonal := ⋯, polarSymm := ⋯ }

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

The semantic central-pushout family selected by Route81.

Equations

• P.semantic = { phi := P.pairing.phi }

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

Route81 naturality as the existing semantic naturality packet.

Equations

• ⋯ = ⋯

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

Route81 diagonal vanishing as the existing semantic packet.

Equations

• ⋯ = ⋯

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

Route81 polar vanishing as the existing semantic packet.

Equations

• ⋯ = ⋯

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

Route81 radical containment as the existing semantic packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadPushoutRoute81Data.actualSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute81Data D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData P.semantic

The split actual determinant packet projected from Route81.

Equations

• ⋯ = ⋯

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

The actual simple-head determinant packet projected from Route81.

Equations

• ⋯ = ⋯

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

The extraspecial simple-head determinant packet projected from Route81.

Equations

• ⋯ = ⋯

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

Route81 projected to the lower pushout packet consumed downstream.

Equations

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

Route81 constructors and drop-in provider

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

Assemble the coherent Route81 packet from its split residuals.

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

Route81 projection to the Route80 square/polar packet surface.

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

Route81 projection to the semantic family and actual determinant packet.

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

Route81 lower pushout packet, avoiding the Route80 residual axioms.

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

Drop-in determinant-packet replacement for Route80/Route79.

The axiom closure contains the eight Route81 split packets above, and does not use the six Route80 determinant/pushout residual names.