Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_479 : Polynomial.coeff recurrence4Scalar2Second 479 = -((353733031247106479630356788093613482751910870179256176879008 * 10 ^ 70 + 1649254008061647421051108614049255826885163101305931186516833715452519) * 10 ^ 70 + 8652175512116257891078733155401111831884538143467266274829509202089360)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_480 : Polynomial.coeff recurrence4Scalar2Second 480 = (2015202915221174499612266669695133213667787404826653276836 * 10 ^ 70 + 2317752083450044873602709502963541054073270898951876598535474907258749) * 10 ^ 70 + 5266859175739262723753818701048570583832048152590720280179825868989763

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_481 : Polynomial.coeff recurrence4Scalar2Second 481 = (34003483978655048223368427363173312062748506488740908071 * 10 ^ 70 + 9452501419159790708516537838665755368880362023396293746242665327632510) * 10 ^ 70 + 1790298048145889331731179737283712786476316325665176133156630804170332

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_482 : Polynomial.coeff recurrence4Scalar2Second 482 = -((72292529447907044003878789563483386526912521421904021 * 10 ^ 70 + 4698251658201632232799827274790552795252062239774829058595071611291474) * 10 ^ 70 + 9987386498080211950486853465343475423902196242206392492216903002335876)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_483 : Polynomial.coeff recurrence4Scalar2Second 483 = -((1637668530795005387127065445974718885382163688282687 * 10 ^ 70 + 2919212761854040818961910469258328892219871082464991451962304037591799) * 10 ^ 70 + 8237236079311997938183801881068851898940719420247348178308426536768238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_484 : Polynomial.coeff recurrence4Scalar2Second 484 = -((168369034536447202423148196017694838334323366001 * 10 ^ 70 + 2365957226321887934380999261648460742543313935104824687231458780968350) * 10 ^ 70 + 9424037636330060708470915256245268874377934291456894191324434603768551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_485 : Polynomial.coeff recurrence4Scalar2Second 485 = (38854043587349226120666431324938742400840286489 * 10 ^ 70 + 9442456745950320471500869514669986724241776380836222970377290975121937) * 10 ^ 70 + 2334109120762371989391302257523219160373473269580894391157053242547027

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_486 : Polynomial.coeff recurrence4Scalar2Second 486 = (43712356604366107406477154614520992065369454 * 10 ^ 70 + 9934601297370444733869538644651106040659819756250414904462567900571048) * 10 ^ 70 + 2362537183495935147646378083282970325032341674646049147761587801851372

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_487 : Polynomial.coeff recurrence4Scalar2Second 487 = -((483699474658866019642214479757066180091999 * 10 ^ 70 + 3571333231496383539320921232081234991779712040964503570184428900163672) * 10 ^ 70 + 5132671862624450060660716909293928603998005624617715441170201087815454)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_488 : Polynomial.coeff recurrence4Scalar2Second 488 = -((670995769317569655360643557778612512704 * 10 ^ 70 + 6054609382140276179475562713979245635279623045141166716654825333694398) * 10 ^ 70 + 7225964776062004801464783644583740754391086538855869784122802508583945)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_489 : Polynomial.coeff recurrence4Scalar2Second 489 = (3624479245939078674575004575387854946 * 10 ^ 70 + 8931249623646201703147289497717593373278319026448499377587384487984608) * 10 ^ 70 + 664528773335221356617081371138411378149050246437962221188356611483271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_490 : Polynomial.coeff recurrence4Scalar2Second 490 = (4175843000250261577583485187707315 * 10 ^ 70 + 3890995107184590002716515410710756062049185630709475672188477808794056) * 10 ^ 70 + 8519610385372815948531292030295733477289157927657806296907038456170607

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_491 : Polynomial.coeff recurrence4Scalar2Second 491 = -((17242814282733225822308092561192 * 10 ^ 70 + 193992968723818122380751181604221947213253532319416124511077659597678) * 10 ^ 70 + 1240257105662804077898108808211189518112391569337367891364743106043911)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_492 : Polynomial.coeff recurrence4Scalar2Second 492 = -((10010267669914903266445747377 * 10 ^ 70 + 4556653436163793616688422451583791523864933229391399559813486185402025) * 10 ^ 70 + 5236256752169598566174808554040600094286723418239042697871947590071323)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_493 : Polynomial.coeff recurrence4Scalar2Second 493 = (47735666275717958374431810 * 10 ^ 70 + 6355694000823590604257289272786206223175719330614325956280721809335534) * 10 ^ 70 + 4771459598174019554198091278364451394563363025594795227018095243580368

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_494 : Polynomial.coeff recurrence4Scalar2Second 494 = -((2889234114224447985588 * 10 ^ 70 + 5027780204918186454960743752105356919589260090044610176432776148069201) * 10 ^ 70 + 1873842726592750124378104683028620552076183232907243815011528599582101)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_495 : Polynomial.coeff recurrence4Scalar2Second 495 = -((55454675886263960971 * 10 ^ 70 + 2158830624743054654167232811686666650893152469440178649946445839404132) * 10 ^ 70 + 9304345067036361389774504556800810116085990468495206604679269358952978)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_496 : Polynomial.coeff recurrence4Scalar2Second 496 = (26577365035348395 * 10 ^ 70 + 8741933860107924313841477773357114092869617705291684957631530739563236) * 10 ^ 70 + 5942797755658846946043254455374169073314590946991277930061310875483099

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_497 : Polynomial.coeff recurrence4Scalar2Second 497 = (12180529795001 * 10 ^ 70 + 2666224381798465850821587174901860934390708524974693757324123171147826) * 10 ^ 70 + 2247251623400923703632718015111713010358487362804853898879261205070552

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_498 : Polynomial.coeff recurrence4Scalar2Second 498 = -((9017389182 * 10 ^ 70 + 7897337075990179490066100041678260512517940685012316293260044157052797) * 10 ^ 70 + 2086208796860540674903086738679214122502434294783855132364207382081470)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_499 : Polynomial.coeff recurrence4Scalar2Second 499 = (634301 * 10 ^ 70 + 4986959757231993035612431404330096506145454134540113984208230766883320) * 10 ^ 70 + 9875601047755915602285991758638748992857628696862920360001929935250453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_500 : Polynomial.coeff recurrence4Scalar2Second 500 = (317 * 10 ^ 70 + 1108679509775633731941547484131238097927017627763168779045443370489752) * 10 ^ 70 + 4923946830319279410610718587545169435031883366772457177521672062792271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_501 : Polynomial.coeff recurrence4Scalar2Second 501 = -(437200125348509872909362613006970914045352907267942664536892293818840 * 10 ^ 70 + 7144977925149459467131746782569556523978628622531041556403663001708572)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_502 : Polynomial.coeff recurrence4Scalar2Second 502 = 944010417163729175905148501046034054109845626740127985789602154 * 10 ^ 70 + 5512766047447590596295272190374229603685020928458440745054494863059394

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_503 : Polynomial.coeff recurrence4Scalar2Second 503 = 1364854150883667007088643622218049881775197025490828737116723 * 10 ^ 70 + 5183845546378096642475405626053413550439166260628826907588695137246956

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_504 : Polynomial.coeff recurrence4Scalar2Second 504 = -(35142088989746646112129009204965402597315375812469609243 * 10 ^ 70 + 2378926503787518583284845125844366350565281602986993937856106210415830)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_505 : Polynomial.coeff recurrence4Scalar2Second 505 = -(74479958616327973954258061729276413847720411628052 * 10 ^ 70 + 7315167106764478907563962955403981593041975238420992948015918739919958)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_506 : Polynomial.coeff recurrence4Scalar2Second 506 = 5278188159266104828692774628474604389418062603 * 10 ^ 70 + 1883241543745103720691624128562936870410516570955621904925414812292280

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_507 : Polynomial.coeff recurrence4Scalar2Second 507 = -(20989194249703967237553122979278067534289 * 10 ^ 70 + 9088808049629890643227350118847065593637141714434960497777560703963531)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_508 : Polynomial.coeff recurrence4Scalar2Second 508 = -(9455513721031085369081296427656954 * 10 ^ 70 + 7547658778044950554157766523318091157873725542647202015543705381121735)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_509 : Polynomial.coeff recurrence4Scalar2Second 509 = 61478833047931952695502959092 * 10 ^ 70 + 2215167591001751950457090208303232392772430739751155949814336127272578

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_510 : Polynomial.coeff recurrence4Scalar2Second 510 = -(25028457005463903609033 * 10 ^ 70 + 392658619717535778214278452994554174949643287788568440850691407172734)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_511 : Polynomial.coeff recurrence4Scalar2Second 511 = -(418465745244810 * 10 ^ 70 + 4021138257162163214944540056246830926172469261974007999785805391953898)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_512 : Polynomial.coeff recurrence4Scalar2Second 512 = 272215716 * 10 ^ 70 + 4768046535320773445155153178807157250972134303141630745581461393720316

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_513 : Polynomial.coeff recurrence4Scalar2Second 513 = -(4 * 10 ^ 70 + 2424700758820261395924300578952097900397848621631505830768407090338181)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_514 : Polynomial.coeff recurrence4Scalar2Second 514 = 11231002459417880704909299761270836144720659591828868792082713