Recurrence 2 lookup certificate: Scalar4Left coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_230 :
Polynomial.coeff recurrence2Scalar4Left 230 = -(((1 * 10 ^ 70 + 5594347229877197257086507692968598506553776305862268785957140223454106) * 10 ^ 70 + 7774523051578560480720397293980841510090216224589135833353273368221448) * 10 ^ 70 + 1191964212727635727402651924819291704238257366185574712878594658564173)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_232 :
Polynomial.coeff recurrence2Scalar4Left 232 = -(((2 * 10 ^ 70 + 317211993591922712811417105274417477507127688164130436429282767663905) * 10 ^ 70 + 7966448932372170901128686161379733966582583827415790629805689551558794) * 10 ^ 70 + 7532642903542777722791045844361223363897427535333166644740318224600806)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_233 :
Polynomial.coeff recurrence2Scalar4Left 233 = ((2 * 10 ^ 70 + 1359579737504193383254207127070912939515019742495053731176064739234155) * 10 ^ 70 + 1947055081973801633940222451658633470219446813422203458111636775398333) * 10 ^ 70 + 1839997614403483590897022318114578172461153078512085555674522467870048
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_234 :
Polynomial.coeff recurrence2Scalar4Left 234 = -(((2 * 10 ^ 70 + 1253848248699937782283514995909881626602540938585641467908051642513549) * 10 ^ 70 + 6067424814617787722616475385697667997987284143112718044450017646569340) * 10 ^ 70 + 8098733882409361504817907583883802466853089144029318256004484060872515)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_235 :
Polynomial.coeff recurrence2Scalar4Left 235 = ((1 * 10 ^ 70 + 9964473394137407189114743581387285965543491179815015605655722756190416) * 10 ^ 70 + 8553408133225839148119488736113393459542046824225744058718090599483515) * 10 ^ 70 + 2413766806388702061342952881625845897647570287185550504480466451031099
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_236 :
Polynomial.coeff recurrence2Scalar4Left 236 = -(((1 * 10 ^ 70 + 7606279168654311582291828146538166663526087260105734799890956236820151) * 10 ^ 70 + 1389381526420697009641571987596891629125604451171583566210152980423072) * 10 ^ 70 + 4864328556878270074878863034678915160195736193055851746318326085389387)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_237 :
Polynomial.coeff recurrence2Scalar4Left 237 = ((1 * 10 ^ 70 + 4427071782126127381390054331182186952866976075789027456662982136670249) * 10 ^ 70 + 4400093840050997038910212722249475464326138356934161189514974914728428) * 10 ^ 70 + 7081325055635604730379553290745571628375090955709028342452671742648168
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_238 :
Polynomial.coeff recurrence2Scalar4Left 238 = -(((1 * 10 ^ 70 + 766122872247943855935909321277396441763348264610466859383676522497970) * 10 ^ 70 + 2973827957373619251421056892951908291391615870812874382282873018765173) * 10 ^ 70 + 1382895554771672026806086886287491012428231651885665521691685649246450)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_239 :
Polynomial.coeff recurrence2Scalar4Left 239 = (6997864591022792473285803080822857310581521207474370185794292963761414 * 10 ^ 70 + 2147031880240401209814997660820355330118879805203646253801623153920703) * 10 ^ 70 + 9128080614282351547895352798709041719284578841317638517312554278128423
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_240 :
Polynomial.coeff recurrence2Scalar4Left 240 = -((3473145572099871807963506170813923718257489591283779993487395355990816 * 10 ^ 70 + 9940365887698508948446204295231510364342714593267990733514317259321083) * 10 ^ 70 + 5955945581036766191612232066093123798277274572146984523525895680343386)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_241 :
Polynomial.coeff recurrence2Scalar4Left 241 = (470091032737798577562599647908080215584498172841326735499818835754806 * 10 ^ 70 + 3938971833757502143097342291101076713649679397061742414668656821888483) * 10 ^ 70 + 8672228853964394348670467758431234022362576949564697707733928182425511
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_242 :
Polynomial.coeff recurrence2Scalar4Left 242 = (1836681327906337359207043214695441573750617174961129555520097937847008 * 10 ^ 70 + 8097862684290745543237902637436007318197739823344006290728924815884362) * 10 ^ 70 + 2594403490749687800598211803372392588812281577236256506870367918226709
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_243 :
Polynomial.coeff recurrence2Scalar4Left 243 = -((3384835004265971471028422877554994166094906465146696876345035734637060 * 10 ^ 70 + 3636204738574551245982537663823533300035145328535899447280272195770361) * 10 ^ 70 + 8004553790997595019212560898658987058211192327409468750022195842852118)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_244 :
Polynomial.coeff recurrence2Scalar4Left 244 = (4212747760304200674175023028126776985469458276218615812579341160503897 * 10 ^ 70 + 2445969431243879753495059405640031819937914478444974704228366944832965) * 10 ^ 70 + 1915008748327976629823963461636098175577980501662383259111918082967975
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_245 :
Polynomial.coeff recurrence2Scalar4Left 245 = -((4433388853574410845350961220429961642850760721525700370062376754830907 * 10 ^ 70 + 1982543942809163634838311259258641836743972141841706536129368462385244) * 10 ^ 70 + 8052192506054734880772226653439707742667399357276068672784107200785594)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_246 :
Polynomial.coeff recurrence2Scalar4Left 246 = (4201455482941165693174749500311970302339401971279783053514781830274387 * 10 ^ 70 + 1575607645987142109638099135520381322320915593187727167031671959887397) * 10 ^ 70 + 7208740995142980621590212404526944440094014728948781667469245400662422
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_247 :
Polynomial.coeff recurrence2Scalar4Left 247 = -((3681389671631285791330495803014978166800430145539137981978697186035135 * 10 ^ 70 + 6702992098472508191202792157744528369738774264247474474334748392570313) * 10 ^ 70 + 7322640487892079038883312819390746446858707576552517973831619660337647)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_248 :
Polynomial.coeff recurrence2Scalar4Left 248 = (3021981713568628097072028233528259732562861700045693798267536749485669 * 10 ^ 70 + 8042108323970126342496550406627927002048975825616682675606558771395422) * 10 ^ 70 + 9694425272910172133742818275779644673060896360586497010216565224498398
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_249 :
Polynomial.coeff recurrence2Scalar4Left 249 = -((2340496545462305801778116711310749227027802549608265992106732892319384 * 10 ^ 70 + 9771486057009172379186140127398949956081617040736604384651405679579436) * 10 ^ 70 + 8079238181852162983181137568476310513323851550197600358507184111402170)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_250 :
Polynomial.coeff recurrence2Scalar4Left 250 = (1716531139504386515119241089084080763223034102171467965969438218428157 * 10 ^ 70 + 2002065575593746251229179617148274270243780484045214321432760285655080) * 10 ^ 70 + 678693610431333252554302580109440002114139543147596344546683341097941
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_251 :
Polynomial.coeff recurrence2Scalar4Left 251 = -((1193784013900056147498534449581351188730442479989296393912693831605701 * 10 ^ 70 + 2271187823769313925559380429985928641806529429813836763608895087035894) * 10 ^ 70 + 5280654693095710232242393414553166733436589255273859495241876695508044)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_252 :
Polynomial.coeff recurrence2Scalar4Left 252 = (786888353788567171361233134505621162559500804116426819434767694727159 * 10 ^ 70 + 3976553803184647580931399143627127424036405037180992961684199477725033) * 10 ^ 70 + 9196485277100674907612403842767672678036099332391060769731959727982945
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_253 :
Polynomial.coeff recurrence2Scalar4Left 253 = -((490377604371130330619709428265192466939333120753194786444632511319356 * 10 ^ 70 + 6001291575451818531864878259245542265902310942255248298413420934659632) * 10 ^ 70 + 9914640623962455172944890365531623801325725256961655077600258704290728)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_254 :
Polynomial.coeff recurrence2Scalar4Left 254 = (287436104631812548001224475622828814922690176955164946004415172080685 * 10 ^ 70 + 8148187093782819078459294929132360225753226519167217312351440608430315) * 10 ^ 70 + 7668946324885521082685656558290072914243204375227191534152961824185312
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_255 :
Polynomial.coeff recurrence2Scalar4Left 255 = -((156976193741597635403604673081333346694652842189901387991455958392555 * 10 ^ 70 + 3852888478779783895078105555299753027717232993506708518072970450669752) * 10 ^ 70 + 3369633935966979192346322235894290477200620764465724575585930039524673)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_256 :
Polynomial.coeff recurrence2Scalar4Left 256 = (78461220457999471074700057565506844965226856741561590739349305933098 * 10 ^ 70 + 6324299918661523238079365343681594573468356028942644208918655970026303) * 10 ^ 70 + 6800581169962996594450109718213908635463439732201170347552737274348567
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_257 :
Polynomial.coeff recurrence2Scalar4Left 257 = -((34560551354461620139617070470513414541473761101605074776547801963726 * 10 ^ 70 + 8558454236114920000822238421573965710837176609277458187451773165019471) * 10 ^ 70 + 8588475046879860109018384338429872547619661346184788455974984553358059)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_258 :
Polynomial.coeff recurrence2Scalar4Left 258 = (12105346670961816037596344364282612681342402068220608705328435746358 * 10 ^ 70 + 86182416394763177290908983461276717470486503573401741216643053230797) * 10 ^ 70 + 5256927006936063337108998680960290630815217670966751931289734183245711
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_259 :
Polynomial.coeff recurrence2Scalar4Left 259 = -((1938816571088313532989750865063844766442621455564124551209139581605 * 10 ^ 70 + 4611573085190686196989266427966610737263637331508900272454989978544789) * 10 ^ 70 + 5411791609619726922174865795772546082479332379193896046085366940229361)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_260 :
Polynomial.coeff recurrence2Scalar4Left 260 = -((1798873611116863965471899991791546395496383207911626543714353251345 * 10 ^ 70 + 956358209486618385386358001452358780854645671354094908760842884454152) * 10 ^ 70 + 6459831284710126850468841192033574855758430811537182392463536080832943)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_261 :
Polynomial.coeff recurrence2Scalar4Left 261 = (2553281565533535537780282300453986003651099107799557808162417077232 * 10 ^ 70 + 2601427630504700734826598300921684668169625808168754131724143381763122) * 10 ^ 70 + 3737188737615316246386166715524774754217421732335957801616247280110976
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_262 :
Polynomial.coeff recurrence2Scalar4Left 262 = -((2167302664756539289950677612566626641814261584941662373721089375555 * 10 ^ 70 + 1940937030071756964615286770446326277252182959383485228098994817584532) * 10 ^ 70 + 7045174986213077441310850613387600341728428428068201826941550124360274)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_263 :
Polynomial.coeff recurrence2Scalar4Left 263 = (1515344050296534391982452189460280461418983310003854441060899583746 * 10 ^ 70 + 3084665062572725303100366347805604561413013782867575713436145195456551) * 10 ^ 70 + 6491115371176800070437551908385364256185408635961648493821410255855888
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_264 :
Polynomial.coeff recurrence2Scalar4Left 264 = -((942372362649464271823275130257863669258410852188050350816577316477 * 10 ^ 70 + 4570112848300965055272414345131762890666373030170546561876795007073728) * 10 ^ 70 + 619709087493704370110094708024520074836400351471798288674691250969526)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_265 :
Polynomial.coeff recurrence2Scalar4Left 265 = (537073102113157396014688895283306360411534323433850211679919062339 * 10 ^ 70 + 468861228009169370561530707983217018840179430349954912971950487513111) * 10 ^ 70 + 4169818629864002282650144188025180158898173817565732054448073743353516
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_266 :
Polynomial.coeff recurrence2Scalar4Left 266 = -((284424307330580038453964801348303707002994624033683040886819335503 * 10 ^ 70 + 9868927326959048163302356316266773383288628861615735313315777832588603) * 10 ^ 70 + 6341298950552061068037736784031094093149746885291973864102773449469381)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_267 :
Polynomial.coeff recurrence2Scalar4Left 267 = (140879711565414060001612384706728835868241964233185545822927802832 * 10 ^ 70 + 5774504450392870505358911664820139937653057642945634840033680099520200) * 10 ^ 70 + 1471104635817953877892198621063690282166363860940342793969635569793346
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_268 :
Polynomial.coeff recurrence2Scalar4Left 268 = -((65406352064701771735609339796078760690419149300310597634932134482 * 10 ^ 70 + 5117989971389398795953032883275726161644530091039089231864412340325765) * 10 ^ 70 + 4364062343318427316414864650280602201254424378408415655043766412653602)