Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1FirstPart2.Coefficients356To383

Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_356 :

Polynomial.coeff recurrence4Scalar1First 356 = (((851976 * 10 ^ 70 + 6861202570475270929301487694070044769256255556762495152777222809186805) * 10 ^ 70 + 7372330885671799130478519743361364407590157396781036639041754958953582) * 10 ^ 70 + 5375185899581397264428337942911416180166869682925717662307980332724714) * 10 ^ 70 + 8555560008115196139618232605780337015354266360353090223263309498665620

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

Polynomial.coeff recurrence4Scalar1First 357 = -((((253877 * 10 ^ 70 + 2380206000907907542852170233132148602911920376869916127166321623721342) * 10 ^ 70 + 3555636715498769439013741607453454222264754414651112950425043899134167) * 10 ^ 70 + 8989933343910039967982490565405329663863523854384444934353535556493983) * 10 ^ 70 + 4516632607776814420989732863860360527085281409716684289716346977511551)

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

Polynomial.coeff recurrence4Scalar1First 358 = (((64570 * 10 ^ 70 + 1650782620677428846549174400712116548354602966287725226094010354282707) * 10 ^ 70 + 5432447845671288268465809176087649078011765655243666660159574687688978) * 10 ^ 70 + 1108621436132708048246076635647907381037287355484377600827905328276361) * 10 ^ 70 + 3062477158565434299438125887920799124220749130770902489676949301621547

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

Polynomial.coeff recurrence4Scalar1First 359 = -((((10533 * 10 ^ 70 + 2683822216095572984240704250894292143820519958778544502210610323818280) * 10 ^ 70 + 8261963524628190828225973292368918719161854035589149679185367348465199) * 10 ^ 70 + 2627772648969519811881083292933535672310803409666786993769969300234606) * 10 ^ 70 + 5236516608108304234384953613382899023261995027660938845564202014265995)

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

Polynomial.coeff recurrence4Scalar1First 360 = -((((1951 * 10 ^ 70 + 3463596655791753038205049041824954578565680802510916982832577910260654) * 10 ^ 70 + 9609911657349784805521311884467250321605137205823263925758663246530768) * 10 ^ 70 + 9265134920463351495106422619780046156346351906587654920726703345309727) * 10 ^ 70 + 5870220332558105876179557555140406172034415432848478796343280133247812)

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

Polynomial.coeff recurrence4Scalar1First 361 = (((3203 * 10 ^ 70 + 9588909337502732589303194746008109281846778703190891236239921734722369) * 10 ^ 70 + 8623467061352502916850628408989545867553891166549459748263156310573269) * 10 ^ 70 + 5187792484261685540296128547929426346425645809423327198081718505737134) * 10 ^ 70 + 8088795575288669636115981398536957192461719810361308035075898720483282

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

Polynomial.coeff recurrence4Scalar1First 362 = -((((2209 * 10 ^ 70 + 8637711924919552387726588785402920052138677876803079880163420976577135) * 10 ^ 70 + 9701947638789294440972892472572420222653004709222223540674488461394503) * 10 ^ 70 + 2913771667491281965026645146940111393990679478250348511857170708646545) * 10 ^ 70 + 7430898273274215654570980016336947790619902410075855644331644627901032)

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

Polynomial.coeff recurrence4Scalar1First 363 = (((1229 * 10 ^ 70 + 3167494671085977751265218512517282559630595644979351996423747414432720) * 10 ^ 70 + 4989542920165338798194476688810870210836810618405503093715476177619481) * 10 ^ 70 + 2306242769979338026024345596135064617031156173256168331023656185774779) * 10 ^ 70 + 1098057067117486863361155650288178730852445662444003011063237038450819

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

Polynomial.coeff recurrence4Scalar1First 364 = -((((615 * 10 ^ 70 + 7640152282891802952440751936727121698270705872670437317964155370532330) * 10 ^ 70 + 6700986196553479603460519095348381286074209567688459646033012168393516) * 10 ^ 70 + 1004970289879501722692046343851029833304494327809241054365067257350794) * 10 ^ 70 + 3703712386089266642912692602688122055338525784622983133799323449160762)

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

