Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2ExceptionalPart3

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)