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_407 : Polynomial.coeff recurrence4Scalar0Main 407 = ((39028774421958086257447613305402562363529923473656765179 * 10 ^ 70 + 4717819444287517119273875871304931603483666237994911895662358897050456) * 10 ^ 70 + 2966536683375865917126897141274507816845728457414179544867700389288434) * 10 ^ 70 + 9617304643580144718759966840608981541383426225486636375001649617388760

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_408 : Polynomial.coeff recurrence4Scalar0Main 408 = -(((8964000261058307126814391453520881929125686327528402714 * 10 ^ 70 + 433736577371417607110130512497912502885711561015349355544119312740049) * 10 ^ 70 + 6986674250028602358808524925891020672007991545738226883483582101907924) * 10 ^ 70 + 8210134959414401237222455789949868076879970880375564161627280430223016)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_409 : Polynomial.coeff recurrence4Scalar0Main 409 = ((1664105749617563679345692817388426278861317635180332474 * 10 ^ 70 + 5223183527745265532970790202859475744504286553784179881836706859373295) * 10 ^ 70 + 7180808267949927500395633392713421705278327244426500169895776796547854) * 10 ^ 70 + 9772062451952125885670839704833400477976634267729471746486932830270639

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_410 : Polynomial.coeff recurrence4Scalar0Main 410 = -(((149766556825941774997446865007795969487330758343819882 * 10 ^ 70 + 8393514558232241373795213335129257808228192422442477924402137395305950) * 10 ^ 70 + 370142688291043762772643035382730186571613805169924230546321905929153) * 10 ^ 70 + 590403399124698571091908722964806146178760555301703727978273518367862)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_411 : Polynomial.coeff recurrence4Scalar0Main 411 = -(((66262157431271441714949054837034886104856982619563906 * 10 ^ 70 + 634853284390129909581563235414197582129900068965387895023808974716969) * 10 ^ 70 + 7088662026706078074745746751506475280440069301967240814417153178410814) * 10 ^ 70 + 5470753527703393426480720602328110468670666310916021584472921316793375)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_412 : Polynomial.coeff recurrence4Scalar0Main 412 = ((53419725886863333182127774784029864201238870142352609 * 10 ^ 70 + 2636893815480644026176058562971553286972780167302628973048705177865884) * 10 ^ 70 + 6951976009358705066068787935173122138791494159419170668915709383994235) * 10 ^ 70 + 7111950555600106190237536511168133094295191804464153639499792769772117

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_413 : Polynomial.coeff recurrence4Scalar0Main 413 = -(((25780421242230113773126411839471571308646658403032341 * 10 ^ 70 + 8674926280183950162075348516620252997484102013216279523817411329918695) * 10 ^ 70 + 2397672490882085854097646020394206163631001651764695393376039077080717) * 10 ^ 70 + 5158193232759738101353857290759833759189333842276447917024505953728470)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_414 : Polynomial.coeff recurrence4Scalar0Main 414 = ((10536567011851746759490292540017339976873118530218575 * 10 ^ 70 + 8004463024722578799878861378354597179829379480925353041527206648534729) * 10 ^ 70 + 3988446924069976612363024014650298397345403063104838812628600062082390) * 10 ^ 70 + 8216090157115719214666462199729325502553612101172056049775206040597426

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_415 : Polynomial.coeff recurrence4Scalar0Main 415 = -(((3985712011209159602504400317492107263498356151836432 * 10 ^ 70 + 5084764580286017492401055985654942188451916200056303897068099429496926) * 10 ^ 70 + 6396143382312943721442330633112940973036567722501004047574026157027642) * 10 ^ 70 + 6137764404336625536018874478581352318152389228749747756466334143555188)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_416 : Polynomial.coeff recurrence4Scalar0Main 416 = ((1455100091694705043064632848644975946483126750572407 * 10 ^ 70 + 7565954285931512047561466084703823317133946247592113074980645733997699) * 10 ^ 70 + 4422388651194374695368927950268556275627910528707463014912342193415422) * 10 ^ 70 + 2422481197425969903615435795405902353052540399332379396040988069007218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_417 : Polynomial.coeff recurrence4Scalar0Main 417 = -(((525977390856231324355255278547020923453805550624567 * 10 ^ 70 + 1949377633970301217648566502178383482793838652346113266241565637904493) * 10 ^ 70 + 8573679867631787196443135432945961657766721119994163035655537483057080) * 10 ^ 70 + 1437621549762250183488344016676268772541641083700598229748331358622370)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_418 : Polynomial.coeff recurrence4Scalar0Main 418 = ((191211412250795511278606702078965615806358673643833 * 10 ^ 70 + 3574727596352945828987329315700544060499170202055177222553470913543579) * 10 ^ 70 + 7455832949367272988446527945280426623496799790630851515866122920676644) * 10 ^ 70 + 7421282706140835953248160791451925336039324392076349228207426594562229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_419 : Polynomial.coeff recurrence4Scalar0Main 419 = -(((70363746421758527469968178473815901355108999851794 * 10 ^ 70 + 9416031084215757641713418078420700741773602921479899907025937935741827) * 10 ^ 70 + 9792701363248302124887721156521158054038932489478651431687585247589329) * 10 ^ 70 + 8660132052227174649784690573521793631194841950934992998728837487241399)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_420 : Polynomial.coeff recurrence4Scalar0Main 420 = ((26163713042925444761577881011699115233064806994716 * 10 ^ 70 + 5068112850517025373001600116124870488130880788335697498902852356516919) * 10 ^ 70 + 2359525842746192148004355946917666866137819767267054233595097814126532) * 10 ^ 70 + 5097136540065829206313792036864752550643804106544815049766386468825587

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_421 : Polynomial.coeff recurrence4Scalar0Main 421 = -(((9757381443667367115622212174658304635653849929879 * 10 ^ 70 + 1684723427897673083357832867400036484842257216625948993531023188661150) * 10 ^ 70 + 8523528059835672892183562717834137724028377589796400541246215591341996) * 10 ^ 70 + 9861109159079349775730884760568029332668859363077323963101371667532833)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_422 : Polynomial.coeff recurrence4Scalar0Main 422 = ((3614426947826234855478514470800623747755515664446 * 10 ^ 70 + 3695339767926189585859838436181468024438574643586033385727776182418547) * 10 ^ 70 + 4322686637137014693174656487073397378046075415816890968385333002115595) * 10 ^ 70 + 1346695160531283546847366723834877280707743405714544527079921064198072

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_423 : Polynomial.coeff recurrence4Scalar0Main 423 = -(((1317582642581352336706809077840773243065691868723 * 10 ^ 70 + 6967799492645166644350484409956519399838133362265087681530666535351606) * 10 ^ 70 + 3667881395789481138032552219055356929243772845489449883010884120440464) * 10 ^ 70 + 9823786636865074445951210597571094556432014481963143445876417711042966)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_424 : Polynomial.coeff recurrence4Scalar0Main 424 = ((469059728667898532284110088785540718768664452114 * 10 ^ 70 + 6425427178386737796077704950323028945528545035840896015600590714250170) * 10 ^ 70 + 4963688608869876012067918049093049875686956402235998216140131967321857) * 10 ^ 70 + 9050972416556599088334614223570201239569551316079104652825033343785925

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_425 : Polynomial.coeff recurrence4Scalar0Main 425 = -(((162130963067281793214767689752266189646864678270 * 10 ^ 70 + 8964334058846000072548488902472748533866853519927279938223787730901585) * 10 ^ 70 + 7075585953015604247885982692961057847389068216730557333971558680316219) * 10 ^ 70 + 141375116279317720367748680625390857266420216915261045823008762788841)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_426 : Polynomial.coeff recurrence4Scalar0Main 426 = ((54175655122976800490553103256182536723603295231 * 10 ^ 70 + 9814773003257205508488635164290569738825487530418616158474518519250181) * 10 ^ 70 + 6434181988621719772319453217526207539633942866005267191759401008013853) * 10 ^ 70 + 5532145188404631516253188613247994284855007642901469942498274021831021

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_427 : Polynomial.coeff recurrence4Scalar0Main 427 = -(((17440698784760007761553205299190814672040177492 * 10 ^ 70 + 3456272065844068908366944992985466472650095943164276515862835841840176) * 10 ^ 70 + 4587469211633135607124479719079930996658260757541883834571543743357877) * 10 ^ 70 + 9987043516317178573068002830348529492662774373133304376276546808943816)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_428 : Polynomial.coeff recurrence4Scalar0Main 428 = ((5393194851914787178055987405736056812027818934 * 10 ^ 70 + 3958471973260407878204636049556633830287581541547553723202509739871407) * 10 ^ 70 + 5767537236545052927222678255767170783364448956291730221423409767251964) * 10 ^ 70 + 2783701203132059738026578902690244615959525128635046228507268960527890

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_429 : Polynomial.coeff recurrence4Scalar0Main 429 = -(((1597028065772894563585510360903736841107353007 * 10 ^ 70 + 2578856083654423449074527476627030673313544634314563522041516456329165) * 10 ^ 70 + 7971382788434468712902342104636602792886857800388490901477114482581911) * 10 ^ 70 + 4201302094665362228987501237395819621855733425713245947187384834909100)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_430 : Polynomial.coeff recurrence4Scalar0Main 430 = ((451177092138232813893939665755757882444255967 * 10 ^ 70 + 6263477536324367909698094912547833008959099365608103639482317573947257) * 10 ^ 70 + 417846630175521606419987525924224708560059948052312318737498847396712) * 10 ^ 70 + 4903345003449263132529922940478865449295527333667864232227486073033319