Polynomial.coeff recurrence4Scalar1First 365 = (((288 * 10 ^ 70 + 8298090657641169610887255330187001979329023652109404500519388574289124) * 10 ^ 70 + 7760078818161197040168180763398723601221391793043291246784714472651570) * 10 ^ 70 + 2069324091274291051474823971753815237164111143892800743295049752886367) * 10 ^ 70 + 2918532800565160008202109163631585431435967213231761300355416630492300

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

Polynomial.coeff recurrence4Scalar1First 366 = -((((129 * 10 ^ 70 + 1640674902051111219349488827489918620950056300187823854139157049645524) * 10 ^ 70 + 2471047077594320451224105405179810915817814301516277168866295165259921) * 10 ^ 70 + 4437526199749040229873364988407695637039397370430993265311808870658941) * 10 ^ 70 + 5042953232423897496063470166834957832980089037484993698507067773616950)

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

Polynomial.coeff recurrence4Scalar1First 367 = (((55 * 10 ^ 70 + 5776405518916715165325543772487091395850186681832099320599518777218125) * 10 ^ 70 + 5303526519399962414023965542557988727637821455149935024368492302926550) * 10 ^ 70 + 8253661923044992872110413059732975287211450887765702426974121804497230) * 10 ^ 70 + 1736303901264414509573185662732396516311673190680248894961083328590194

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

Polynomial.coeff recurrence4Scalar1First 368 = -((((23 * 10 ^ 70 + 1205299671398424456572950729854510167893567760643310528842798773146217) * 10 ^ 70 + 4125214216820201978582283896824414241722350676748676649348073540346042) * 10 ^ 70 + 106327765534324124186890367506033100889848660578441639357252039960737) * 10 ^ 70 + 6863871587931589700163992918996445042236531876126126316161293071970473)

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

Polynomial.coeff recurrence4Scalar1First 369 = (((9 * 10 ^ 70 + 3198928727333220273929122430180730951900932714455752609277058240690264) * 10 ^ 70 + 2898500518042472865756911914361228630125884600277582074005125183888280) * 10 ^ 70 + 8715202128605285930405290830521751203796819839293933793093186018795518) * 10 ^ 70 + 7493386347259548048643945813836794469424575515115540029425406154102566

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

Polynomial.coeff recurrence4Scalar1First 370 = -((((3 * 10 ^ 70 + 6423407190110081278707077584379028278282588388192409133117120517486882) * 10 ^ 70 + 1135350636488128198497422395165165983044889432866723959015087560209795) * 10 ^ 70 + 5078096015786427543296557939894418367046221180974539756637414906153002) * 10 ^ 70 + 5241154319986574098844836948738757087539702116980593849591163073249327)

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

Polynomial.coeff recurrence4Scalar1First 371 = (((1 * 10 ^ 70 + 3790305773813558327331520067089145731055501305810073876411785236466934) * 10 ^ 70 + 1580093025033539078802116658929137233235696381707054439420642400631902) * 10 ^ 70 + 5997454132325943384764172135369842985124105247784250916973705691614737) * 10 ^ 70 + 319391072642246526952224708568987385158371849290341245479136589012513

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

Polynomial.coeff recurrence4Scalar1First 372 = -(((5047951864859391420025819146589335263571411929779782322989002423592059 * 10 ^ 70 + 7010010021377975901822815689335923593563163977664297795538336393324785) * 10 ^ 70 + 1112668442040728157330351251000921228747536798160843342144948015297710) * 10 ^ 70 + 7427321194077763984336055604355993164810544932175040033595993111937455)

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

Polynomial.coeff recurrence4Scalar1First 373 = ((1780318896070156601135532587483620680177540224396097650374124686419224 * 10 ^ 70 + 1481843244820731374052405711669579058111906062716250820235317038155580) * 10 ^ 70 + 2743984355333734901327522700089512016498992959424468799105244293687153) * 10 ^ 70 + 7877078751749458754485134150219633343632697905335961943436445873460589

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

