Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1LeftPart4

Recurrence 4 lookup certificate: Scalar1Left coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_507 :
Polynomial.coeff recurrence4Scalar1Left 507 = 282418050029497846408161074263766864233027819293410625266258 * 10 ^ 70 + 2279599935421952757550001018448753724534715851627960893298113808631111
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_508 :
Polynomial.coeff recurrence4Scalar1Left 508 = -(4464700312163327014450802551041523337853579178887915996 * 10 ^ 70 + 3048766636643252066726042150275630674665860124517202875594477147230077)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_509 :
Polynomial.coeff recurrence4Scalar1Left 509 = -(53197206054541567642820630827558307358353983117700 * 10 ^ 70 + 6325352178404354155511038352890892625536380443905876818651384651764999)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_510 :
Polynomial.coeff recurrence4Scalar1Left 510 = 853922260578295821264700576035370066227750258 * 10 ^ 70 + 9569614440693689882548358205912974348429555942481613141276928872996296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_511 :
Polynomial.coeff recurrence4Scalar1Left 511 = -(1996454667743144854026069862507209358671 * 10 ^ 70 + 776571697563843844700502687989659754173453070123268601207258248461365)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_512 :
Polynomial.coeff recurrence4Scalar1Left 512 = -(4741800665475652951534851095641980 * 10 ^ 70 + 4051208260735686490724437346575174313559863184666227513531833190533302)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_513 :
Polynomial.coeff recurrence4Scalar1Left 513 = 7296889776352632347808253140 * 10 ^ 70 + 8521904392099234680384834434145104407652236391383600390476693578297617
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_514 :
Polynomial.coeff recurrence4Scalar1Left 514 = -(1867661148314463135041 * 10 ^ 70 + 5534006381165931989624797475560302904509541100683181489719839367135185)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_515 :
Polynomial.coeff recurrence4Scalar1Left 515 = -(338068141793463 * 10 ^ 70 + 873026389098247449799006523184800147209602376762417909059470251924135)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_516 :
Polynomial.coeff recurrence4Scalar1Left 516 = 21498246 * 10 ^ 70 + 3637121555508487754702623968909536557562407109244665710400458262238609
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_517 :
Polynomial.coeff recurrence4Scalar1Left 517 = -2666287900015295305458274149235472678958732330604976322992876224204960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_518 :
Polynomial.coeff recurrence4Scalar1Left 518 = -9430486515507006953907938380010713558764573967437259715591900