Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2SecondPart2.Coefficients374To398

Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_374 :

Polynomial.coeff recurrence4Scalar2Second 374 = ((38746287200054783452990775342142074950576510439388268047873089631692 * 10 ^ 70 + 7385384456487308305582994287143576348770899611595723332293739099893086) * 10 ^ 70 + 4600534531811854807975486321982327024999338746289728681569400214048769) * 10 ^ 70 + 9886105921776051443113267618884566080055153155507889420525831964333995

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

Polynomial.coeff recurrence4Scalar2Second 375 = -(((11031326007482652174101316398512031289854710545930302167470799403466 * 10 ^ 70 + 4172534630482859021254751331607828902922254224413171919670019053351636) * 10 ^ 70 + 473383393893092063288730786319901067980036864383886785072179710699320) * 10 ^ 70 + 3634132265929668452266425077527669295523632784530380211232977013625119)

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

Polynomial.coeff recurrence4Scalar2Second 376 = ((2866436238966211743624707332649774414048681855047779624432399898452 * 10 ^ 70 + 3501159744116792207837699895568569177637301731231751184917858129285892) * 10 ^ 70 + 8186762604529151819325627828162280681178478229804952056433756488982587) * 10 ^ 70 + 8323879504293500523021286820246823071164188922398234789103475052744881

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

Polynomial.coeff recurrence4Scalar2Second 377 = -(((641589307720151358379197939887154115751814885516822935665743961199 * 10 ^ 70 + 2147069318885751784606857433363673743145670978433986811768448750318638) * 10 ^ 70 + 3654538403647968576463922659190850551925294708612105403484626390201935) * 10 ^ 70 + 2433376644231585221056197699321742355528338806421784513033920976545336)

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

Polynomial.coeff recurrence4Scalar2Second 378 = ((101910038470230221388909107853010003903697740454372911409278511451 * 10 ^ 70 + 9076304575100684019141382016470475980396146292407589420870164111106365) * 10 ^ 70 + 9191814845239994759421359179320992686842836460226459080784730337672685) * 10 ^ 70 + 1314407451031569951802591119272931546867199369754227343695462784971586

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

Polynomial.coeff recurrence4Scalar2Second 379 = ((3232674094570134230649982401533658000771335464226595062564308547 * 10 ^ 70 + 7277775461132292420610139422852948295504734475709468583246036031496749) * 10 ^ 70 + 4692030871063106133144602369172829576569821399933250971314276258182054) * 10 ^ 70 + 3116916655400115650164387936727939153807105915893229820242253698499871

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

Polynomial.coeff recurrence4Scalar2Second 380 = -(((12682561106500804334087886884304476355308494975724294337946199973 * 10 ^ 70 + 833885705036375504670056573312697289202025959271210100622692227739813) * 10 ^ 70 + 8582536352973966961007801180930765529784276058941360071262786723405016) * 10 ^ 70 + 9788734477238993292251524272672854188244958606459172042856012302593884)

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

Polynomial.coeff recurrence4Scalar2Second 381 = ((7657637224789611426253233958216835201447942880005507303442540877 * 10 ^ 70 + 8051070789157107192568227119287835625025428332102117290416387760292831) * 10 ^ 70 + 6482157911905972949266656773418537171434664066767584104406092002653718) * 10 ^ 70 + 8489727452110319375526891580134658217906963434192298887064887043723874

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

Polynomial.coeff recurrence4Scalar2Second 382 = -(((3531736959837448561144613833429876426914158883714264728650248080 * 10 ^ 70 + 6606920218733610210322731864168317904556778479889414331913464195517366) * 10 ^ 70 + 1989296427028677133328814259958175712541458406993044508753523521917897) * 10 ^ 70 + 5280543042353327144289010326515685150285196350193609286271413252670636)

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

Polynomial.coeff recurrence4Scalar2Second 383 = ((1458353384009747673508190427475574535747738286373089200714715448 * 10 ^ 70 + 5074279428695294332535596573250562472895356549242655312767033272031048) * 10 ^ 70 + 9716412564365979466824369676970876580771751402259930896775966777587362) * 10 ^ 70 + 8565441354949478930602428265965445143416420997139259037793290936021776

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

Polynomial.coeff recurrence4Scalar2Second 384 = -(((572866453725109364660534873595666603877569989322109529642385050 * 10 ^ 70 + 7960928795072835059049961031732033214631516033908646577027392542789426) * 10 ^ 70 + 4851255533451174616215778958034791413008866129162723778688630788006926) * 10 ^ 70 + 2135152591700813627800044647321805197448623418023206947523858610934389)

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

Polynomial.coeff recurrence4Scalar2Second 385 = ((221541906568022910328782828204855652543587787703836556527978735 * 10 ^ 70 + 9636399113114612401177304860495847943447131965172274671381581378957134) * 10 ^ 70 + 21960354497527806954473231993647969307829581833315483524164919394986) * 10 ^ 70 + 1588872058666562161790894921306367187865527634048052983704626316536295

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

