Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0ExceptionalPart1.Coefficients313To342

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_313 :

Polynomial.coeff recurrence2Scalar0Exceptional 313 = (40627693261718843912975071827347 * 10 ^ 70 + 6925712030612436085177424754570902606942647845620071905811840353983843) * 10 ^ 70 + 5816412160725570566238853981370886299225581141000929759619778227052600

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

Polynomial.coeff recurrence2Scalar0Exceptional 314 = (912069929414519886267276898758 * 10 ^ 70 + 6425599035673400756747579571386293465879315103986035761652523943735891) * 10 ^ 70 + 1951638568980240800987248635690442897745821577341171072502756912163100

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

Polynomial.coeff recurrence2Scalar0Exceptional 315 = -((1923728069380584480278129213451 * 10 ^ 70 + 1017524035404767773146093213827793542726221602067785059080893209905233) * 10 ^ 70 + 3635740443632282476764176593152394798961633714925996079256958337566852)

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

Polynomial.coeff recurrence2Scalar0Exceptional 316 = (478931550550300139503417039955 * 10 ^ 70 + 336143846911064208081577800441281891636513951866818274315132519818782) * 10 ^ 70 + 6867734703114322058124701440461772419806259540685461698079737385035690

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

Polynomial.coeff recurrence2Scalar0Exceptional 317 = -((52369803124807781820871502022 * 10 ^ 70 + 3328445994576987332310058849504395215615020534264811860162065578795423) * 10 ^ 70 + 4137653200192052197325743525177610018340132328731338529699409199144053)

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

Polynomial.coeff recurrence2Scalar0Exceptional 318 = -((3334807923400619107476865193 * 10 ^ 70 + 6214970301349103870444231752099090852799585896644353626043812139973328) * 10 ^ 70 + 9963478314633985642687549409205387971934430687052288523787965106252886)

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

Polynomial.coeff recurrence2Scalar0Exceptional 319 = (2309668772067368458780058504 * 10 ^ 70 + 2525983144265291125271364229058276550105699826676115803423219446112696) * 10 ^ 70 + 2223477416326517154564677058098291410559794636751184686440008604366271

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

Polynomial.coeff recurrence2Scalar0Exceptional 320 = -((373700876175921726424896981 * 10 ^ 70 + 5962944936169950568219734705794487223663559980414958822190564800699656) * 10 ^ 70 + 8887558019269918955664623499946132591702987259682897699861986130813335)

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

Polynomial.coeff recurrence2Scalar0Exceptional 321 = (9853191657987538575526719 * 10 ^ 70 + 975570030873281712027692064457221033538179748346008751029550872155519) * 10 ^ 70 + 3744318548826480598698401499394089930842548318064761521390125019240227

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

Polynomial.coeff recurrence2Scalar0Exceptional 322 = (7135991837247487775535645 * 10 ^ 70 + 3675832825685843417573913083949254009109639030664426463370336996425097) * 10 ^ 70 + 9898808837758105341189935920177948164879537593119138486441986044709804

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

Polynomial.coeff recurrence2Scalar0Exceptional 323 = -((1241363710467434377197571 * 10 ^ 70 + 7784004739349815763693185605981096477633345342368577064572490738717256) * 10 ^ 70 + 5933338103223275684859453257553611664815881561358095327709726080279954)

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

Polynomial.coeff recurrence2Scalar0Exceptional 324 = (3283358208682570513380 * 10 ^ 70 + 1207185388915442528516117949127109257337970353549253483855979370975730) * 10 ^ 70 + 1470005902667061799868468213154894510991198689848229134761057042929257

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

Polynomial.coeff recurrence2Scalar0Exceptional 325 = (25817007487769173157518 * 10 ^ 70 + 6140707875165777286265907469547174497418997454297419561489499724501334) * 10 ^ 70 + 5462649952826333543712693794306573604236501372615307775072006196074424

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

Polynomial.coeff recurrence2Scalar0Exceptional 326 = -((2392404810161593292044 * 10 ^ 70 + 894499073081361270677690955464079083766875007739352424433055981726812) * 10 ^ 70 + 2066569105896894214387779129436982141292098386278344167651098632344841)

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

Polynomial.coeff recurrence2Scalar0Exceptional 327 = -((444288667555734263878 * 10 ^ 70 + 2871558134208060097066898698226422084618577009256130552727317254334520) * 10 ^ 70 + 3136263163180463631343142442329877772999739144151873879042319786000011)

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

