Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart3.Coefficients383To406

Recurrence 4 lookup certificate: Scalar0Main 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.recurrence4Scalar0Main_coeff_383 :

Polynomial.coeff recurrence4Scalar0Main 383 = -(((1550281776055281683787193889001610444182344719675849098661502316239 * 10 ^ 70 + 8965633575460153653180983948933927725096511314800372923359167589747795) * 10 ^ 70 + 8595039959943704505210564080382486990998263857309452055397603726022804) * 10 ^ 70 + 8816821870729057489575162989332600802330196570966785379009558369867011)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_384 :

Polynomial.coeff recurrence4Scalar0Main 384 = ((89751622854329376054539901515347574672795440519505281114112251079 * 10 ^ 70 + 8920603145033274815945308888908424438686551328542094901444790709067774) * 10 ^ 70 + 4114075792076485555727522252814285470514861996429449213990700278440729) * 10 ^ 70 + 3450671797389881656046967842971865622939348633594158414851577775056338

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_385 :

Polynomial.coeff recurrence4Scalar0Main 385 = ((109434099580917174100793396234022531074377449559865793944294208449 * 10 ^ 70 + 7857937321622775915298338064248298399644744297437071481741221970234100) * 10 ^ 70 + 9218988843047118580865865362127350858463540815073554284734019970294321) * 10 ^ 70 + 4365313397436336460500017539677690528540643930280529694856779280055813

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_386 :

Polynomial.coeff recurrence4Scalar0Main 386 = -(((78825841056154704991534175841469861816947792506350713157547358805 * 10 ^ 70 + 5069552067950796446271422154513780288602922035168219745965481318078459) * 10 ^ 70 + 9091289922504510036703477387340163755166844853315657194291583944928547) * 10 ^ 70 + 6277335757349481927832272986823680522846604768164182307130868975879988)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_387 :

Polynomial.coeff recurrence4Scalar0Main 387 = ((38258934127880910935897024597994966387088967546671767557802683595 * 10 ^ 70 + 1864847996255874575281258485892889301518261720924076678336613698314103) * 10 ^ 70 + 9309861310653682151950419885809219094539405571479613264746458771797052) * 10 ^ 70 + 2151639691510720504299516367968456578331602551102496919166024666312821

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_388 :

Polynomial.coeff recurrence4Scalar0Main 388 = -(((15923791005933361947914695473198992299285668877464185805107019486 * 10 ^ 70 + 7256754959324629351366361523893559463070482132041759638386581362381725) * 10 ^ 70 + 215871677737875875453012989276724790401799240704377658867152431306918) * 10 ^ 70 + 7082202730235318499601062858911894609217318160598082981466409564071544)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_389 :

Polynomial.coeff recurrence4Scalar0Main 389 = ((6111019277396755183412941355772947816824591056464974468053344533 * 10 ^ 70 + 5553965027196376469045097340850906528710010503465422952811679437071454) * 10 ^ 70 + 6174078643504288723299232878137525498660744945949039880733954228146109) * 10 ^ 70 + 3520394735572730793682155624821575007166617458146533054521100487470623

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_390 :

Polynomial.coeff recurrence4Scalar0Main 390 = -(((2247135996383902147597092922856576711279585666759434004707899533 * 10 ^ 70 + 6199721684893881038287836910616363392540168206739487280641357716605798) * 10 ^ 70 + 9773893248026819999662536062198553787801472641223656830637916800674869) * 10 ^ 70 + 7313015348923021131285526579458142617406767887565237230722526727884946)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_391 :

Polynomial.coeff recurrence4Scalar0Main 391 = ((814657803954929209114942857554277772980913352643379954341285694 * 10 ^ 70 + 848827963735396870269923111611757914927573997850066077847807708207447) * 10 ^ 70 + 7652950508797977708034405718819852296690894167353850244478356337005284) * 10 ^ 70 + 1338930958726714984407659626246190227347201179794849917718677010002112

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_392 :

Polynomial.coeff recurrence4Scalar0Main 392 = -(((298057461460808952664973447601826126856914279534513876913918146 * 10 ^ 70 + 9365161284723152119678033946318867363595851802917710393136355563784608) * 10 ^ 70 + 6793373172904857096741814707592827272106838245293212057212425738875106) * 10 ^ 70 + 7564045508050842433187664023621612757669387238872173199153647253883775)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_393 :

Polynomial.coeff recurrence4Scalar0Main 393 = ((111817284825224806392120164813829396512789383724853781446771918 * 10 ^ 70 + 7373940831139556075025344708582234383505478132891363321682653928296513) * 10 ^ 70 + 4408622811350811621042747020499146214946479410686815744334471343652518) * 10 ^ 70 + 5792423954206240139299857781623498936157414528055835362368509315721092

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_394 :

Polynomial.coeff recurrence4Scalar0Main 394 = -(((43212113604562776326119719215534456018098523940816197496608601 * 10 ^ 70 + 4684066653506294522732091970063398227083850180552705418747994677504712) * 10 ^ 70 + 5417613950887411825603704909876111935709370372047811611639504704704363) * 10 ^ 70 + 281495304309754083478992798604006643377484035836058671616560684010298)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_395 :