Polynomial.coeff recurrence4Scalar1First 374 = -(((601631991357835456485675376232599272730795488542800571001539799401986 * 10 ^ 70 + 8255464429632497627311848871051479871214905853141921885386760911863120) * 10 ^ 70 + 3122473271786409416674902585774930740826310969518769131579757593416579) * 10 ^ 70 + 118904597430722156228790947083303665588041159651236838614540975548702)

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

Polynomial.coeff recurrence4Scalar1First 375 = ((193097130732843364126719796248789832813946564601916143762389572962547 * 10 ^ 70 + 4491196740798444138685301094187784910619726233934569567185746396930423) * 10 ^ 70 + 6568980228525511801018295533225119214283363503559868360182070568922305) * 10 ^ 70 + 6938352280432784840192300705017142850343343074050737538478373180572555

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

Polynomial.coeff recurrence4Scalar1First 376 = -(((57976934469364187698044410298575823572005342777990557312952575715899 * 10 ^ 70 + 9866287851906828752655079065469016940040630118323355411812301902333358) * 10 ^ 70 + 1323696122225092723911706059891671844176510292686888641711530947235514) * 10 ^ 70 + 3752593567502528688961421685513674623199935604847478181649363388961721)

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

Polynomial.coeff recurrence4Scalar1First 377 = ((15815165317160723710207850131241144582738665260685914897591983707339 * 10 ^ 70 + 3701709126578915170879601701856687683120903495770349896696156683477942) * 10 ^ 70 + 3230959977690617102924050171736606480529176183544228934850420108823729) * 10 ^ 70 + 5631583165281588072054138439934080083284455903176457504440299087360103

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

Polynomial.coeff recurrence4Scalar1First 378 = -(((3656221844231908386513134469410256610482869261326742860317941413280 * 10 ^ 70 + 9604326501536007641118514597661082846176309686494462670849019352106408) * 10 ^ 70 + 8200059942692213606800446706795723342014695090053589604050168265011148) * 10 ^ 70 + 3247595671280359189303039026279196183011240432185540827596982521246711)

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

Polynomial.coeff recurrence4Scalar1First 379 = ((552779547190033443550116257221212198159756876720724921041489154441 * 10 ^ 70 + 4279085597894204709052923740124520960036308862436269741341960758261956) * 10 ^ 70 + 6056200655575935949942807320352467520029473583100537960844668811746262) * 10 ^ 70 + 7072370310219942713390480262322064288952881642548821214648516533478558

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

Polynomial.coeff recurrence4Scalar1First 380 = ((67733002895135294915147147958686678160430963762690931772465247754 * 10 ^ 70 + 5809009584659994969667837101321032024116303978684519525042260639121264) * 10 ^ 70 + 4719251770635413101003814171261464025941428793866344429487018207114070) * 10 ^ 70 + 97696664767797938707582107677341790972193667559939858248005126544702

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

Polynomial.coeff recurrence4Scalar1First 381 = -(((110786896572173366102496578284293791119201536233770122864341183835 * 10 ^ 70 + 8074660260407849838986310688374695120236716376975599633557934964542112) * 10 ^ 70 + 9744526251695890396769847571594633209270035602579439590046838236071078) * 10 ^ 70 + 3469509430222651343575750311427563193000221224055719224903928358356897)

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

Polynomial.coeff recurrence4Scalar1First 382 = ((65416050483493921045371673870005464385898982428340785235777135348 * 10 ^ 70 + 5087008849296683577834889087751596319967659436728193551325037634848062) * 10 ^ 70 + 9430585987761779497148960732103937955170655631813066591756823618229422) * 10 ^ 70 + 3457611224615131280800429370148935646610478559441722633890883957259983

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

Polynomial.coeff recurrence4Scalar1First 383 = -(((30169167216653489824769675501638440290429374953786324888243292611 * 10 ^ 70 + 8396375040253065289625794832748375757901190253692200726535963111627798) * 10 ^ 70 + 8036791618934710606353484733995457086313805758565107267777471806108287) * 10 ^ 70 + 7809028912870126231621433342594575219049910769436779258931879797550705)