Polynomial.coeff recurrence2Scalar0Exceptional 328 = (110908266604634067644 * 10 ^ 70 + 503550503642397142572279852686106164759257389530356276512790390755849) * 10 ^ 70 + 2342102469631787899338498057135154196444708692884727931870976022492371

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

Polynomial.coeff recurrence2Scalar0Exceptional 329 = -((602556911900047361 * 10 ^ 70 + 282255714498476679286547475888384010346985676792036327817678510755094) * 10 ^ 70 + 4372206336283598181686423889310553599812688571744673570277415729195248)

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

Polynomial.coeff recurrence2Scalar0Exceptional 330 = -((2720805823138029237 * 10 ^ 70 + 7772154749060233325646639966228964974563900219026599003700222853273395) * 10 ^ 70 + 8205216201445756759207656879374296282074715768723764064489618213892932)

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

Polynomial.coeff recurrence2Scalar0Exceptional 331 = (323680619809591065 * 10 ^ 70 + 3931077723159643403528193000601948279212969649083999574933519809642576) * 10 ^ 70 + 8064257313518979415000710077682641579385575341305453737466861592644434

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

Polynomial.coeff recurrence2Scalar0Exceptional 332 = (22257331312666993 * 10 ^ 70 + 2787882516140613015072613766192526144678904716112806189734475657659924) * 10 ^ 70 + 9363702252588248086303729686885028843070311304259383927938252580802804

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

Polynomial.coeff recurrence2Scalar0Exceptional 333 = -((8410133343129128 * 10 ^ 70 + 5225953477390907948291821059493636656944499445243516178385667858346965) * 10 ^ 70 + 674181149515824139518263606126366126441149494320750082009427395680782)

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

Polynomial.coeff recurrence2Scalar0Exceptional 334 = (379666602022818 * 10 ^ 70 + 2533901192387312715877974971368232410055558490233502009076034325068263) * 10 ^ 70 + 2513868574698413766710306377371085477237752067910242973532903942852848

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

Polynomial.coeff recurrence2Scalar0Exceptional 335 = (102000767163571 * 10 ^ 70 + 9456478166017339203790070117938287197326077758245135234115054065581571) * 10 ^ 70 + 556731773939359096926147164035614584002153513058438586935341688159907

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

Polynomial.coeff recurrence2Scalar0Exceptional 336 = -((12834799925145 * 10 ^ 70 + 3914599178692664024851270682380476871295742588377108310935137290155210) * 10 ^ 70 + 204371890718670421450252607956532259475609665299102784337894962850837)

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

Polynomial.coeff recurrence2Scalar0Exceptional 337 = -((537291076535 * 10 ^ 70 + 9775458882066163626040149846493959894531145539194129188139764149764919) * 10 ^ 70 + 6891568739709302946848727250011543089031391550982202904437157447199836)

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

Polynomial.coeff recurrence2Scalar0Exceptional 338 = (182197382754 * 10 ^ 70 + 9222872208947686728561021782997817937740220939350787466877519166166980) * 10 ^ 70 + 5720973124680755844217217236981114043873016733970265584346184146698185

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

Polynomial.coeff recurrence2Scalar0Exceptional 339 = -((2056984577 * 10 ^ 70 + 23399435709789210727864072131210897884128131958495578355493516783700) * 10 ^ 70 + 9166037063864421283279543415502691646953469784345946614186177243430811)

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

Polynomial.coeff recurrence2Scalar0Exceptional 340 = -((1740775701 * 10 ^ 70 + 3327354072161394226333227329318130735731557467402815264483594382202583) * 10 ^ 70 + 8585984249937844098901100299464496005090914571563430246022558219051746)

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

Polynomial.coeff recurrence2Scalar0Exceptional 341 = (61821980 * 10 ^ 70 + 8071475621895784062515512810772288819444413441363921911457754947783725) * 10 ^ 70 + 8532616897593468898865468094425449264177878258889822910744748230975241

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

Polynomial.coeff recurrence2Scalar0Exceptional 342 = (13322817 * 10 ^ 70 + 4163507305876377393251146344717032595489189080883932720682010334383768) * 10 ^ 70 + 9557479742931498691171941401776907672198807219306872587362895454345073