Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_397 : Polynomial.coeff recurrence4Scalar2Exceptional 397 = -(((3192885366813986313802598147336904453929979801765887174785 * 10 ^ 70 + 5472793489728244499349093657184713169329913830436097756510950498795435) * 10 ^ 70 + 599969626298042599510638862083242584752714776398928789181576117276993) * 10 ^ 70 + 7264228366881399842329798398787818490033845718286831012223158366608334)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_398 : Polynomial.coeff recurrence4Scalar2Exceptional 398 = ((952473422660556608822935916166386149896691794169749514877 * 10 ^ 70 + 2833986708027015410960042424460942690136835149042422744046820803668421) * 10 ^ 70 + 5160297902154766818801526380072639849582355999917051869921620871940771) * 10 ^ 70 + 9549526496497782913786140607107673466826436954116602758893443008169405

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_399 : Polynomial.coeff recurrence4Scalar2Exceptional 399 = -(((266425874167535484271074149507131908677538135181822128629 * 10 ^ 70 + 5147207741670352574012193403057400121518453225364370934951162244362427) * 10 ^ 70 + 292454131711144301879912047552176986102639718801457113682532471363057) * 10 ^ 70 + 5736554343035092224587764655477315152506030864736692499767922821687377)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_400 : Polynomial.coeff recurrence4Scalar2Exceptional 400 = ((68304485842756418807805936206744458040574616161844523269 * 10 ^ 70 + 8469825478797076775994357281791225273688081838080493343793929929111725) * 10 ^ 70 + 8388271546226056198639028109460808737002269136642411454213575260476254) * 10 ^ 70 + 7497795517771776871248538953021534445514826731677749877080042920886710

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_401 : Polynomial.coeff recurrence4Scalar2Exceptional 401 = -(((15273832741607102307051046569169622223096298540409684335 * 10 ^ 70 + 856055509646942856810779406367398494241692435981948568542118519625873) * 10 ^ 70 + 3443163754285901035044282052134255918200614629849556438721308889354948) * 10 ^ 70 + 9227701618401125055383288989335397870626968018777493334151148184766358)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_402 : Polynomial.coeff recurrence4Scalar2Exceptional 402 = ((2565547937561171181632592247245124562307764111673707767 * 10 ^ 70 + 3616288335164613266831273308377761803877932029787226430820442151013742) * 10 ^ 70 + 1320795820053909749976141717380531611392999168463565629300398731554346) * 10 ^ 70 + 6424579024885912906632154588711174245861795291064463351841405661707889

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_403 : Polynomial.coeff recurrence4Scalar2Exceptional 403 = -(((68857434420540586574852289423121079689352831616301903 * 10 ^ 70 + 6413082533122974673482516505600858401716967456886791135364573154395252) * 10 ^ 70 + 3863601851256389742057316736218285179144822558406154691049920425807517) * 10 ^ 70 + 732160810319293844226864227197488754519279081884807032281204324425703)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_404 : Polynomial.coeff recurrence4Scalar2Exceptional 404 = -(((201514313387523038187819383213568637280749493674180870 * 10 ^ 70 + 7554678615335394404595679585101874597136993734619478987129640214354617) * 10 ^ 70 + 2945595497220537250019232082971795940505835733970514578549333806264608) * 10 ^ 70 + 7105358995541352667354776201236895870259305969705658839463431462103588)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_405 : Polynomial.coeff recurrence4Scalar2Exceptional 405 = ((124702692647284355985315073831802748390642830218622337 * 10 ^ 70 + 5621094580763171608939611905382046845143389243644233447834364568680139) * 10 ^ 70 + 5150415104888602635354335600198655345502252220575934786821447044725659) * 10 ^ 70 + 5984952699325720105711831391090963451755360432418779617766399211844134

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_406 : Polynomial.coeff recurrence4Scalar2Exceptional 406 = -(((54123837863119862991401682619652528169267297541983902 * 10 ^ 70 + 9617086228957565578307313780011260739295443202372661938879081201939701) * 10 ^ 70 + 7707089410021533540896693415287121689557583345948296388149621774841884) * 10 ^ 70 + 8358333503859218491152045735009653200683901061596682221220383332569440)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_407 : Polynomial.coeff recurrence4Scalar2Exceptional 407 = ((19996662371670540096277131897079738683439975418590520 * 10 ^ 70 + 2541503488934302916562603999244989550916633495481149140158048672745297) * 10 ^ 70 + 4764751385429489173875908374433449065065789554124919652768304878698103) * 10 ^ 70 + 2717283773918916300192691672220750341610520310081577397069792628306908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_408 : Polynomial.coeff recurrence4Scalar2Exceptional 408 = -(((6646842409273453836110590520950321602836879504671276 * 10 ^ 70 + 3724601409862304316492545303429717806865394240107284978175372233711661) * 10 ^ 70 + 4118062300938728444324243441225517423103040962480483126379983131436187) * 10 ^ 70 + 9616784713787778006818399563516367532375005676067050112996972984290314)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_409 : Polynomial.coeff recurrence4Scalar2Exceptional 409 = ((2030657767034710056267509129023967456556363596671428 * 10 ^ 70 + 7978997270093525634100729454756202057966401734433236338296876481234518) * 10 ^ 70 + 2330479561861322765132431829147612455340217615920927325588538276538681) * 10 ^ 70 + 5209872129500413500359693396118219584500125607455571886522894513565586

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_410 : Polynomial.coeff recurrence4Scalar2Exceptional 410 = -(((574468355517337702132075301023574601929119351861848 * 10 ^ 70 + 8780982888821508716781762000501209768283951167284451555776008395444969) * 10 ^ 70 + 2302279752400731869571610452235525853505304195604198437469471657490028) * 10 ^ 70 + 7173579099618262201950487191678869733513354927590215186978861444623199)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_411 : Polynomial.coeff recurrence4Scalar2Exceptional 411 = ((150272738580388936403341545270750329723648689576794 * 10 ^ 70 + 248051378787034517574681339277988259447060272873787528972516458746010) * 10 ^ 70 + 4954549610912390228619556160706369356792574919789805956348606564358925) * 10 ^ 70 + 898846394455645671237384166245366511253936288678783021924773347280632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_412 : Polynomial.coeff recurrence4Scalar2Exceptional 412 = -(((35939072972762811730063609078087338036737631678326 * 10 ^ 70 + 7889561690117506982151400716467362469437163920031130977638092057507751) * 10 ^ 70 + 4341277834454564383361157330069277269504367629693863199345930981653755) * 10 ^ 70 + 8970599037400074278067872464022587400932997116074790668874439385247623)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_413 : Polynomial.coeff recurrence4Scalar2Exceptional 413 = ((7628869539731953412620573159134944157308313556304 * 10 ^ 70 + 8917336324112652431165125045523925253956760472141058125865272614662522) * 10 ^ 70 + 5427427713420867789317050363943471812957453981577279271793098392537439) * 10 ^ 70 + 4312251248695448409133324197212448137401312935744415455978501506380453

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_414 : Polynomial.coeff recurrence4Scalar2Exceptional 414 = -(((1324134200034594566475420469952803698900918866031 * 10 ^ 70 + 4857712503972356254648083542475941784657247245063983457619913165176883) * 10 ^ 70 + 7280292008343504527064176578081595374853095803761012095911576262249092) * 10 ^ 70 + 7976697125287621014587090159036811672891035981314299886962533962574070)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_415 : Polynomial.coeff recurrence4Scalar2Exceptional 415 = ((129547994380375934383430475294028492795688007245 * 10 ^ 70 + 5116781431195289017120181237916215254683065535860669661041131971747795) * 10 ^ 70 + 4642177293877702892457394520678173274906868873062147181377251499940472) * 10 ^ 70 + 5830410123784306513442556477421730239500877108663515458846121314046336

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_416 : Polynomial.coeff recurrence4Scalar2Exceptional 416 = ((28799596927581098551311335526913059123755939841 * 10 ^ 70 + 5618737072391013067321469121404155696325785805356174792796471923173016) * 10 ^ 70 + 1058664598809338744084960026570115453811983103803819856004800795170888) * 10 ^ 70 + 8414980371623965504921789429212959102295465021863377505138142833801853

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_417 : Polynomial.coeff recurrence4Scalar2Exceptional 417 = -(((24019304639848969478980315951255748344610415115 * 10 ^ 70 + 5303731192486937623334339123504931250044711470113764729579769114996206) * 10 ^ 70 + 4082197826366773884386614137997331473280196335986812657590670289595010) * 10 ^ 70 + 9084327808530880766994442878494568418494436070293763378241183360005646)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_418 : Polynomial.coeff recurrence4Scalar2Exceptional 418 = ((10215663121202858636390052599130637094757346438 * 10 ^ 70 + 8659915772196377819121472709348308308277387040589104765730001930571404) * 10 ^ 70 + 3801502859395961254472999828103056778987802460427897179295186541866324) * 10 ^ 70 + 9471463441093704249190341120630906624620757278757456987087774999534665

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_419 : Polynomial.coeff recurrence4Scalar2Exceptional 419 = -(((3502281556683445030486244889255463890966819990 * 10 ^ 70 + 3437742582834118601330041708412869234906433071618928319697903122898744) * 10 ^ 70 + 8010102499526970441103852783679962466108957669630807324148175083272291) * 10 ^ 70 + 5055324430807282546103348938921402418775265583087217039310723588835111)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_420 : Polynomial.coeff recurrence4Scalar2Exceptional 420 = ((1059685936958712377281105280190366387836743062 * 10 ^ 70 + 4213639339656786849138796446219581725473010738779232811559906978337394) * 10 ^ 70 + 9777796013123267561310944411122820912611712826236014733790965322493608) * 10 ^ 70 + 8425295535224346116574969747505314525462404711397878204451315900490573

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_421 : Polynomial.coeff recurrence4Scalar2Exceptional 421 = -(((291731008339702161466731626308063472133253459 * 10 ^ 70 + 602517251204382276337303926002917171861367715779845975311025615837521) * 10 ^ 70 + 8315640016042348297118983700842866448159815030218715391361948689536581) * 10 ^ 70 + 8771476129378347006229380839804985420481866196245048988994469199436232)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_422 : Polynomial.coeff recurrence4Scalar2Exceptional 422 = ((73780956442930037182890233980530343464308965 * 10 ^ 70 + 7215872946013577414204564945734420785890599819998761139466034970792630) * 10 ^ 70 + 2029038668320427523851323536164944962508586163346397289856533812616975) * 10 ^ 70 + 2476864648473278716450199527289152830527594166467675702188624085030977