Route82 minimal-block determinant/pushout closer

Route81 leaves eight determinant/pushout atoms:

• a same-family pairing phi_lambda;
• an independently chosen square family q_lambda;
• the square diagonal and polar identities tying q_lambda to phi_lambda;
• naturality of phi_lambda;
• diagonal and polar vanishing on T;
• containment of the symmetrized polar radical in T.

This sidecar keeps the same downstream determinant-packet surface, but lowers that frontier in the shape of Section 7, prop:simpleheaddet.

The square family is no longer a residual atom: it is defined theorem-level as Quadratic.Extraspecial.extraspecialForm (phi lambda). The square diagonal and polar identities are then definitional/proven projections. The two vanishing Route81 atoms are replaced by one Annihilates packet for the actual extraspecial square, and the radical-containment atom is replaced by descended nonsingularity of that quotient form.

Manuscript anchors: Section 6 for the extraspecial square construction and Section 7, prop:simpleheaddet, for annihilation on T and nonsingularity on the simple head.

Route82 scalar central-pushout family

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

Route82 residual: the actual scalar central-pushout pairing family phi_lambda.

This is the irreducible construction datum left by the current Lean API: the quotient group objects K_lambda = K / ker lambda are not represented as first-class data here, so the family they induce is recorded directly.

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

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.toRoute81Pairing {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : MinimalBlockPreheadCentralPushoutPairingFamilyDataRoute81 D

Forget Route82's construction name to the Route81 pairing packet.

Equations

• Phi.toRoute81Pairing = { phi := Phi.phi }

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.squareFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : MinimalBlockPreheadCentralPushoutSquareFamilyDataRoute81 D

The Route82 square family is the proven extraspecial square attached to the same pairing.

Equations

• Phi.squareFamily = { square := fun (lam : Module.Dual (ZMod 2) D.R) => Q2Presentation.Quadratic.Extraspecial.extraspecialForm (Phi.phi lam) }

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.squareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : MinimalBlockPreheadCentralPushoutSquareDiagonalDataRoute81 Phi.toRoute81Pairing Phi.squareFamily

Route81 square diagonal, closed theorem-level from the extraspecial square definition.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.polarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : MinimalBlockPreheadCentralPushoutPolarSymmDataRoute81 Phi.toRoute81Pairing Phi.squareFamily

Route81 polar symmetry, closed theorem-level from the extraspecial polar definition.

Equations

• ⋯ = ⋯

Route82 simple-head proof packets

structure Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : Prop

Route82 residual: naturality of the actual scalar-pushout pairing.

• 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.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : Prop

Route82 residual: the extraspecial scalar-pushout square annihilates T.

This single packet is exactly the two displayed conclusions of prop:simpleheaddet, q_lambda|_T = 0 and b_lambda(T,M)=0, for the square defined from Phi.

• annihilates_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → Annihilates (Quadratic.Extraspecial.extraspecialForm (Phi.phi lam)) D.T

structure Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) (Ann : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi) : Prop

Route82 residual: after annihilation on T, the descended simple-head form is nonsingular.

This is the final paragraph of prop:simpleheaddet; Route81's radical containment is recovered below by pure quotient linear algebra.

• descended_nonsingular (lam : Module.Dual (ZMod 2) D.R) (hlam : lam ≠ 0) (hinv : ∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) : ⋯.descend.Nonsingular

Route82 residual axioms

axiom Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutPairingConstructionData_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D)

axiom Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutPairingNaturalityData_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : Nonempty (MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 Phi)

axiom Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutAnnihilationData_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) : Nonempty (MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi)

axiom Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutDescendedNonsingularData_route82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) (Ann : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi) : Nonempty (MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 Phi Ann)

Route81 projections from Route82 packets

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82.toRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D} (Nat : MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 Phi) : MinimalBlockPreheadCentralPushoutNaturalityDataRoute81 Phi.toRoute81Pairing

Route82 naturality as the Route81 naturality packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82.diagonalZeroRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D} (Ann : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi) : MinimalBlockPreheadCentralPushoutDiagonalZeroDataRoute81 Phi.toRoute81Pairing

Route82 annihilation gives Route81 diagonal vanishing.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82.polarZeroRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D} (Ann : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi) : MinimalBlockPreheadCentralPushoutPolarZeroDataRoute81 Phi.toRoute81Pairing

Route82 annihilation gives Route81 polar vanishing on T x M.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82.radicalContainmentRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {Phi : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D} {Ann : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi} (Nonsing : MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 Phi Ann) : MinimalBlockPreheadCentralPushoutRadicalContainmentDataRoute81 Phi.toRoute81Pairing

Route82 descended nonsingularity gives Route81 radical containment.

Equations

• ⋯ = ⋯

Coherent Route82 packet and provider

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

Coherent Route82 packet tying the construction and simple-head proof pieces to the same scalar-pushout pairing.

• pairing : MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D
• naturality : MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 self.pairing
• annihilation : MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 self.pairing
• nonsingular : MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 self.pairing ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data.toRoute81 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute82Data D) : MinimalBlockPreheadPushoutRoute81Data D

Route82 projected to the Route81 coherent packet.

Equations

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

Route82 constructors and drop-in provider

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute82Closers.minimalBlock_preheadPushoutRoute82Data_from_splitPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadPushoutRoute82Data D)

Assemble the coherent Route82 packet from its four residual packets.

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

Route82 projection to the Route81 square/polar packet surface.

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

Route82 projection to the semantic family and actual determinant packet.

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

Route82 lower pushout packet, avoiding all eight Route81 residual axioms.

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

Drop-in determinant-packet replacement for Route81.

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