Recurrence 5 lookup certificate: Scalar0Left coefficient convolution #
This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_282 :
Polynomial.coeff recurrence5Scalar0Left 282 = -((((1892157534458732982475818973931960779516488923591476816118673928530939 * 10 ^ 70 + 6980848982681867776162421408192051415556122628058210005708178401090208) * 10 ^ 70 + 6802182170638635849186996879510716975057631366808424704281612555507574) * 10 ^ 70 + 9746450024828373767049279510197387214715801922958543661847489247495689) * 10 ^ 70 + 7191143817123252842069615083399568352736461189948608521313907725937362)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_283 :
Polynomial.coeff recurrence5Scalar0Left 283 = (((817931248770373204683822588869244943221751524107711202659955563260482 * 10 ^ 70 + 3840547491188289559302999413945974484655537005235043496641613959019313) * 10 ^ 70 + 956760427344299886098241940830730595711960120446504944105173358105408) * 10 ^ 70 + 8122670526651949016072680198809332398905043318493440797184012067566064) * 10 ^ 70 + 1028078160053472784047925076682556864092530083444622989142619796647232
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_284 :
Polynomial.coeff recurrence5Scalar0Left 284 = -((((325471689944215270414781256028833856992032969011623530998836850495279 * 10 ^ 70 + 749441264247665035259151904670647839532759493287992374900158511661020) * 10 ^ 70 + 6487735413304923154229582828359243284166059824499877257692195215512711) * 10 ^ 70 + 1621611925210601093180243147452777466991614855743233828768862349157965) * 10 ^ 70 + 6767635995967415785786027436213687647472212034147516244982647671281610)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_285 :
Polynomial.coeff recurrence5Scalar0Left 285 = (((118278745403984360486228899365400275505316815631332497096621383195945 * 10 ^ 70 + 7860312064093565007780328605653396219381472012668482892106609170046245) * 10 ^ 70 + 1528210574468730758650023109456937962023718408456798637663096315396555) * 10 ^ 70 + 2970114321685595865941457298242052142475650239809883856529911374460811) * 10 ^ 70 + 9090048303718968506423985640634872932468489463451526038354050040783841
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_286 :
Polynomial.coeff recurrence5Scalar0Left 286 = -((((40180930082638558824893655110298042434288974950789659292346398441325 * 10 ^ 70 + 3276016360875365411554831658593143456436617043207432257248843620902737) * 10 ^ 70 + 5747496410312780156531819867800755342745201920901140199381766180971778) * 10 ^ 70 + 8432351049443697829091580632513840366565949676331070690610061543632704) * 10 ^ 70 + 2836539918412354963153798005842630209353540122395521969368904483679007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_287 :
Polynomial.coeff recurrence5Scalar0Left 287 = (((14860251006301894478299829471357721267443872896173680005978521219505 * 10 ^ 70 + 6302055463378261608604932002275709776481152146807270647726505032393697) * 10 ^ 70 + 9965997825829432939428614149003865532408221570691014256513856864355682) * 10 ^ 70 + 7839083915250967973054342869703019976022426798747662398401475731020607) * 10 ^ 70 + 4531007689231703462063013690986675596765451098027450786699405007872229
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_288 :
Polynomial.coeff recurrence5Scalar0Left 288 = -((((8215046485848266910864321825101427430497922361712501644367810125240 * 10 ^ 70 + 3997414350347271651388793700743686803704682308013897259895155405810202) * 10 ^ 70 + 1294089284942141304788875174102461889934867618232392076084855789436247) * 10 ^ 70 + 6288509404204246811024868167400063443086123462369143055586310593543298) * 10 ^ 70 + 2356000080362291515236113318182961245470025518721170084730663213502425)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_289 :
Polynomial.coeff recurrence5Scalar0Left 289 = (((6717636352184986250772835701380504753702882237041596141778937321169 * 10 ^ 70 + 8399658710949507877203966248674748050196577048714007604020881878229946) * 10 ^ 70 + 444650313742820118223730501747243071910945505514632178087420944717520) * 10 ^ 70 + 9573431120926361028518068515872401776036128028666983203802764464364087) * 10 ^ 70 + 1219416641061909040897310728968522322003636928304076782578834995526676
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_290 :
Polynomial.coeff recurrence5Scalar0Left 290 = -((((5921112849299857353101881392760384788825246322803152254439455127959 * 10 ^ 70 + 1752679122205593913118913688288350150945558600895796469852031176255229) * 10 ^ 70 + 6598118928472724740968495138920232005118355465868078442045155384427962) * 10 ^ 70 + 8350213703622298765365759210645385973456130344045429920207779680314942) * 10 ^ 70 + 6045949415425534326766822670352577572527840145780326578605297475688563)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_291 :
Polynomial.coeff recurrence5Scalar0Left 291 = (((4869757762093114527334366764552989616874206470070043222542923116480 * 10 ^ 70 + 2217075305716280791701528928034026858918503467162434731854185920468735) * 10 ^ 70 + 5624321447323528032375987076021792464691180115534207451630622180823110) * 10 ^ 70 + 8951413920628387118603111061173719536713296441091230059003307486905935) * 10 ^ 70 + 886632793238131261409615423080526703328187743578393296035542165112806
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_292 :
Polynomial.coeff recurrence5Scalar0Left 292 = -((((3660950417136797782456355238891519697563937267266074188345148995693 * 10 ^ 70 + 8323380143470537050939068060423344123730951749318567880932473242997704) * 10 ^ 70 + 6746430114021603166082227213769554988673392199036257534686662749747495) * 10 ^ 70 + 9238811325588571260128856267015345330474983279932809609584200826188265) * 10 ^ 70 + 383518542099395227104887862467447668965522826007183749294079157848247)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_293 :
Polynomial.coeff recurrence5Scalar0Left 293 = (((2537532398636297395167548932158380729147816318269619584860336553624 * 10 ^ 70 + 9592381319152757911006878317737912810887461881473216678591422269241780) * 10 ^ 70 + 4079393758068618431788581635301182337220056301083122287414671975739896) * 10 ^ 70 + 5787189026479902178855256351394867993462302205952396588856611425863996) * 10 ^ 70 + 7245153196665178587215544335909952409417424859848465899263282216320298
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_294 :
Polynomial.coeff recurrence5Scalar0Left 294 = -((((1640242036427899904768865484680469328670921625461414945345620603263 * 10 ^ 70 + 2422894936774499144802770215324167285431935012496201117707726908014474) * 10 ^ 70 + 1883214594598359053686785790780901173250291882098851117149820558072231) * 10 ^ 70 + 5446868223827619628879610319262926057929029899514913361619921680013583) * 10 ^ 70 + 9883200700259043981437003092605119505596393336133394269052173789581531)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_295 :
Polynomial.coeff recurrence5Scalar0Left 295 = (((997929744970919459710014451842600553212480830438796766451635850229 * 10 ^ 70 + 8944723241544046694358563545321018740484838663406824270181124816027303) * 10 ^ 70 + 9550019770730221962978288013065703036850729287100907775199088457303685) * 10 ^ 70 + 3731370916432686530897209457511247835497858213730403528722502828914821) * 10 ^ 70 + 3408651770987541930979872941667751940875811868734807385704658956536119
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_296 :
Polynomial.coeff recurrence5Scalar0Left 296 = -((((575376153586576889425316099223039360111900031267371201694827378293 * 10 ^ 70 + 8240228642629763246526392782938202172068913782054349358735973167411272) * 10 ^ 70 + 6173882512560822464189549186036547954158424224227732253911686624928861) * 10 ^ 70 + 9472801634748307422842177320957735646566363315038357391578844190241413) * 10 ^ 70 + 3431478408539607345481083482691086766943059292413788118205475882776604)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_297 :
Polynomial.coeff recurrence5Scalar0Left 297 = (((315934772611205756294934653552582553562757463443827378733837514234 * 10 ^ 70 + 6411626871848374841449149466441626854641198920386453086662745878277254) * 10 ^ 70 + 7829495780668196359248529647231698652263661606159625571127822729924133) * 10 ^ 70 + 87756815839500655308059642974063747126493957343215644436835753228363) * 10 ^ 70 + 1281684494078754235787266204185976032963240206919496504214416341291884
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_298 :
Polynomial.coeff recurrence5Scalar0Left 298 = -((((165796818916898510212269817664861872994752555097837780074968989454 * 10 ^ 70 + 927385126521692511157051957565559044624551153707653614316003404872398) * 10 ^ 70 + 1433484307643704405032971682488739501650628631935600575118642776814590) * 10 ^ 70 + 29200475665748276702538378810615408055140534126916116516421802273191) * 10 ^ 70 + 1247785781164198300654483630254142840313300215504823643268230951180909)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_299 :
Polynomial.coeff recurrence5Scalar0Left 299 = (((83376137178272288699650232526030323497360250752742917366326150219 * 10 ^ 70 + 8397680736163653647407783643215270906241715185299654782247082465198579) * 10 ^ 70 + 3256004689716995618333049388104307620225984000302266141836343145006981) * 10 ^ 70 + 1469027031245630995844887656204577208375458104299609082158408965318022) * 10 ^ 70 + 6812894075231694097461954276923471225294032992685796567895089552175511
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_300 :
Polynomial.coeff recurrence5Scalar0Left 300 = -((((40268757034213267318446599749268741560652901504701992463127403572 * 10 ^ 70 + 3402480370363223485913213380450016156163144064850250921843188152030049) * 10 ^ 70 + 5139727937865087993818264493434498536928876215065961696066442425121974) * 10 ^ 70 + 1136688227856030674216253913007123867119471370222129093520700703555271) * 10 ^ 70 + 3418424450271009846365529667464030077640450284657610682900273012299495)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_301 :
Polynomial.coeff recurrence5Scalar0Left 301 = (((18724216617516428253236266020236239223188391201411930404874933117 * 10 ^ 70 + 5964973342893463036356964791164377267740687246703050688476900274846919) * 10 ^ 70 + 8541966328186315318021276818612943114462976548869935878568906683552328) * 10 ^ 70 + 3202215344930749894488271955440643546201886882010050373754575231802453) * 10 ^ 70 + 6005904607500346737208140275500661967563317921861611475693425138662990
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_302 :
Polynomial.coeff recurrence5Scalar0Left 302 = -((((8410886760660904068279510796437526983183616410136227173809841318 * 10 ^ 70 + 1343700023189549530358515755989085200541798848641004359277562565536918) * 10 ^ 70 + 411940511855848248543572045286565180288398448672214738232935330643756) * 10 ^ 70 + 7461412438370812318315766465557306997661576263895579265468314042662608) * 10 ^ 70 + 8117180382503888902329507526366217698955932167862228677884537408469235)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_303 :
Polynomial.coeff recurrence5Scalar0Left 303 = (((3671143590960913309875880466878569156179258894110125753758603685 * 10 ^ 70 + 423084131011028980491459235810093890781831442757895512915306550688503) * 10 ^ 70 + 2840626761301935087909642879872667234041809609260025185424107551561289) * 10 ^ 70 + 2597142144339838031595998570695923199397995060166731956220368906303064) * 10 ^ 70 + 9193122333767165405253690735311415352737143289659942175724196635588139
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_304 :
Polynomial.coeff recurrence5Scalar0Left 304 = -((((1572798341623594103198946790187366702624862624189548775720272086 * 10 ^ 70 + 9505881463945774453360331286381346270501447893000108633550448193270531) * 10 ^ 70 + 6646641776560085500458980712009600748421520328149428248151972005907127) * 10 ^ 70 + 6332228226432136087322798974274557741670073802565875677554129751581216) * 10 ^ 70 + 7079422672671950059629433799695714435664919875536303409852952867969084)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_305 :
Polynomial.coeff recurrence5Scalar0Left 305 = (((672459471048328478921700308853627022793400896660847615746643313 * 10 ^ 70 + 9597612307144331518444835607075334134450246484200583460701270923941980) * 10 ^ 70 + 2164504907479373520184161895110802992938350672211663685983326463844103) * 10 ^ 70 + 9579269627124312315675663355555205058748678150218713185660668799683854) * 10 ^ 70 + 1016967696097556695280925075207796350379068765254961376580229628596371
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_306 :
Polynomial.coeff recurrence5Scalar0Left 306 = -((((293789223423945766408982716220716045942181771665585798543026998 * 10 ^ 70 + 136408916069012103718124909978396907724126899673403483235279752811367) * 10 ^ 70 + 8296336499452417105561751505432620481652009960262987950291297618620405) * 10 ^ 70 + 6883299107668097140899967336590859385432011583830014707880427004165797) * 10 ^ 70 + 296232401616897125603826732525904743899474214504089136257457692175663)