Recurrence 4 lookup certificate: Scalar1Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_514 :
Polynomial.coeff recurrence4Scalar1Exceptional 514 = -(382311299282171528059 * 10 ^ 70 + 1061929691291629800519727432439396177281329402809665493098298063237532)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_515 :
Polynomial.coeff recurrence4Scalar1Exceptional 515 = -(87642775825089 * 10 ^ 70 + 6211733089592221154479547065465371983150215697974868191249748699522037)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_516 :
Polynomial.coeff recurrence4Scalar1Exceptional 516 = -(4902123 * 10 ^ 70 + 1053036114136610684935595588880659686570387376240608956389794447820751)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_517 :
Polynomial.coeff recurrence4Scalar1Exceptional 517 = -920548595062435436386211821527454846543259162047702859738901029077210
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_518 :
Polynomial.coeff recurrence4Scalar1Exceptional 518 = -5549041120153585801193546258062638078959319258914876744495111