Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_407 : Polynomial.coeff recurrence4Scalar1Exceptional 407 = -(((4179776903337181702899687736177177798966855152737254 * 10 ^ 70 + 638398796394668250399716755638319235774369502405503850132894116792351) * 10 ^ 70 + 2039628452474701959103291629389184857854397907585447908433951720213124) * 10 ^ 70 + 702342889974024151077458534035498412730767417015969322097405240907841)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_408 : Polynomial.coeff recurrence4Scalar1Exceptional 408 = ((37871499151891776977905094566426317137059541136776991 * 10 ^ 70 + 4818968247920960946700007606613910537705260982827420906058664157979399) * 10 ^ 70 + 6413115590385753201611668660741031689524972205850070457632561210925171) * 10 ^ 70 + 3962133598938730895850357709324129190339460013746083679148175455858972

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_409 : Polynomial.coeff recurrence4Scalar1Exceptional 409 = -(((22058724044786003272289880707200707343801787412166213 * 10 ^ 70 + 3600861783489982435501699375266951401391894598530287945837354318882780) * 10 ^ 70 + 5654631029032371543325413404837870975233517797902947211066747596852127) * 10 ^ 70 + 5713164609468596689496764159233327305762435846400731282112473899874128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_410 : Polynomial.coeff recurrence4Scalar1Exceptional 410 = ((9499481198093857512162872527717470594622239728687209 * 10 ^ 70 + 8555217875176420480594139041210337841539285258989100125455201396555317) * 10 ^ 70 + 2440002359365833603463033680637983698228559728010800450811210848500887) * 10 ^ 70 + 3349235007369676042920837986812197941624153654978250425502983987294244

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_411 : Polynomial.coeff recurrence4Scalar1Exceptional 411 = -(((3555202290760719948121732477398667450923584532280199 * 10 ^ 70 + 6879018505742760846404601204124100612166784534491344325282736625464211) * 10 ^ 70 + 5439763641207606908428993835590115362943884267712189912398358691357771) * 10 ^ 70 + 7693201676977849928896273262228747240298843273539974791287913529407755)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_412 : Polynomial.coeff recurrence4Scalar1Exceptional 412 = ((1215362965045628626595877710052963455947711583489689 * 10 ^ 70 + 4843867028536757921468504880171073127097041146901099030939763921623192) * 10 ^ 70 + 263269930117468657871018427623719586824275211491491209825618540712476) * 10 ^ 70 + 891456836488287669706494288098345912974513574946758999803616676502408

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_413 : Polynomial.coeff recurrence4Scalar1Exceptional 413 = -(((386588626477770282663688183652080768449740360399103 * 10 ^ 70 + 4044561221180753097027865002424074047210327007762438778215775632720617) * 10 ^ 70 + 1915759691505847582740839701049538534325801380075490869734056747992888) * 10 ^ 70 + 7841361821798241375238126848307540644522395216460719167671896220411831)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_414 : Polynomial.coeff recurrence4Scalar1Exceptional 414 = ((114788289795616172326411093604011614578172901459461 * 10 ^ 70 + 9146792576820886232691674126681434599941758811378699611194236083782534) * 10 ^ 70 + 1849695129147619717303282515378300831340841221562362551224783040927675) * 10 ^ 70 + 6368225077532317216961075777952417925007579353122887266415124135524031

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_415 : Polynomial.coeff recurrence4Scalar1Exceptional 415 = -(((31528693946067047190696998021302818699176193223555 * 10 ^ 70 + 5000354625947778970026392979273739818975396932442926318372443305241933) * 10 ^ 70 + 6947160449213154548921728908937326508111728458272497658670786073530870) * 10 ^ 70 + 6486758462119539999853097443911218799780759234651149194985182679235362)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_416 : Polynomial.coeff recurrence4Scalar1Exceptional 416 = ((7805210377499584586390186137753569331036170224619 * 10 ^ 70 + 3856383241385114889108912616496523418661248584637440208418013867080877) * 10 ^ 70 + 876878610463118713394659152581889653397201485806672698164206267951051) * 10 ^ 70 + 2207036496325196306743510192458136430992000071902619242164017158552581

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_417 : Polynomial.coeff recurrence4Scalar1Exceptional 417 = -(((1632201825788427607824254270402302180829874554758 * 10 ^ 70 + 566901357288232783344295473301311298648675310342336543173914780644549) * 10 ^ 70 + 4674429646473234301545034675877668825626140905346485783455632754397762) * 10 ^ 70 + 712239906903364960312593074644372744229601600374198795165582770832368)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_418 : Polynomial.coeff recurrence4Scalar1Exceptional 418 = ((229646858464208855609991224993346665936907028626 * 10 ^ 70 + 7546846129076486959879065860698537914063192304301318512132638644494638) * 10 ^ 70 + 3050021171216691577596836312448333705503114305960115861365105161956043) * 10 ^ 70 + 1613774138724940955514183121177709300397046378461052681464571543857108

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_419 : Polynomial.coeff recurrence4Scalar1Exceptional 419 = ((14906166062752847575398375007883590548500056834 * 10 ^ 70 + 8826859386858396717427816855048824391760874412104125686375367805783652) * 10 ^ 70 + 5506454149001280341316102509756533649302122509089267669248613376164433) * 10 ^ 70 + 8267869514286672553165543986196175649093912180204719222221352208411704

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_420 : Polynomial.coeff recurrence4Scalar1Exceptional 420 = -(((28107570704229070251893648358544559368987238029 * 10 ^ 70 + 1076402479061813761727435849921310900778855375871550261222667076714482) * 10 ^ 70 + 5924554104074179455624809299977167190428227915511858509233192546900631) * 10 ^ 70 + 4368220485589245083056599440908834935182698247889122413074368917810110)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_421 : Polynomial.coeff recurrence4Scalar1Exceptional 421 = ((14055267887484909216365329410843879903000708225 * 10 ^ 70 + 384916899455587674903016437100054536117711510201331677368560325005810) * 10 ^ 70 + 6143810873541117935252601780806304069995098887988803116580468116026112) * 10 ^ 70 + 2648032871868934476524818899177807139655029266107368506034887766117141

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_422 : Polynomial.coeff recurrence4Scalar1Exceptional 422 = -(((5215455011020100220672632992726546026742592391 * 10 ^ 70 + 2902117155863427170870019169634361170508026603391503595385763058522267) * 10 ^ 70 + 2860890760370183838739575221806796568273604127486665992058047566642860) * 10 ^ 70 + 9728689015996283575842542812983654364491402835820138085397881421532797)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_423 : Polynomial.coeff recurrence4Scalar1Exceptional 423 = ((1620487035659883952558393865969755804595405109 * 10 ^ 70 + 2029955013248110016505174759634443352658090798721802300856187044862154) * 10 ^ 70 + 4894309499872207544987048573903232917152729291734935823782887015128282) * 10 ^ 70 + 5979078042043379548741514147410060918705378931373767592040533685075504

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_424 : Polynomial.coeff recurrence4Scalar1Exceptional 424 = -(((433000701326570192726873723914192079348548012 * 10 ^ 70 + 5350937451420036566858083798349680262480266476982753003077593789846799) * 10 ^ 70 + 3219273113246443600784676904675051823732086366155628337800856936917273) * 10 ^ 70 + 6204429098690189123879115250918411157078574724803297521729794244292694)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_425 : Polynomial.coeff recurrence4Scalar1Exceptional 425 = ((98130426631790425371349657990438266643500166 * 10 ^ 70 + 7210874139996085115985762916617276156028475217020490607292848796944918) * 10 ^ 70 + 3107838649581777583792446253737831228319215871517578074653817384640357) * 10 ^ 70 + 8930272626975819239016132542850503208796442190271886980097916273573770

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_426 : Polynomial.coeff recurrence4Scalar1Exceptional 426 = -(((17544280522269874746959822564310548520646990 * 10 ^ 70 + 2343732795418728105501824513982762773719542526922321004446901356679101) * 10 ^ 70 + 3664425409505030006123740021893242929929522231388612587250162486852776) * 10 ^ 70 + 3175857075796055973603061842823203447804106623976700543212643703155305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_427 : Polynomial.coeff recurrence4Scalar1Exceptional 427 = ((1760476512681980908293505311713157595739720 * 10 ^ 70 + 2868988006355432930506852340916067643745077167282394925612844553623586) * 10 ^ 70 + 6369948803113774121454766780443518629435269023072531397016317457729306) * 10 ^ 70 + 6551849481130553706259791648932789144041460562239035802282274473541042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_428 : Polynomial.coeff recurrence4Scalar1Exceptional 428 = ((311998602660962835503679879038921544757811 * 10 ^ 70 + 7512346708922026827807464230366377187478955961780880247626506705185660) * 10 ^ 70 + 6142432817921943534430534334586289032775121171608373509438720612092155) * 10 ^ 70 + 2648736066374528466364205153205740071808704199947561071118351764596562

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_429 : Polynomial.coeff recurrence4Scalar1Exceptional 429 = -(((250055658455685951887203719413842516817311 * 10 ^ 70 + 1031550544501815631229484513135813590714215776340932849763075571802896) * 10 ^ 70 + 2233773431770387207511727104379982108111607150772632620743043074190345) * 10 ^ 70 + 4171107440598502280681865001319594685664410633332621066605118679663406)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_430 : Polynomial.coeff recurrence4Scalar1Exceptional 430 = ((92149887619617942403256440563558603520164 * 10 ^ 70 + 3908953291948387253960676938777134763285361457997750401447816234750425) * 10 ^ 70 + 1494537025853793570481591050280878069069485194363905957428937221261920) * 10 ^ 70 + 6351332549742689864185775993376137323801839026911935691386211704227386

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_431 : Polynomial.coeff recurrence4Scalar1Exceptional 431 = -(((25619076018575652042899269163330090715828 * 10 ^ 70 + 8226019942446012644856702714957669068723016543213235982387533555950427) * 10 ^ 70 + 6580544263557858886188131283426992198090605277561276493205740693196049) * 10 ^ 70 + 4424441472051443059784493935872641349809268304659275089055278219046847)