Polynomial.coeff recurrence4Scalar2Second 386 = -(((86123164768638926119337241488850060982765125393158799034028503 * 10 ^ 70 + 8912109029831532328895618326694623872990123497316821325691016004535397) * 10 ^ 70 + 6971681991010189867620725022314556287005497364318072276632581599105420) * 10 ^ 70 + 5981605274293695764839045045288056004651829953583827091687668043201679)

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

Polynomial.coeff recurrence4Scalar2Second 387 = ((33967173546214728006481535548419572644839133153944182231965266 * 10 ^ 70 + 7397769935470578391273343490823028907283239085361998057601212102157448) * 10 ^ 70 + 9936970858830507300865061790007537550671789204901025466039542469692346) * 10 ^ 70 + 8884399103184348466707357093824079527283797850735871991160864728049699

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

Polynomial.coeff recurrence4Scalar2Second 388 = -(((13576916023994189641348185016448416151032315513082225240719304 * 10 ^ 70 + 8331577783040656383690535035758970535259355421780434666587898927451966) * 10 ^ 70 + 4200508705953105195422447513422663406061557823104666929137887849016599) * 10 ^ 70 + 7674093305070051175904150062160320212376201957817000273057262638380678)

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

Polynomial.coeff recurrence4Scalar2Second 389 = ((5456454076756558736551338006065591566850669462847647556347764 * 10 ^ 70 + 5755774997135084964525092416792235665683209137281520958321453620281590) * 10 ^ 70 + 8357519871859963253220915459936628382756919171233408596927199698312886) * 10 ^ 70 + 5974599165649867528624387092548679892716038621853611434866522341200971

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

Polynomial.coeff recurrence4Scalar2Second 390 = -(((2182350467065840974437178167393655296814285928431296083564457 * 10 ^ 70 + 3100096784211781434153689546369348117253636186179038830393280805797164) * 10 ^ 70 + 2152776392337291553477780818746451988000415206256336663845479493682482) * 10 ^ 70 + 7561285562806096412943182547517147052995093494440969129716782023371577)

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

Polynomial.coeff recurrence4Scalar2Second 391 = ((860501029053374203153262904962510471444677213145974481026124 * 10 ^ 70 + 9037383145515909866568872799505529004097496074769360263119041860084704) * 10 ^ 70 + 5441963860614017093649468002189460040582090835790876342764414610590665) * 10 ^ 70 + 9857549398610940302541232912661262935402525617145235761923251795600156

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

Polynomial.coeff recurrence4Scalar2Second 392 = -(((332078747524859340628892875600211153125208851427410501958346 * 10 ^ 70 + 1599850824796547213538935042171430583642167410607078580494947569605565) * 10 ^ 70 + 7507883026161742910298483238958480606228257823478533078749987549740891) * 10 ^ 70 + 4919300808531069424703293373630700574331090470322523620636083039084811)

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

Polynomial.coeff recurrence4Scalar2Second 393 = ((124789584315940123608407122840916853288290024927182712802003 * 10 ^ 70 + 5697942637806439050079264507655429508787845759742569939158027932105556) * 10 ^ 70 + 1580864610251390953523302031124613746063205649078220020766074161765292) * 10 ^ 70 + 6313343480718794449919821729456324708263357358799414001343673393521153

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

Polynomial.coeff recurrence4Scalar2Second 394 = -(((45502480244245857745027568896497683739972147771630333974629 * 10 ^ 70 + 3855270544440012843807723930598012966652192850089209798346861119574801) * 10 ^ 70 + 9896772545774614299895604629663612245736330059708050391071412580569321) * 10 ^ 70 + 4343995145841309192182254495768399928846784139661496875080332694518699)

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

Polynomial.coeff recurrence4Scalar2Second 395 = ((16057700276292197291541877022451046421008577190163671545108 * 10 ^ 70 + 5427660529936096198878402080754028245876617546568062671925276219475783) * 10 ^ 70 + 3073414261087834734215672227414147335576882883302184820186413208658136) * 10 ^ 70 + 4868703382567130219928928075894698390428396789186170564874523000695464

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

Polynomial.coeff recurrence4Scalar2Second 396 = -(((5471953280461656606858347923145781899885419663597098545742 * 10 ^ 70 + 1658911142727291076871353771090798200459117265365596659977867800020472) * 10 ^ 70 + 8772149109848810972338285006848496752893846409563058869572288816495635) * 10 ^ 70 + 8984872907714986423740810543066447743591686210988131630738068595854932)

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

Polynomial.coeff recurrence4Scalar2Second 397 = ((1796231564784907584397291980212698407350598054874495788034 * 10 ^ 70 + 2009884713079349869894837319489302741602906454084850365514478607119418) * 10 ^ 70 + 5342756100408183513960427422603319950537769899055149146582894572261022) * 10 ^ 70 + 5880076676524730873879231324849017364316926669066778492661448302494812

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

Polynomial.coeff recurrence4Scalar2Second 398 = -(((566258740503927008522145264296071471469400429048849059017 * 10 ^ 70 + 262460792453394030443992560473897102822009631155260665788051687864684) * 10 ^ 70 + 4279266681234394106416343334965939112346033108581527644664893354654756) * 10 ^ 70 + 6351450994793218087509182878396578605130564349834908265109015141825201)