Certificate extraction from empty canonical characteristic support

This file closes the algebraic end of the characteristic-support route. If the order-characteristic support of the literal canonical quotient is empty, then that quotient vanishes and membership of 1 in its two-generator right ideal yields the exact fixed-source Stafford certificate.

No theorem proving that the support is empty is assumed or supplied here.

theorem Stafford38.CharacteristicCanonicalCertificate.exists_fixedSource_certificate_of_orderCharacteristicSupport_eq_empty (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (hsupport : CharacteristicInitialIdeal.orderCharacteristicSupport k (WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate k n) d N) = ∅) : ∃ (R : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (S : WeylIteratedEquivalence.PresentedWeyl k (n + 1)), 1 = d * R + WeylIteratedEquivalence.presentedCoordinate k n ^ N * d * S

Empty order-characteristic support of the canonical right ideal gives the literal fixed-source certificate with source x^N.