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.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_478 :
Polynomial.coeff recurrence4Scalar1Left 478 = (76617927338143601076825142693165744610855350449059046463371295680849 * 10 ^ 70 + 1173309816077408705403503732007686745621895623882019848969756322946079) * 10 ^ 70 + 2145580332853503076037999789227163269955799088769090188485447995366531
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_479 :
Polynomial.coeff recurrence4Scalar1Left 479 = -((1903232558365977745222195094334596286068933784794014069703181238874 * 10 ^ 70 + 8527881407487113734056431791885254483043366718434783127890829125446131) * 10 ^ 70 + 4739467666082295720646659415787364385220724512059180895457130378020247)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_480 :
Polynomial.coeff recurrence4Scalar1Left 480 = -((2311767725272703510138868364452838540214811436092215305279729634 * 10 ^ 70 + 1566518647150925547777756137340240582491756114759222120836996644527462) * 10 ^ 70 + 2351380421572136047098427771824784070488969940561033353836973464764369)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_481 :
Polynomial.coeff recurrence4Scalar1Left 481 = (681042433537116011461936400373663486544812855945356435088444202 * 10 ^ 70 + 3795053574652591827965978618172513526129631382791731625611759580532967) * 10 ^ 70 + 7317384426980898857937558372873014926388156086531206817517254799332631
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_482 :
Polynomial.coeff recurrence4Scalar1Left 482 = -((3620201332789129908964410227332555084202802584981366240567240 * 10 ^ 70 + 6644444125761547334851360324975201145562115428042947921245032567854212) * 10 ^ 70 + 929404223890537842107572338585150382162972183647217234221580063981464)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_483 :
Polynomial.coeff recurrence4Scalar1Left 483 = -((112277351554154146029971104357264501218295061252552485274746 * 10 ^ 70 + 4941379643852247214267758098604587426397693003752125377547029353150127) * 10 ^ 70 + 4691651129817395289925322406302388367260695629861924183593504111998155)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_484 :
Polynomial.coeff recurrence4Scalar1Left 484 = (483896825529224368740682534267589266519101572129919514718 * 10 ^ 70 + 9641938464366595833681814301462802395219745755907784886964858057301756) * 10 ^ 70 + 6942837111411385035010976875095087523546848156375534642489112440349742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_485 :
Polynomial.coeff recurrence4Scalar1Left 485 = (10823002484764297578795413874523516439038926659097055071 * 10 ^ 70 + 5198511830924633263821524588512087107345558176655132055402977220256304) * 10 ^ 70 + 8240807342631573005550889164945059440519341782480576100654667483410979
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_486 :
Polynomial.coeff recurrence4Scalar1Left 486 = -((9086493520009080072813555404541584083060480326075465 * 10 ^ 70 + 3621466692458210501447685779640465396370743748071798129393702185881285) * 10 ^ 70 + 4344662975781279296710983383094641359948895476724402026107567920861190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_487 :
Polynomial.coeff recurrence4Scalar1Left 487 = -((488098569552170745584585727183376474238181481777312 * 10 ^ 70 + 3258837501600606607854506806645887005828711993976709654698913474923003) * 10 ^ 70 + 1175700883211990100360267324962311444771812190167596442562043379323958)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_488 :
Polynomial.coeff recurrence4Scalar1Left 488 = -((512969154173947504953925736749959694086343295797 * 10 ^ 70 + 1798345946493874758024304355631635442379708749014018041895019455571946) * 10 ^ 70 + 4584015045915846467174590008934604903519428473933187664455050384379190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_489 :
Polynomial.coeff recurrence4Scalar1Left 489 = (10702863810482982922899521107030863542018343675 * 10 ^ 70 + 9761104376830142998628781912466458901265031668323550218581925888100175) * 10 ^ 70 + 9247567666013894815465720182165250166550344716294712964772934386604539
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_490 :
Polynomial.coeff recurrence4Scalar1Left 490 = (20826703252341907977512952903613860866956332 * 10 ^ 70 + 3373809806825989188609627331879827481264012924734516317998253004424105) * 10 ^ 70 + 9563786402942786956281140938145759577381604313205839586250497213245376
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_491 :
Polynomial.coeff recurrence4Scalar1Left 491 = -((122572172829056251319944553018445367202020 * 10 ^ 70 + 4531443167970897363002015864071692428173030752131086275833143794066403) * 10 ^ 70 + 2505504174146451824830207814114612045721804077619448769310963188507117)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_492 :
Polynomial.coeff recurrence4Scalar1Left 492 = -((269080270014444379375644620052318174761 * 10 ^ 70 + 2724436497264058935726052869688767046894464683465391283390726858654109) * 10 ^ 70 + 1378602986226539652667848730663980129395748396872735909516884869316672)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_493 :
Polynomial.coeff recurrence4Scalar1Left 493 = (864930088125143328797236099854936859 * 10 ^ 70 + 4449212071870410428286575233567103022645380580596732391134128596037725) * 10 ^ 70 + 5261361626206944248126085308996602519310369432295196830803106417370020
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_494 :
Polynomial.coeff recurrence4Scalar1Left 494 = (1634992009730427461628718412101790 * 10 ^ 70 + 3130940187929764716041065599524067396086959119957562519274925054729441) * 10 ^ 70 + 2044283424318939762108060859576576458358560735485486714601898135440059
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_495 :
Polynomial.coeff recurrence4Scalar1Left 495 = -((4066801101171647450358554690058 * 10 ^ 70 + 6280219180405610278446630003479975693122091035866761939446246148801003) * 10 ^ 70 + 5509052338760109614571661169920029850625627741010279250994066209296986)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_496 :
Polynomial.coeff recurrence4Scalar1Left 496 = -((4549824448185914976154315672 * 10 ^ 70 + 7333109294712773953668093621060566564814390510393657843523904712911108) * 10 ^ 70 + 6743317349174297487739667913049258896893823003601407913254345899379740)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_497 :
Polynomial.coeff recurrence4Scalar1Left 497 = (11693526468040997849471438 * 10 ^ 70 + 7561251403231174258533018570541425777176474015486855231744764169527289) * 10 ^ 70 + 6307948498191759474127323098095148587108601331816849292997160433359208
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_498 :
Polynomial.coeff recurrence4Scalar1Left 498 = (3043400530706908746879 * 10 ^ 70 + 7146079138979986569818496374999971903265115722485976463886497165451738) * 10 ^ 70 + 7371991053229004212438988163084077685079096320541827176501859953188699
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_499 :
Polynomial.coeff recurrence4Scalar1Left 499 = -((14765065397913137520 * 10 ^ 70 + 2829871521130057125392814156545376428289147416814950040635405692668204) * 10 ^ 70 + 8131233845113778016822919927741124428196711561370804035005340410299595)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_500 :
Polynomial.coeff recurrence4Scalar1Left 500 = (4096177259945854 * 10 ^ 70 + 561994973709372331441580909105725500841708185760307680103582380313332) * 10 ^ 70 + 7326320943905408970799693118316099540943484640481544241546400010379947
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_501 :
Polynomial.coeff recurrence4Scalar1Left 501 = (4100236503153 * 10 ^ 70 + 4563028591500413567847715834609836867469035907121190728779049819991090) * 10 ^ 70 + 588892403011822063533653211049258753035875524089637184001037509784159
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_502 :
Polynomial.coeff recurrence4Scalar1Left 502 = -((1929208386 * 10 ^ 70 + 7320123515902100464770449127869507302224751327366322998179999908554082) * 10 ^ 70 + 3237127582974178648626860623806100429573922207030128731038898193920051)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_503 :
Polynomial.coeff recurrence4Scalar1Left 503 = -((16160 * 10 ^ 70 + 3743361590754193566115413777332267462175651944725778324587212830422544) * 10 ^ 70 + 3573830177128730040798133491935530859574228933220305089197835646792217)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_504 :
Polynomial.coeff recurrence4Scalar1Left 504 = (81 * 10 ^ 70 + 9326337334966632452168828177338924544436306096197665168304263923139408) * 10 ^ 70 + 6522482284549335450369409720197746279156164864689850451624191892719438
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_505 :
Polynomial.coeff recurrence4Scalar1Left 505 = -(73512835015762238232649383817770764141682088569316112889135223020040 * 10 ^ 70 + 5098786130644309952903187260363657799160192191134302648534064391455705)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_506 :
Polynomial.coeff recurrence4Scalar1Left 506 = -(2111233048858045200657968856728385218104357508361392142020176247 * 10 ^ 70 + 6180426832024095620843805339086977293093969483926696777238392473124672)