Recurrence 4 lookup certificate: Scalar0Left 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.recurrence4Scalar0Left_coeff_75 :
Polynomial.coeff recurrence4Scalar0Left 75 = -((105832534607992601390946781341936154732831323104222217088851448 * 10 ^ 70 + 9934214351316092933609306547538763337424798219349898340829761179159387) * 10 ^ 70 + 4515992905543326714096843576117808147330229577150761276376218692201020)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_76 :
Polynomial.coeff recurrence4Scalar0Left 76 = (1770268366545030571237332755521915622745178936516580995156217597 * 10 ^ 70 + 496475983230794100357615087969853697899763826330009305032778335686059) * 10 ^ 70 + 8815840389438472504380624126782668735815392497947761594329818137372585
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_77 :
Polynomial.coeff recurrence4Scalar0Left 77 = -((24603505950326686471548493515986848469030849201240722220176265932 * 10 ^ 70 + 122253321720019354770543077447014219320573741169045682304568317190767) * 10 ^ 70 + 2581916809575856029766721412591219226781399076540399262805579046005386)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_78 :
Polynomial.coeff recurrence4Scalar0Left 78 = (217926076760720290722142859219290063753548009634336733109061958085 * 10 ^ 70 + 7060552760482739511377927516663527879844067589191608495696059322932648) * 10 ^ 70 + 5489420132449559046845681570617919460960234270074968762058659409991969
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_79 :
Polynomial.coeff recurrence4Scalar0Left 79 = (1673048639643041946495720815330164736389579028738234457532966138561 * 10 ^ 70 + 4139134060903693740819582752074656954601015102039424799611516548854347) * 10 ^ 70 + 456911714231995683263632626612181058624148438699425644727844322003118
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_80 :
Polynomial.coeff recurrence4Scalar0Left 80 = -((150354273604292061758884674484842375753657384723692167592568943023249 * 10 ^ 70 + 6153159458717098656821212263670528671372714752218782263734229721932027) * 10 ^ 70 + 3327212050189921311361794453915865938617218860491415517010013547784868)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_81 :
Polynomial.coeff recurrence4Scalar0Left 81 = (4981786765728666368063660286162624166841278066940512484046434351253009 * 10 ^ 70 + 1762129820505435569771546041626096146468711873650944412719817691803241) * 10 ^ 70 + 2957628292413822506142328195766960965260498601481653241446174414260771
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_82 :
Polynomial.coeff recurrence4Scalar0Left 82 = -(((12 * 10 ^ 70 + 7301837273871653453109977975546464419408692385790457471506556333852224) * 10 ^ 70 + 3034948897822938594259810729028485480755012872233451767577542403496974) * 10 ^ 70 + 5994246679932087578188387108413309425138933025214661730641388325020322)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_83 :
Polynomial.coeff recurrence4Scalar0Left 83 = ((281 * 10 ^ 70 + 1742355349828597490060188186106307788062875232531916439096158671538778) * 10 ^ 70 + 1851440391759689462039974350351558779370356263813657871702853468035446) * 10 ^ 70 + 9967329524969851474161804409736576708991951749878001356347818694465400
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_84 :
Polynomial.coeff recurrence4Scalar0Left 84 = -(((5571 * 10 ^ 70 + 6973589885254018468354839693466303883108942971566363612041680028476878) * 10 ^ 70 + 9319328186049321918073744999837372371027053482978597187508682344531585) * 10 ^ 70 + 9577289611199652251477055292993631188387496235535973825782408566155892)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_85 :
Polynomial.coeff recurrence4Scalar0Left 85 = ((100317 * 10 ^ 70 + 3152013465218831836859138496288695721617237283479965790396757069383939) * 10 ^ 70 + 8221977815766014617374053136334199863891405400821780664031781215665719) * 10 ^ 70 + 3435523252940950997196195705774546690076512318660328109647731992782783
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_86 :
Polynomial.coeff recurrence4Scalar0Left 86 = -(((1639250 * 10 ^ 70 + 1638350126170341529400106319763866406388677181850564839803270068677311) * 10 ^ 70 + 3987037231085030036003351022021931418229307582025684864586408976312183) * 10 ^ 70 + 7499187374975944850275754056063439010942525894124709658665692626778906)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_87 :
Polynomial.coeff recurrence4Scalar0Left 87 = ((23919922 * 10 ^ 70 + 1226624173898458764923325098378231568741821121049394705653708171688484) * 10 ^ 70 + 7920282606404260801297533039906673418230162889374292708593296744113445) * 10 ^ 70 + 5400135522514710789634612829207816123902688511004907483750781504432370
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_88 :
Polynomial.coeff recurrence4Scalar0Left 88 = -(((297325431 * 10 ^ 70 + 3112194823407423820224136397595532040405700977289944640850403370867936) * 10 ^ 70 + 3784577238991989068636925554490985366498050463472770150807910790631668) * 10 ^ 70 + 921768348613827437736365125401431371895342452280230944559253603424459)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_89 :
Polynomial.coeff recurrence4Scalar0Left 89 = ((2682380163 * 10 ^ 70 + 6172666377700809967195636266173019641638348181703839262400826698472668) * 10 ^ 70 + 4734863992658268868610745525692773497518467279450729256026565658898314) * 10 ^ 70 + 7337910829559052052277290742847117702954285276331837678466499568964234
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_90 :
Polynomial.coeff recurrence4Scalar0Left 90 = -(((1167265320 * 10 ^ 70 + 1318691109367909353441514947164116294366398751299543817199147634664391) * 10 ^ 70 + 1478593581820974122557484500137872072600269452514704688813137558967017) * 10 ^ 70 + 6908381415303840350261746171215610593833181357287781005324846709281582)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_91 :
Polynomial.coeff recurrence4Scalar0Left 91 = -(((720891350617 * 10 ^ 70 + 8412404548108106748800997182410828552789314827821974384658605090018684) * 10 ^ 70 + 2893587909559923665792549721733907570378843408689753966698192394093823) * 10 ^ 70 + 5269729633881917609597894366251774188613991504706904139605961190217580)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_92 :
Polynomial.coeff recurrence4Scalar0Left 92 = ((23305656252322 * 10 ^ 70 + 3399262422030462410334262475490194061518169636224916280866558497715434) * 10 ^ 70 + 3324917358927224806416589158759888486248942952725428970567539923233790) * 10 ^ 70 + 9273624398854588217805561768656624430271539086256833711168192033710590
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_93 :
Polynomial.coeff recurrence4Scalar0Left 93 = -(((541500941232666 * 10 ^ 70 + 8811084335905720490929652746104786873329286524791508690579347998061183) * 10 ^ 70 + 2489666089838820706575792570828499676362074220139678678586302739725899) * 10 ^ 70 + 5128470707859306291869926911683582876604377172646479603467973297688547)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_94 :
Polynomial.coeff recurrence4Scalar0Left 94 = ((10801120164071971 * 10 ^ 70 + 7527271279984338084602087679231794249038845163738001403248742306134420) * 10 ^ 70 + 535076974613238680494849541185411377750116296362633904573371203090385) * 10 ^ 70 + 5797619579458386619985850277819319855699187889277135836456316090657606
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_95 :
Polynomial.coeff recurrence4Scalar0Left 95 = -(((195520904181684886 * 10 ^ 70 + 9605159408041373721645797937635057871942479247100099667232495278655327) * 10 ^ 70 + 5598449143641440021625457997535882255424283084119351019721329207556035) * 10 ^ 70 + 2890543901431255903592566654736325086236095666230947506319146725531089)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_96 :
Polynomial.coeff recurrence4Scalar0Left 96 = ((3293327121765458463 * 10 ^ 70 + 5189739665568590863550207078344040637263042089630665001655560507901249) * 10 ^ 70 + 303366534141634762367369689655977913672856181008490865621954885278230) * 10 ^ 70 + 5297683410859280861764113987182782743430334258861520878435433635595481
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_97 :
Polynomial.coeff recurrence4Scalar0Left 97 = -(((52323885106779167934 * 10 ^ 70 + 9781604901718306325025182175536158890979842883171227022028163463055693) * 10 ^ 70 + 2012764391058947798096023124799802363867622933843783863159292921816853) * 10 ^ 70 + 9240933170007009380043028042657682041249644750108986791798799939804889)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_98 :
Polynomial.coeff recurrence4Scalar0Left 98 = ((790689453196746369879 * 10 ^ 70 + 515009917705799283807268613991265460978478008817943920370735063360823) * 10 ^ 70 + 6468324798674430030720098905547828520945719948495619897453547576280700) * 10 ^ 70 + 223287471507567235803216014513284562131007321622643601945354269444807
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_99 :
Polynomial.coeff recurrence4Scalar0Left 99 = -(((11427751295482303261566 * 10 ^ 70 + 4935258101913146100876446959824364460324419561440548523231672932405872) * 10 ^ 70 + 580790734073699170275666512780694116529525788936551991691949836462921) * 10 ^ 70 + 5085469181161670752888138655161892820756524865829391529811129297836639)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_100 :
Polynomial.coeff recurrence4Scalar0Left 100 = ((158587895501008482492398 * 10 ^ 70 + 8316510687979620163528872140030644433144578870786561989858367549478383) * 10 ^ 70 + 8321389390428394213226864959473284353680431123319086331946295697567432) * 10 ^ 70 + 32362862975085344913798457297027223530957090107445862832816352992287
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_101 :
Polynomial.coeff recurrence4Scalar0Left 101 = -(((2119343666560896093707196 * 10 ^ 70 + 7447801553911981893218984526307386025272430389502154423083122800227386) * 10 ^ 70 + 8901551945234926700278184207775190227637309938693997316170602436733582) * 10 ^ 70 + 8400070654306381237037956269298661710431326102168652196995133444009560)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_102 :
Polynomial.coeff recurrence4Scalar0Left 102 = ((27335948379356391712975000 * 10 ^ 70 + 1180631519234737820470549716144117066327932819145924367133595622674456) * 10 ^ 70 + 598564235603791923405209220943553276340069652593768332933092040972908) * 10 ^ 70 + 1596521183931632012919090908162922909239229401342852103032882798983645
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_103 :
Polynomial.coeff recurrence4Scalar0Left 103 = -(((340917400671477545617271403 * 10 ^ 70 + 8593353681087517582061189721311779290944425498767416590613086997515026) * 10 ^ 70 + 7714246994602292194699376317526354530821032494894843646646995891073427) * 10 ^ 70 + 8075334712044828536457677029234581816644916420245856260887320306739351)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_104 :
Polynomial.coeff recurrence4Scalar0Left 104 = ((4117045549774448030510618911 * 10 ^ 70 + 7170354777767147546061934995531610200566770009507179873086075178582129) * 10 ^ 70 + 83906326977056943312703687405074499677945935225953354465085203842150) * 10 ^ 70 + 9625520314293110338377612435975834409654905044184119401670321809478760
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_105 :
Polynomial.coeff recurrence4Scalar0Left 105 = -(((48203509783147252418676414157 * 10 ^ 70 + 534892902855907650544977936180782703219759776944987939099428271225918) * 10 ^ 70 + 3917664785390734959154554641258268767992735943367014406484759103987759) * 10 ^ 70 + 1173268609024903780069879229984067329253859957412698469092309862760105)