Polynomial.coeff recurrence4Scalar0Main 395 = ((17085655710863461887359743457224333914448634373906432519756481 * 10 ^ 70 + 8293602479011342400850693264565914988182058158126862559309078047728513) * 10 ^ 70 + 705202143556448663366234499065869668401389745951443116699429006404004) * 10 ^ 70 + 5356039743795250667383810266863860728964146292412190228716953519240734

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_396 :

Polynomial.coeff recurrence4Scalar0Main 396 = -(((6818445211343368579938946838094353354459267983801489313976931 * 10 ^ 70 + 2875292686813310918060647437820521769551516162247610639803093797650739) * 10 ^ 70 + 421291963785606765160760024891059076711781801750716424069568492842543) * 10 ^ 70 + 2681312208895795600528680803210884839929412956430211370806737261337279)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_397 :

Polynomial.coeff recurrence4Scalar0Main 397 = ((2706680240162263082690605420404427712875358527719281273126147 * 10 ^ 70 + 6351295992112878784245274474947883604978415597730218124112832641902799) * 10 ^ 70 + 7420288000758245480468899623702330285123681759706687832729425254380241) * 10 ^ 70 + 484535271235069721097346171772671920592305148971461351322184025676154

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_398 :

Polynomial.coeff recurrence4Scalar0Main 398 = -(((1055979036560296983134087104754577266619855657515407610625114 * 10 ^ 70 + 4216133857885359260199097840112066196293171155868659929438211173092736) * 10 ^ 70 + 478096365798596782565960671364737132343414173391418299545721325707315) * 10 ^ 70 + 2698213876701351667970270318209092775190947813500800668171252661851523)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_399 :

Polynomial.coeff recurrence4Scalar0Main 399 = ((401398494743892307907291052348544221238885254278649543385853 * 10 ^ 70 + 5961518464946550344758268360956962403126084253494502072930071271642182) * 10 ^ 70 + 9562057825325269635016625711329439246970722948566019262978150069940464) * 10 ^ 70 + 2790199870579970666031669651049139162145837253189962752846807394048427

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_400 :

Polynomial.coeff recurrence4Scalar0Main 400 = -(((147787998676287650800763584603589393573272894506495210444223 * 10 ^ 70 + 8742701014779676248989807078689563834300182973215865738570473542727002) * 10 ^ 70 + 3278092577435192947440235574427956956805559143407328563959847237993220) * 10 ^ 70 + 8506659663049824273408714656429903946337751305236207446611987368552818)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_401 :

Polynomial.coeff recurrence4Scalar0Main 401 = ((52488000670668751257711949397197092009799618029236247917248 * 10 ^ 70 + 9865217717071965908736377786078385397166654431617927781688604694574330) * 10 ^ 70 + 8183498493972102853133628597986676236928007975971843366224933732886576) * 10 ^ 70 + 3510276743060868999683785995147347487508562576233841308699156041049510

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_402 :

Polynomial.coeff recurrence4Scalar0Main 402 = -(((17923459111933868003168799254010705051307530849553116143178 * 10 ^ 70 + 2437564918401379849783838325023384334325377666678701834653187165239232) * 10 ^ 70 + 901420069144361761371227864899058826323230342478641608643190308889673) * 10 ^ 70 + 6395061744734664511714240156466230023822562432781768222494223622369244)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_403 :

Polynomial.coeff recurrence4Scalar0Main 403 = ((5865810805140931420543026146487926924688235746587768720908 * 10 ^ 70 + 4158580455418504093542303404157479729590731649077534154454409785521809) * 10 ^ 70 + 7082399513366273958131838259904923710023438450229312149865146815285722) * 10 ^ 70 + 7172072670287012841270964695197756980329853914185353076693839475874078

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_404 :

Polynomial.coeff recurrence4Scalar0Main 404 = -(((1832547868667909447803691192024041707349770927750628455586 * 10 ^ 70 + 7542380954204453522878166873675126772873546363396094872511668681473729) * 10 ^ 70 + 8780658012426345234040527696413149144612124419661319330054052406363001) * 10 ^ 70 + 1667242135344240488968554072637443060383549642759020165742050797331)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_405 :

Polynomial.coeff recurrence4Scalar0Main 405 = ((543370606842792471433799940897282001087875418120738089376 * 10 ^ 70 + 9631985063383176652492430775442041356208321282555949454733153709739260) * 10 ^ 70 + 5419294087869958506854140493057537836935752958582784673152231798882896) * 10 ^ 70 + 7964521675676160158642007749155897329785060194768430492336946979726497

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_406 :

Polynomial.coeff recurrence4Scalar0Main 406 = -(((151480281992675671525902224977866015436825090402900860294 * 10 ^ 70 + 8795274762958023499035713117339821224488555128748840812103478297929766) * 10 ^ 70 + 8337971118611195861371760486364807651465179333927582882726610781034600) * 10 ^ 70 + 8292107217544269997595621867523035621721105320835149969437599202250911)