Recurrence 4 lookup certificate: Scalar0Exceptional degree bound

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_low (n : ℕ) (h : n < 1) : Polynomial.coeff recurrence4Scalar0Exceptional n = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_natDegree_le : Polynomial.natDegree recurrence4Scalar0Exceptional ≤ 522

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_high (n : ℕ) (h : 522 < n) : Polynomial.coeff recurrence4Scalar0Exceptional n = 0