Recurrence 2 lookup certificate: Scalar0Exceptional 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.recurrence2Scalar0Exceptional_coeff_343 :
Polynomial.coeff recurrence2Scalar0Exceptional 343 = -((549413 * 10 ^ 70 + 4208969948797911301739259730429578608203074531224559687994506903378498) * 10 ^ 70 + 8257188805099232609917347523120110939282475000829286819440859633607858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_344 :
Polynomial.coeff recurrence2Scalar0Exceptional 344 = -((90941 * 10 ^ 70 + 5777183123868540950676223565818539960756922180336654742990542795991679) * 10 ^ 70 + 1272887837969715847954175897815351405909140035299171293157493423831202)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_345 :
Polynomial.coeff recurrence2Scalar0Exceptional 345 = (2346 * 10 ^ 70 + 6825810543754798128616518108664855109053566746746817263362678452876984) * 10 ^ 70 + 234539901512427802073171640235604180438990955982738668952302180333348
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_346 :
Polynomial.coeff recurrence2Scalar0Exceptional 346 = (543 * 10 ^ 70 + 9109637531435348230577153529910979650469314456899864674873103167844002) * 10 ^ 70 + 3910600193657169473685353228707331062708668996573232812980381507632508
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_347 :
Polynomial.coeff recurrence2Scalar0Exceptional 347 = (3 * 10 ^ 70 + 7270408278438467808606726998804909682985659994388140929958733827812358) * 10 ^ 70 + 3595296610246089567044023676108100396175042581797861029007040036326940
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_348 :
Polynomial.coeff recurrence2Scalar0Exceptional 348 = -((2 * 10 ^ 70 + 2592241391137741242814317148735924069008138348360559685037707348044131) * 10 ^ 70 + 9977009243884770112838260461997115791662762472528176626677428985464553)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_349 :
Polynomial.coeff recurrence2Scalar0Exceptional 349 = -(1157088599351683624962019464616853459126295764411593341261893475392866 * 10 ^ 70 + 272521727614164856871897734033976310369376674757451530802934057438803)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_350 :
Polynomial.coeff recurrence2Scalar0Exceptional 350 = 17796650906286593788122542700685392866975629638690200442643053293683 * 10 ^ 70 + 4296920124640739458086874544157970165235986273072642642225303632794652
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_351 :
Polynomial.coeff recurrence2Scalar0Exceptional 351 = 4670342226708756094661907626585587108573725117995085690565167880828 * 10 ^ 70 + 3983162130489204305419709455564772308024650492559466146822216965166751
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_352 :
Polynomial.coeff recurrence2Scalar0Exceptional 352 = 272873304725445052465532015470246017083789212741952995677994257933 * 10 ^ 70 + 9604272185013280891469281668386630183930691230342161298215038924739718
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_353 :
Polynomial.coeff recurrence2Scalar0Exceptional 353 = 9682634654954712596323460453589730262992481207766192554796999605 * 10 ^ 70 + 9573071792177419273047501453896036946570289139661276553154444144560364
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_354 :
Polynomial.coeff recurrence2Scalar0Exceptional 354 = 242193094703442328234452646619800167830027830033067779391215090 * 10 ^ 70 + 4066961343714232260420337389119083708248160512804574769525156501144027
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_355 :
Polynomial.coeff recurrence2Scalar0Exceptional 355 = 4513059696585816764960836882259986314508236641723812335180326 * 10 ^ 70 + 6216989777864062243937950099119543990278151356881576241812869246434133
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_356 :
Polynomial.coeff recurrence2Scalar0Exceptional 356 = 64265634087812037244571230039600691344689939956302692174264 * 10 ^ 70 + 639396207094989616810014514296899015911502837759540061327247948348363
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_357 :
Polynomial.coeff recurrence2Scalar0Exceptional 357 = 707081563502274724266509038148889102239019294005415004422 * 10 ^ 70 + 1508832716198653299454793814761699858576019989915458992919190320131909
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_358 :
Polynomial.coeff recurrence2Scalar0Exceptional 358 = 6016899621150508185485649319881487375183128135836465375 * 10 ^ 70 + 1542069773624697940733085538521317759908452269069545865056053323252271
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_359 :
Polynomial.coeff recurrence2Scalar0Exceptional 359 = 39228482408365074320313530122688963572434974879802060 * 10 ^ 70 + 6381801648005063820126100778427641907243256899898098893810474365370706
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_360 :
Polynomial.coeff recurrence2Scalar0Exceptional 360 = 190991661669912501015403980803598605963230904605099 * 10 ^ 70 + 9778562298805122453337992489785117779863526962304642650912103607320779
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_361 :
Polynomial.coeff recurrence2Scalar0Exceptional 361 = 651904484369244253689398454667751245961478653487 * 10 ^ 70 + 7994438061121182500274386632569615416760595003904557718560082225630875
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_362 :
Polynomial.coeff recurrence2Scalar0Exceptional 362 = 1267232864668550440512112596812439852136011101 * 10 ^ 70 + 4360419453772119048843455192714663402029374093147250643616810915499101
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_363 :
Polynomial.coeff recurrence2Scalar0Exceptional 363 = -(438840974158198713372998382551243631526257 * 10 ^ 70 + 9983754302896018313846917084406976642569341025153952717365064197604899)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_364 :
Polynomial.coeff recurrence2Scalar0Exceptional 364 = -(11485223772645554165512257574953434321605 * 10 ^ 70 + 9460120949175752033555295916530207081399419889966057222671858155502751)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_365 :
Polynomial.coeff recurrence2Scalar0Exceptional 365 = -(34965931757333621569932799623725453907 * 10 ^ 70 + 7354650064210415382517824094785468314372924355951042916870183159394843)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_366 :
Polynomial.coeff recurrence2Scalar0Exceptional 366 = -(39482819738688786451946930281877259 * 10 ^ 70 + 6281907695502883176122757911805939469874311790089158614784250296175112)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_367 :
Polynomial.coeff recurrence2Scalar0Exceptional 367 = 50683767301952086300777225899647 * 10 ^ 70 + 6680586465989551781668240039039587116016335956883249542000809274443839
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_368 :
Polynomial.coeff recurrence2Scalar0Exceptional 368 = 245128064618118153857396289933 * 10 ^ 70 + 787857688893822694457910428833512070954004734588462906088190121425624
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_369 :
Polynomial.coeff recurrence2Scalar0Exceptional 369 = 333419100578026778645966959 * 10 ^ 70 + 9920616097644290314618298756185701955788215328425374795737492022404995
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_370 :
Polynomial.coeff recurrence2Scalar0Exceptional 370 = 50354846668458080510333 * 10 ^ 70 + 75827741420184255008445666847656868614137839960204717803795285111416
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_371 :
Polynomial.coeff recurrence2Scalar0Exceptional 371 = -(470938389779703633099 * 10 ^ 70 + 8340308251624029472747068303341897107217607103661784865608998025203627)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_372 :
Polynomial.coeff recurrence2Scalar0Exceptional 372 = -(743022644416108433 * 10 ^ 70 + 8479443990652253899111019792769044096950164909747983899391727402717366)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_373 :
Polynomial.coeff recurrence2Scalar0Exceptional 373 = -(577603773149763 * 10 ^ 70 + 8402940840422102164501436953480928520053414386924546712316901770911355)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_374 :
Polynomial.coeff recurrence2Scalar0Exceptional 374 = -(264431906257 * 10 ^ 70 + 9478902032801832945501179382808493341079958898833384449889819334700383)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_375 :
Polynomial.coeff recurrence2Scalar0Exceptional 375 = -(73210084 * 10 ^ 70 + 616168142128345368870824449314258905307699470650795034518618388240264)