Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_509 :
Polynomial.coeff recurrence4Scalar2Exceptional 509 = -(3286127262682039007830194009 * 10 ^ 70 + 7252333216864906666914134348701962631713958065318777628611718246924102)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_510 :
Polynomial.coeff recurrence4Scalar2Exceptional 510 = -(2076904240066505215127 * 10 ^ 70 + 3788953879459631752678301240927480122043782278961977386044038067585468)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_511 :
Polynomial.coeff recurrence4Scalar2Exceptional 511 = -(529267548547218 * 10 ^ 70 + 9708428880715532513914162398938068069892536116436912506037075619677750)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_512 :
Polynomial.coeff recurrence4Scalar2Exceptional 512 = -(39070898 * 10 ^ 70 + 6620426043111253058945577805156479327197819386653956563973635407743647)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_513 :
Polynomial.coeff recurrence4Scalar2Exceptional 513 = -8317359457646468060504239164769546151922568984850618923928186578545690
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_514 :
Polynomial.coeff recurrence4Scalar2Exceptional 514 = -53701746906274322922389292413329009090012362832185396756764943