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_74 : Polynomial.coeff recurrence4Scalar1Exceptional 74 = (2153854489503717871747232638473525668244165669831963216297005 * 10 ^ 70 + 4740497854975338863096777555190180879168139357008269424415977067104536) * 10 ^ 70 + 9420256171049947402730872491802000625979069230305883945061463896455690

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_75 : Polynomial.coeff recurrence4Scalar1Exceptional 75 = -((49207332985777639094700563350488579862134787692687718248436777 * 10 ^ 70 + 8342246022011153269016473485833911021411546439803527975678337326031688) * 10 ^ 70 + 6450202324385656941539249764594685328393517635539940703522977657344640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_76 : Polynomial.coeff recurrence4Scalar1Exceptional 76 = (1086086961053625366866546011747553822951490730098402521940418308 * 10 ^ 70 + 9410727072290350380486189123777304961200379510026533629334458211020215) * 10 ^ 70 + 6172581205190180973947804200631159753979029362889502986408452915865361

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_77 : Polynomial.coeff recurrence4Scalar1Exceptional 77 = -((23167392415388783588576570524561592584461555039405463010524643260 * 10 ^ 70 + 9358521665748478453689858758955741634381753148204260577407968293509581) * 10 ^ 70 + 6274057012870440678787161812691067168108970573528862480084816217408813)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_78 : Polynomial.coeff recurrence4Scalar1Exceptional 78 = (477768175063221097022696741601085456064235474754239873393243179865 * 10 ^ 70 + 6568658883260858351241217411233115988583509813116890428232041703093806) * 10 ^ 70 + 4655801343587877323504868579417330483457011182063740334650122660511047

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_79 : Polynomial.coeff recurrence4Scalar1Exceptional 79 = -((9528569795960183673953377618225501685970210941370692231204840977401 * 10 ^ 70 + 3298695152234953012230564286499844728177280842206489805619481973759480) * 10 ^ 70 + 2297536182716813511284044602850452701249907571327800425062895184978354)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_80 : Polynomial.coeff recurrence4Scalar1Exceptional 80 = (183841994408059686749042324496164601310979860869174322159613186533816 * 10 ^ 70 + 8787682183322454592721306354081217200428215765401957350222970634070845) * 10 ^ 70 + 8875666666999125323849127677764294001425838011444570038185007920148531

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_81 : Polynomial.coeff recurrence4Scalar1Exceptional 81 = -((3432395277055997060516660475643114632119583262582325257856270612603423 * 10 ^ 70 + 1203887318998573064117418295525945340254822428787230370546737957040649) * 10 ^ 70 + 1305477831056360632500417514426863432480262680019858158736851538681588)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_82 : Polynomial.coeff recurrence4Scalar1Exceptional 82 = ((6 * 10 ^ 70 + 2030794579764171073914816161082662680717885252246268186087557366694274) * 10 ^ 70 + 814086477946576582798157894646826972730904255395065991469696217465085) * 10 ^ 70 + 480737683973012630029229404170021179914622180983601436703638933477647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_83 : Polynomial.coeff recurrence4Scalar1Exceptional 83 = -(((108 * 10 ^ 70 + 5398927254607172954363749344622796990584068866595269297114196462558609) * 10 ^ 70 + 1817130291629595962388412663791157281381707018841681967949041753669896) * 10 ^ 70 + 5311622924832791558865763149893636098591093519987948214798028582173898)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_84 : Polynomial.coeff recurrence4Scalar1Exceptional 84 = ((1839 * 10 ^ 70 + 2902684566220390113084925004078654723618178379665030948767983586928919) * 10 ^ 70 + 794048959576880587556124286708230958707805148192568028298369286546868) * 10 ^ 70 + 4474112249065995473189890736046145738478089525744661851172599574366915

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_85 : Polynomial.coeff recurrence4Scalar1Exceptional 85 = -(((30191 * 10 ^ 70 + 7865133678030896068176912712768156903470166044770001850741037073278728) * 10 ^ 70 + 9406908878654995614928599811346326946935893350196891195004221411382327) * 10 ^ 70 + 8365338366890770108750065970191949910721727333287645797642541651682441)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_86 : Polynomial.coeff recurrence4Scalar1Exceptional 86 = ((480170 * 10 ^ 70 + 3481052295094473262056068447822338027575663592801386259906714161646974) * 10 ^ 70 + 6097227386890747739952147019457730317746767274005889684378976051032337) * 10 ^ 70 + 6922836895964110234801426717163425926227226882419553346046154346652859

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_87 : Polynomial.coeff recurrence4Scalar1Exceptional 87 = -(((7400331 * 10 ^ 70 + 1628676763739597905860225570943235097822455209446372440991440554309666) * 10 ^ 70 + 2167949725947534342433202553394194199808223482895291121910919810411687) * 10 ^ 70 + 4067763751160760431052259466140753128550549151424608337740686136091643)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_88 : Polynomial.coeff recurrence4Scalar1Exceptional 88 = ((110542139 * 10 ^ 70 + 9458747314597807855713349457735611036180273623656595151019694946729697) * 10 ^ 70 + 4953298368313389741940707429871337524074444351503822675096258097735517) * 10 ^ 70 + 9231610169448024995717365469785217928130644646239575704849710396438804

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_89 : Polynomial.coeff recurrence4Scalar1Exceptional 89 = -(((1600613807 * 10 ^ 70 + 8612714422173622469751592520485594561213880008145992065317812586999792) * 10 ^ 70 + 3257082392385331609936180376773788638433097612561963626224368092413948) * 10 ^ 70 + 6218031772606213434880125424919998038657825565582604520950462599391953)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_90 : Polynomial.coeff recurrence4Scalar1Exceptional 90 = ((22468639907 * 10 ^ 70 + 9302457152183150573542112940590592474486722285261429121648405470768896) * 10 ^ 70 + 533780892127830726738901074313072287417101523056111074058519081487774) * 10 ^ 70 + 622120415246931327339486484784224040854021803496546471320174870879296

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_91 : Polynomial.coeff recurrence4Scalar1Exceptional 91 = -(((305798490272 * 10 ^ 70 + 6780223230346924748038181036431362261331140574288836676876146877772438) * 10 ^ 70 + 3023982606335513362835904744419608420998676506076527033308463074825811) * 10 ^ 70 + 395097115189786275154563458221181385554127248054385404908261358929933)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_92 : Polynomial.coeff recurrence4Scalar1Exceptional 92 = ((4035382726181 * 10 ^ 70 + 2525065657485447281066781316648013504375183672946800122506627583989686) * 10 ^ 70 + 9780669236330813455287349177459909353459919454358562466688281035926634) * 10 ^ 70 + 4879741181249288494942716085066201234882541215282351924726455817723038

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_93 : Polynomial.coeff recurrence4Scalar1Exceptional 93 = -(((51633470091501 * 10 ^ 70 + 4163864765387126794695537171184162531961681664869128421474430557553431) * 10 ^ 70 + 4269024178742872114590376974421779616931124457190664838068211940892397) * 10 ^ 70 + 5946046697012166180596078327839828565496295497139036339951242603015961)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_94 : Polynomial.coeff recurrence4Scalar1Exceptional 94 = ((640564575894406 * 10 ^ 70 + 6782214614895157124788889895103934007425754724925404911583648683803388) * 10 ^ 70 + 8800426768847563331688128966288600082156821995705504373826764361878666) * 10 ^ 70 + 3381828924576788995006814983708542528669276655497588840735555747710241

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_95 : Polynomial.coeff recurrence4Scalar1Exceptional 95 = -(((7704525607672254 * 10 ^ 70 + 6377102393618298234014239314071264367337675946088623395340862864318624) * 10 ^ 70 + 1056565325191254074413602576273203339371862287885928904319595979638928) * 10 ^ 70 + 8560097585526847977097692482399351102747612049698716845541291872679371)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_96 : Polynomial.coeff recurrence4Scalar1Exceptional 96 = ((89829998194692079 * 10 ^ 70 + 2591311315394804963183410420304172467102990011217579836241627915702788) * 10 ^ 70 + 4719473906532899115105222416151396613244984686849526974710575002166091) * 10 ^ 70 + 5889426320703033993362553262203289084070290452231841823398231100410107

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_97 : Polynomial.coeff recurrence4Scalar1Exceptional 97 = -(((1015080369158560901 * 10 ^ 70 + 8398670211405947498335290583550623178285775942778871681954735174585414) * 10 ^ 70 + 8370480504402095520852105012455125771068120212969428689343947000640209) * 10 ^ 70 + 6418380542813111056948771106465115486461489716944488544726305797831686)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_98 : Polynomial.coeff recurrence4Scalar1Exceptional 98 = ((11113674684217160613 * 10 ^ 70 + 4355575271353970033061668789767295946151644176029135739846496794785813) * 10 ^ 70 + 9865091790301026589174378597963164759569501764576307405792570648276225) * 10 ^ 70 + 2299081521656990254759665261926168731896476278143608566810581166021097

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_99 : Polynomial.coeff recurrence4Scalar1Exceptional 99 = -(((117848232147266113379 * 10 ^ 70 + 2440854809096582343282255737825392422107494504245052481273293924134295) * 10 ^ 70 + 7516133886386408386877273776783265151818058180274193072910128423091185) * 10 ^ 70 + 8160490391853686335933383334410360010540854424504994833152698836428053)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_100 : Polynomial.coeff recurrence4Scalar1Exceptional 100 = ((1209680122194384029297 * 10 ^ 70 + 8234613592574534168775557079805128950998953216457365439568108611069558) * 10 ^ 70 + 349100119824110888824299901760808759230473362275947871953142084991653) * 10 ^ 70 + 5180579674336050703870882185269467780354253205834146040487633035409553

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_101 : Polynomial.coeff recurrence4Scalar1Exceptional 101 = -(((12011647485429882340036 * 10 ^ 70 + 638960220570374485735411825785162943685517762165377665153403294960185) * 10 ^ 70 + 2751030910803647313658596649417799814282016378133014856700900510375926) * 10 ^ 70 + 1047314881242864453017568060410466387602832078918046933365941269490118)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_102 : Polynomial.coeff recurrence4Scalar1Exceptional 102 = ((115273220130587653241113 * 10 ^ 70 + 7473171570592912578743134332908147109815104335454834193296412633286946) * 10 ^ 70 + 214547256496933059816382478174330116202972859105394769010896100868424) * 10 ^ 70 + 7624406750239458958398518011863460511547621325951403852835924287423290

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_103 : Polynomial.coeff recurrence4Scalar1Exceptional 103 = -(((1067905012703344693207608 * 10 ^ 70 + 4144688872470461161745191565536012880034684584294468059105304169438195) * 10 ^ 70 + 3829158253567179698248920657403338127771564159571035080208911334490286) * 10 ^ 70 + 7392517947002521856018628432757761807420769860950932110678603669459599)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_104 : Polynomial.coeff recurrence4Scalar1Exceptional 104 = ((9535160504462443727289298 * 10 ^ 70 + 8441391677287949275121296604311833021914541271157444526663323353349506) * 10 ^ 70 + 2815125496028483304675747605710497810069115168265897901314145538449942) * 10 ^ 70 + 3214393112731360881310554233219670772956565106299382470098218711627752

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_105 : Polynomial.coeff recurrence4Scalar1Exceptional 105 = -(((81880942058378537660119368 * 10 ^ 70 + 956071935748518402670480593392960682169021381560232768498712717070802) * 10 ^ 70 + 2186647696139776872366490232764487492591222924723087817685508248154712) * 10 ^ 70 + 8035452595531739674541284207602981303189805804634749074781066231606261)