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_160 :
Polynomial.coeff recurrence5Scalar0Left 160 = -(((((27 * 10 ^ 70 + 9256435916268325026954610241270203753886163035040538749389599116474827) * 10 ^ 70 + 1845419209106087940898485429242099876143812612786805423008108095731971) * 10 ^ 70 + 5380696373798182458869158526652441938863133843228354463805587484166011) * 10 ^ 70 + 3569897821322798052052168836179075141345880022413563097399580772046495) * 10 ^ 70 + 3266097820019181535665297596971482368120965396653309488972048400477396)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_161 :
Polynomial.coeff recurrence5Scalar0Left 161 = ((((65 * 10 ^ 70 + 8490817678370662643417203187444564208094283366116792070329935442309850) * 10 ^ 70 + 7798400350936647485454845954972764280418990428184516312329805670434225) * 10 ^ 70 + 3710996802142794683967934434213357444330985583773933844726909095828789) * 10 ^ 70 + 2784666452875144939561377555995329727913445923260376342265068284142538) * 10 ^ 70 + 715812066279385078184312102928780191312619160849292216099621000822557
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_162 :
Polynomial.coeff recurrence5Scalar0Left 162 = -(((((152 * 10 ^ 70 + 4770207273233064187272034457586360690376616677501080716695025035379058) * 10 ^ 70 + 4914541086494091301823915470577313079152712624525430357152866562068203) * 10 ^ 70 + 8053288551556692727367582632195268622429661815348698290954889473443384) * 10 ^ 70 + 276837774302493453009619809096618169613906926572101840291482537596046) * 10 ^ 70 + 301428175746053708504758508088672015406511636755285929173065997292539)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_163 :
Polynomial.coeff recurrence5Scalar0Left 163 = ((((346 * 10 ^ 70 + 7354136558329893995527433655735490150579331424060673364000860956994157) * 10 ^ 70 + 707514779433823047736742871403397668717526856751485379458674601867852) * 10 ^ 70 + 6250328896162307242247976432835079233615084428542065157179496327772600) * 10 ^ 70 + 4589056892852403831662996755310264968161270503481367866001862395547133) * 10 ^ 70 + 8811287247263532415020828100770173414583911684628494148147108688757435
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_164 :
Polynomial.coeff recurrence5Scalar0Left 164 = -(((((774 * 10 ^ 70 + 3928954218092254312113348938869821191286391753653798191329370134730820) * 10 ^ 70 + 3685224309817745115421822957223550848584310506720634832961924979529357) * 10 ^ 70 + 3968430626201080927085360067346867181531308525885209708819223047233129) * 10 ^ 70 + 2312140025564333551535917144933374556891091012269477450247467330395629) * 10 ^ 70 + 6444350379306668905478767428484009264192906946034619616441524190099930)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_165 :
Polynomial.coeff recurrence5Scalar0Left 165 = ((((1698 * 10 ^ 70 + 7261372893079743907971718210177275607212950488056503315514750890125050) * 10 ^ 70 + 3176665934926720896485394438984655970732039178087040597278637056596066) * 10 ^ 70 + 5197290868524675740602366334262361137055301171892359178968723734651217) * 10 ^ 70 + 5587102350844988662261875093721171884683693605000871897081122868498228) * 10 ^ 70 + 3493495727191772458233475477460642878841364490433429689164152397013949
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_166 :
Polynomial.coeff recurrence5Scalar0Left 166 = -(((((3660 * 10 ^ 70 + 2690300317606695437730613670216013983820866816937566218462364779373194) * 10 ^ 70 + 4397066609470289638931283458998550424371045659066191261382227101005027) * 10 ^ 70 + 9058407355053782817648158677528275707012392627574649175605751622137888) * 10 ^ 70 + 3669755918465064042287417874965189414209817981181721694755529353775125) * 10 ^ 70 + 6912694342796961411268258137294370754045265296207952696083596893089723)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_167 :
Polynomial.coeff recurrence5Scalar0Left 167 = ((((7747 * 10 ^ 70 + 4425146849532979067289960313888518325930751531173384244888807447801166) * 10 ^ 70 + 6844141068063468325106130858206755852327457010689555042941784109974486) * 10 ^ 70 + 6433777158765710448464620283793478462110986486164180258103422133002739) * 10 ^ 70 + 3434393808548672119637644778899302093561663681025314336353037170456117) * 10 ^ 70 + 8112198805943302396368570274535711386290631927313356815224551427655354
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_168 :
Polynomial.coeff recurrence5Scalar0Left 168 = -(((((16109 * 10 ^ 70 + 6777488662066189704868120638941662263085974397516971711841650865551856) * 10 ^ 70 + 8744858065403361106481909553700444859690097399655510929924909055606621) * 10 ^ 70 + 7712849748749162316070856518565839595458032399186377262707560889701565) * 10 ^ 70 + 4771817253718545293851160794595049030240092730070596566305571466374339) * 10 ^ 70 + 3753314877873941546111863009756693364487020189145831588754849847991044)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_169 :
Polynomial.coeff recurrence5Scalar0Left 169 = ((((32909 * 10 ^ 70 + 8004310717195773344790540301567203716863457488838691782429349153295561) * 10 ^ 70 + 7008674109154545791470982367301084034710351054047673282060791950924411) * 10 ^ 70 + 1374151149142687787430446781008128693849170113521806238202038244983224) * 10 ^ 70 + 6824167894728882203681334187105545328870467828458652726464200377015521) * 10 ^ 70 + 2159416706585755605626327679889802172391231649324859360673276522562768
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_170 :
Polynomial.coeff recurrence5Scalar0Left 170 = -(((((66054 * 10 ^ 70 + 866369315393936785820362270928280109369136629530801652574781143566819) * 10 ^ 70 + 6463676147737899792735971225885973114083701682283031384115758074494904) * 10 ^ 70 + 4299939642409958100619250279672760939723715096383044800440426122722857) * 10 ^ 70 + 3313084291749585424542250888435226461456611597375154161134079042338777) * 10 ^ 70 + 357002559849664909672575395948986233294292662958545750227681576791558)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_171 :
Polynomial.coeff recurrence5Scalar0Left 171 = ((((130267 * 10 ^ 70 + 3918623904223718268473119441761040404756203633416485926767565173261116) * 10 ^ 70 + 469603628588695436666231736289197544345915153126349536268754271969271) * 10 ^ 70 + 3048153027004725640312556139739317646699913762385882047577210531973042) * 10 ^ 70 + 3368072530362391922364279926875926893071222121746236805334573839759035) * 10 ^ 70 + 3991516144233830512221174712589916385185051741181733749582128080737
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_172 :
Polynomial.coeff recurrence5Scalar0Left 172 = -(((((252440 * 10 ^ 70 + 617190749988244457925319682904571375628435399204041499800532255755239) * 10 ^ 70 + 3555998537709668142053372749336066084711220506112289918890487256623003) * 10 ^ 70 + 2490969571554695177458381196846806363632775384315776520543530269145630) * 10 ^ 70 + 3283556982152572352954431801357861053646537336693044397181937046598500) * 10 ^ 70 + 2231111498413956782565414342566633707912737815333758078257173857124650)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_173 :
Polynomial.coeff recurrence5Scalar0Left 173 = ((((480719 * 10 ^ 70 + 5179297815013599443009183523949866479340342341966440087041525394033158) * 10 ^ 70 + 9580659348200011361154548718791744422513761887601746470890161893080762) * 10 ^ 70 + 5464720612779443958848233201024059594211998131422940811086461696560337) * 10 ^ 70 + 9681978848874356073422359996771938550936470344136007230302390284162519) * 10 ^ 70 + 4847741181478975216895939600792552689357484160883549115033838263367561
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_174 :
Polynomial.coeff recurrence5Scalar0Left 174 = -(((((899621 * 10 ^ 70 + 8427393574221280612015030270551023722412673688184437879169732902325212) * 10 ^ 70 + 6738596435167988105521750864185533976903000722477048096723870941896918) * 10 ^ 70 + 5678876059292963553690559167372929428469303360698482986560123880902813) * 10 ^ 70 + 5568100451598876168972450398854889321392186215710709491657301360579769) * 10 ^ 70 + 7720650877038362553272745392066437546124118133834757544135286873623357)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_175 :
Polynomial.coeff recurrence5Scalar0Left 175 = ((((1654574 * 10 ^ 70 + 4034236243002969264740098846496215649839397782925660147640263699015419) * 10 ^ 70 + 8482606446149053848468874350272586206918322605497378654799706423858855) * 10 ^ 70 + 6225210083553576229243774072477689719323229495802399386631835850917355) * 10 ^ 70 + 3525785227680842782419324166914220221716795271584847065821320307877586) * 10 ^ 70 + 6845501258738557346317510067566890567126461589022069187051902686277749
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_176 :
Polynomial.coeff recurrence5Scalar0Left 176 = -(((((2990842 * 10 ^ 70 + 1787648586444358885895025883569391208316405382386703853168079889314192) * 10 ^ 70 + 8372999916837632456174349095676738950693759951984027827196153460776207) * 10 ^ 70 + 5611203377499678964280411994443187696594730564636878223558929720555162) * 10 ^ 70 + 236846859455439541901080295743942433097483444593095227342730979245179) * 10 ^ 70 + 2914426812679628299457445929570063665437541439842648381183673697488642)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_177 :
Polynomial.coeff recurrence5Scalar0Left 177 = ((((5313784 * 10 ^ 70 + 1005486223396617024223966003340571588227105217192461628147207572371858) * 10 ^ 70 + 3274005258938827140300460260484529820224962722553149401279951758889307) * 10 ^ 70 + 7230714875615731868756200872237192702301536335162906486233220557778433) * 10 ^ 70 + 5248227219067326373761517128047333762641242098707645104623148505925314) * 10 ^ 70 + 202531584763720249348465813107074430564232384610512031972679288789081
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_178 :
Polynomial.coeff recurrence5Scalar0Left 178 = -(((((9279816 * 10 ^ 70 + 5367273282859114188132010892208780763772179411840571409004933630707380) * 10 ^ 70 + 1450778628284480502875037781324338030651965271016837317454604472593686) * 10 ^ 70 + 8285473437478189550386862169795474717758104132281635528531433151238720) * 10 ^ 70 + 637314649912346149903041754350187427173637914680321635168179566597768) * 10 ^ 70 + 3782058923841292760783913325241237214380818811491328211014300623013628)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_179 :
Polynomial.coeff recurrence5Scalar0Left 179 = ((((15930205 * 10 ^ 70 + 2984257867871301820793593658396239656430527982437009393264604319039826) * 10 ^ 70 + 7149587438903504719050419665934204030393162396230325822962839685028476) * 10 ^ 70 + 2878647458694002761784339765646845591620036480654522764874302034854761) * 10 ^ 70 + 6441683920126464247428298872715156339219347674165199451129629729284567) * 10 ^ 70 + 3902611626880887849997543923402950561516131932192392023946745680307641
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_180 :
Polynomial.coeff recurrence5Scalar0Left 180 = -(((((26882573 * 10 ^ 70 + 9670580273823311560901179990713778381082503640325554743320575647333473) * 10 ^ 70 + 9666927830093796162379708366639423055552819591627883858781046424786557) * 10 ^ 70 + 1835400957326443224632060998755084498391460097998489308210028250979949) * 10 ^ 70 + 4256720233239946715678226271171275455202817348923652876467238944994567) * 10 ^ 70 + 6157451355626679300406710333581980938544738611600873968824225871874315)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_181 :
Polynomial.coeff recurrence5Scalar0Left 181 = ((((44597284 * 10 ^ 70 + 3083696381827960814972713699167991983999063718204691655175289732572611) * 10 ^ 70 + 5521150250075069914749726635805384964914292143452545503403265487305778) * 10 ^ 70 + 7953157290094967949330608232611435879249046074821722297860542494813610) * 10 ^ 70 + 4589975177710090931103728215456813926862589789725606876125255467666580) * 10 ^ 70 + 8249293554895570490115484142671571460400579242242662499953914701709298
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_182 :
Polynomial.coeff recurrence5Scalar0Left 182 = -(((((72736814 * 10 ^ 70 + 2228294059312424613333299689158206394147113593987818995930849816964295) * 10 ^ 70 + 5275382086910615100308945486902056960839175823772272827667459394410165) * 10 ^ 70 + 8999926388628190222419620611426751903440655859723200381000076182932515) * 10 ^ 70 + 8362378384922741139085774780841808434719561352140426143034035847759555) * 10 ^ 70 + 8395245709990871678712720552687432376472161153621690730409567739706172)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_183 :
Polynomial.coeff recurrence5Scalar0Left 183 = ((((116634835 * 10 ^ 70 + 5159197844713549335739630892176852719872815770973450845075551596531431) * 10 ^ 70 + 7466013624124064636582057434356580756899199071546743311765786887612826) * 10 ^ 70 + 7465672413790008278182652629361257648119413903844366475123973894355215) * 10 ^ 70 + 2967179951217905268785278883743489964228761658265176486684227355312763) * 10 ^ 70 + 9216516652038889092138030779130376534912933188365733507431735398865640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_184 :
Polynomial.coeff recurrence5Scalar0Left 184 = -(((((183886536 * 10 ^ 70 + 3811502761022160030586517922612550794501018897290174867520036508192940) * 10 ^ 70 + 2714048561699748387984830718960521779324080999152804186030683558657184) * 10 ^ 70 + 531092499198669146412337074514609793284348082528117153830950542766704) * 10 ^ 70 + 4709779276096005436481421209228421301309697905870511920097708195978563) * 10 ^ 70 + 7753851413810241040058957901159564069433918401924088312097042953663898)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_185 :
Polynomial.coeff recurrence5Scalar0Left 185 = ((((285061395 * 10 ^ 70 + 6098211343282854776518734756326593205007767469402838912981045060659778) * 10 ^ 70 + 8690504633252921700138919033587377172988132470120962963460468384271516) * 10 ^ 70 + 7110469221726160603748309937134922412121863703362018940298673933242528) * 10 ^ 70 + 7702794347403856640270733169086409632803376672645165290672029135143835) * 10 ^ 70 + 3638520102052682737000119051855084518553571984035105383531599979172341
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_186 :
Polynomial.coeff recurrence5Scalar0Left 186 = -(((((434522806 * 10 ^ 70 + 422012257484097590196308854969507295294135575039923076957069958814326) * 10 ^ 70 + 2475682464839892131846898636060287725432464489863580341764288126702781) * 10 ^ 70 + 485705179412700038855789425907515269843210045725768680385255194099835) * 10 ^ 70 + 5096244412169192372603911439472878320220059418825719227974875914677364) * 10 ^ 70 + 5734953120045282207579392161379110326874543772294900281145342331618249)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_187 :
Polynomial.coeff recurrence5Scalar0Left 187 = ((((651314911 * 10 ^ 70 + 5233021695010597907988655825685342021401392412840980401648702630141931) * 10 ^ 70 + 3304800794797407296950138323194877134760603834988179779428484305199166) * 10 ^ 70 + 3219056983846057287509951030538494898857026149198958643891855392359188) * 10 ^ 70 + 3838276400814863734711083106667222268348954253034813951978362939725092) * 10 ^ 70 + 4292022468896979158168158445892195478580030029121887143701381382243481
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_188 :
Polynomial.coeff recurrence5Scalar0Left 188 = -(((((960046033 * 10 ^ 70 + 4545341549125048649079983152259549078486235748867139123241556029669216) * 10 ^ 70 + 7156773533765847686881434025774425017884160576595923259027234591120914) * 10 ^ 70 + 444455676938734362451828937980773606384851066219065315606622652594867) * 10 ^ 70 + 3085701385026185108245011518632554710575495182859428817507988921582526) * 10 ^ 70 + 1347332974521178827680752709260126823257681003305099901613452834728873)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_189 :
Polynomial.coeff recurrence5Scalar0Left 189 = ((((1391661921 * 10 ^ 70 + 3235437154225544789841082002227960091572655401121305903309955026686225) * 10 ^ 70 + 1240368322485932509531565795059515360334287542915251389403221314325950) * 10 ^ 70 + 8345193952951454981471230023185247020716155276313685233247477941175381) * 10 ^ 70 + 8905359652941488669826849697875224943783267026378503758939164338256677) * 10 ^ 70 + 2671885089527928178499261632656131035591892804050712239093354542383312
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_190 :
Polynomial.coeff recurrence5Scalar0Left 190 = -(((((1983964526 * 10 ^ 70 + 1990300726232092435656087586299330169249292620524289803920868146614246) * 10 ^ 70 + 3189287281556871190497650095102466359103437914818977740566498210810161) * 10 ^ 70 + 1568802519367056009801350661691066956922880517309601060835310264374092) * 10 ^ 70 + 3393570175681482737393213265756249253041761989842589864380314610936890) * 10 ^ 70 + 1146902902882062784931859535457909451733954300607709806641680911450948)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_191 :
Polynomial.coeff recurrence5Scalar0Left 191 = ((((2781698971 * 10 ^ 70 + 8504613170442549155257005170040626927003567624504169259570127813664605) * 10 ^ 70 + 2377019387060822115892784237004243003306144304335576893459443617519405) * 10 ^ 70 + 7639207144545495719280381581726717883742389755358320506572682892322946) * 10 ^ 70 + 8640874708278915683250506366362826477389899778315727555432115066669792) * 10 ^ 70 + 4731273907585240900630499853377825964263319867315535552140452803785668
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_192 :
Polynomial.coeff recurrence5Scalar0Left 192 = -(((((3836010713 * 10 ^ 70 + 9857179727563449193655529133576778163663719052193921931955992193432341) * 10 ^ 70 + 1347673959907462511776445273514891287989729388980100187194635267350908) * 10 ^ 70 + 7138608871134655545399215046792680041878120015907440195307741869189081) * 10 ^ 70 + 5553444956286684073178676820695302376210659252369746001516194808367592) * 10 ^ 70 + 8750695628691432041180852180139664602528934715538458479732553315019546)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_193 :
Polynomial.coeff recurrence5Scalar0Left 193 = ((((5203075520 * 10 ^ 70 + 3229869158114676316499570700399155553112000490092499903740428032854879) * 10 ^ 70 + 355024855286209730591421416579227168170946808069165763259784980493438) * 10 ^ 70 + 6669579423766704431738733966552780940871004109876594433194819642776144) * 10 ^ 70 + 8602136445976627855641928678331027786914530860878955988495492041043302) * 10 ^ 70 + 2273057808053731655019298893490606017622157774329868839300012669255840