Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_53 : Polynomial.coeff recurrence4Scalar1First 53 = -((82019141965530252337079200218 * 10 ^ 70 + 5753444227494031017111681302380043194229702198460006282250709148283791) * 10 ^ 70 + 4345830362753023998651626828719651596329213114302698972352572287396025)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_54 : Polynomial.coeff recurrence4Scalar1First 54 = (4868870066082564554392103579642 * 10 ^ 70 + 9162161440338152094522344051744403453564966713881245863012481367406602) * 10 ^ 70 + 1292055748265672132565891662679388473534564399393298928039508536464211

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_55 : Polynomial.coeff recurrence4Scalar1First 55 = -((271341950433496254794130346203458 * 10 ^ 70 + 5677688511974497476455181941978192113164453158197463040030938165120678) * 10 ^ 70 + 4576783361835287118906803381207365453799220716670483399985456410980810)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_56 : Polynomial.coeff recurrence4Scalar1First 56 = (14233488044171350023814728976878643 * 10 ^ 70 + 3932491679962014964975610296938004135354273374106320527002001787959091) * 10 ^ 70 + 7342964032881466353550401566903551136852204011190788703785934980651134

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_57 : Polynomial.coeff recurrence4Scalar1First 57 = -((704255848120719549708245280547943750 * 10 ^ 70 + 7041031012077407673946760159672095561417091411243372351959552646954346) * 10 ^ 70 + 561966629959602075202792687438719504231902495973900673532174785414870)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_58 : Polynomial.coeff recurrence4Scalar1First 58 = (32925479330612476101073421170774030236 * 10 ^ 70 + 5020967402673335194498762621305257769385738833296139759214987498276272) * 10 ^ 70 + 1638627658550976516439560709959422008560780550528331549141293320714491

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_59 : Polynomial.coeff recurrence4Scalar1First 59 = -((1456614432830485358782441899432279337348 * 10 ^ 70 + 3360809267704365334310411509295666726751420288586656221164571676271613) * 10 ^ 70 + 1324994388864495467707623327556524338843319216216951238927318390519633)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_60 : Polynomial.coeff recurrence4Scalar1First 60 = (61050205869046819859047887849406315164484 * 10 ^ 70 + 7498812713158769739848621018882042185919530568397569119895511155808567) * 10 ^ 70 + 9162159225106763301219944124326301964303317874827823320086405891196568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_61 : Polynomial.coeff recurrence4Scalar1First 61 = -((2426508688202274818026059573091301398600015 * 10 ^ 70 + 1567242512764432790059256273438705530395574046080082139981915732019362) * 10 ^ 70 + 5828631463177495873237636268902304415704000645425119405386366197952914)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_62 : Polynomial.coeff recurrence4Scalar1First 62 = (91529237251496654126943374124820992132874857 * 10 ^ 70 + 7010171532639625675554798975693588753244107531248267680923282001996705) * 10 ^ 70 + 5233585213593121590103369321155191497616084501934964384552760114729032

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_63 : Polynomial.coeff recurrence4Scalar1First 63 = -((3278396551477928720836907218867715763287572991 * 10 ^ 70 + 776794920319790851997196007216484515816833509624712601950099980011254) * 10 ^ 70 + 7168474721853157871497246434786423452163613752547826917189555383732967)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_64 : Polynomial.coeff recurrence4Scalar1First 64 = (111540154170718967800665690541947778793160038702 * 10 ^ 70 + 1917426567976168371465865699205880143720368609085535788920064000034720) * 10 ^ 70 + 3565605183055618338254680279540389317037520586436416509349891898568230

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_65 : Polynomial.coeff recurrence4Scalar1First 65 = -((3605005618467234877644250807567220978294089312871 * 10 ^ 70 + 6499543053694892530625056107797581313051444221779099038869207535643767) * 10 ^ 70 + 9411003363972129171559485300193940734620679687785277569171095402358920)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_66 : Polynomial.coeff recurrence4Scalar1First 66 = (110660967987557837438809334228734541660778285570615 * 10 ^ 70 + 1158275652533295817210687479942692983728368778494389725034979414048137) * 10 ^ 70 + 6694017654068481931908374708845725193240103971017801509103118799658689

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_67 : Polynomial.coeff recurrence4Scalar1First 67 = -((3224369931398306705944713985408918363329849009894133 * 10 ^ 70 + 9072017318429225628044319047621431709602835434869696883150642630385876) * 10 ^ 70 + 7472684654821779743730829314966792857516515188288200104270009075890040)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_68 : Polynomial.coeff recurrence4Scalar1First 68 = (89082429182050306748296524541788698739119817480271722 * 10 ^ 70 + 3307339534139813578038728301596602568606875055617968220417462858360816) * 10 ^ 70 + 1362486343890168293995595018417163893378386989053437553145421727289666

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_69 : Polynomial.coeff recurrence4Scalar1First 69 = -((2329554432896641711060551989601623916776396898381091680 * 10 ^ 70 + 5310673359770287722920422588873487796073550080318954460608068363194077) * 10 ^ 70 + 3577870352162845989141093169054947486143296026069804235923212389530593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_70 : Polynomial.coeff recurrence4Scalar1First 70 = (57502024660798516002129440787141311519269309587797442773 * 10 ^ 70 + 6141717202966483294358794273201621857200051759213076951248690814210294) * 10 ^ 70 + 6474073891880680052786469205531353779185200436377813834263620257900561

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_71 : Polynomial.coeff recurrence4Scalar1First 71 = -((1333901674616572059670629319725539649087891714650949473739 * 10 ^ 70 + 5346737852704682770818553862186970983202974675433980433111222866569817) * 10 ^ 70 + 9135166525292526378639756575388068864138835677809853741389437230517452)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_72 : Polynomial.coeff recurrence4Scalar1First 72 = (28874536473770671042695480000878099721495943971220184944511 * 10 ^ 70 + 4808094647679856865025953055208342376733584733032756952923793038264065) * 10 ^ 70 + 6656721380978574271669002686750898443543718736167497275915914107367072

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_73 : Polynomial.coeff recurrence4Scalar1First 73 = -((576190874957171326273903367649222229966767901582971153884594 * 10 ^ 70 + 1264598887673668146952055306070965636678625399276696708604748991155116) * 10 ^ 70 + 6624024758941406032702610091251236238655616910009208190089133993213620)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_74 : Polynomial.coeff recurrence4Scalar1First 74 = (10357508882927470977247841124849604465279752497587798823475242 * 10 ^ 70 + 2027384729122622932011388181803780708583422222086625246961522957994262) * 10 ^ 70 + 8338564773227293637514548613308997240897696681432812926232149829024672

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_75 : Polynomial.coeff recurrence4Scalar1First 75 = -((159257960827717462658343525173839207081539728885448297279818507 * 10 ^ 70 + 5043183306405330621841796762738884804007117288309801772935610531078741) * 10 ^ 70 + 9917818009450464337115503999975545362916123141783800371086789056245809)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_76 : Polynomial.coeff recurrence4Scalar1First 76 = (1779915042477942228792857699116574637963372292785382448093133524 * 10 ^ 70 + 4114845108751269126923818150459752161650965242113448630098592565397752) * 10 ^ 70 + 4160696949493216977818047648150669600923219725994855939459016238772539

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_77 : Polynomial.coeff recurrence4Scalar1First 77 = -((1091717266450193088764746347576566771089642439066674177780406435 * 10 ^ 70 + 1602780169457588579296295384595879337459495102612372614536954519732544) * 10 ^ 70 + 2458627630091074421607088842817290330506570339831691104803604651448513)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_78 : Polynomial.coeff recurrence4Scalar1First 78 = -((718097993411383408076529138587034401309812312588817136766696019005 * 10 ^ 70 + 745953497047374325523586909831265527004071996870832342536024995772246) * 10 ^ 70 + 8048845968142624047390151179130675377378635826781815573012300978112326)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_79 : Polynomial.coeff recurrence4Scalar1First 79 = (28307662131817233077434265928159122809816591364332028157327625903350 * 10 ^ 70 + 3613099142754596630845867003416674419717912365311073062829319147805257) * 10 ^ 70 + 2936905001160446505121834241890485787530812507695613552908788926534821

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_80 : Polynomial.coeff recurrence4Scalar1First 80 = -((792244276221691704011136233598895152142202015337608286032042984192610 * 10 ^ 70 + 8264793282424978065635393458867923300575975526558879754019575650415434) * 10 ^ 70 + 4741121721653767709769643323138385503289183356605141711923771609694727)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_81 : Polynomial.coeff recurrence4Scalar1First 81 = ((1 * 10 ^ 70 + 8756485919943475432923783454651594021004946319654329759405825169376928) * 10 ^ 70 + 4204044520621267592099833555738226093908482866685123352904985736281406) * 10 ^ 70 + 9646531324106638837896943682840559193910673008671013425916347189850337

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_82 : Polynomial.coeff recurrence4Scalar1First 82 = -(((39 * 10 ^ 70 + 5348761784272809510934614836343154065521074234327588538668103550793670) * 10 ^ 70 + 9920228337091365632280302235839291631519102084206237691298876614221559) * 10 ^ 70 + 4163118910592510025777158501591042405651739076090301235012818574917899)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_83 : Polynomial.coeff recurrence4Scalar1First 83 = ((755 * 10 ^ 70 + 7053976512561438402727051841832177039518220531238694683344348618801121) * 10 ^ 70 + 417862515513639828437941825100236233138787087541666943003332568409442) * 10 ^ 70 + 6029957507697886001897642093467837245907402751845163907687852232758367

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_84 : Polynomial.coeff recurrence4Scalar1First 84 = -(((13141 * 10 ^ 70 + 8883040949561792561410122192321304144373770572914867085884655850283803) * 10 ^ 70 + 3935341962535493194201831989720370824704561510969759092272522233047448) * 10 ^ 70 + 8017486660673226427570654005530084027749822723662559749014440314944283)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_85 : Polynomial.coeff recurrence4Scalar1First 85 = ((205867 * 10 ^ 70 + 3912425966333428342699637827579647137710311843233849616495055394770681) * 10 ^ 70 + 6571951093039971073196544073629724162022492401545168166485045691745709) * 10 ^ 70 + 6424824545145421518951115839182930437069178919921251530350254305954234

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_86 : Polynomial.coeff recurrence4Scalar1First 86 = -(((2814108 * 10 ^ 70 + 666252309643372228020190314238471821050964992253935112155419894561197) * 10 ^ 70 + 6256166508018472087915931190926983392434212655076820797820338924157084) * 10 ^ 70 + 2504163396426857350551693669690835385721047163382482640133985088659350)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_87 : Polynomial.coeff recurrence4Scalar1First 87 = ((30516902 * 10 ^ 70 + 8479523951159509493073493537953267186007059674501269796072098156404275) * 10 ^ 70 + 8922961987602531449906608629075328629564718372794068332765247729356928) * 10 ^ 70 + 598861953270171572707514432100364819579837429777386165318651759964713

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_88 : Polynomial.coeff recurrence4Scalar1First 88 = -(((158013209 * 10 ^ 70 + 4834636415599654238798368367798037141361446622147746329033645866454328) * 10 ^ 70 + 2567495165262071374689864121033280564286810243010203127719886041588494) * 10 ^ 70 + 4760143333400843929456734496227657514784715761329454554038135559504690)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_89 : Polynomial.coeff recurrence4Scalar1First 89 = -(((3905340792 * 10 ^ 70 + 1107451539323184468152618376264330130039481816954779028066534971394253) * 10 ^ 70 + 5982769410388421724623054064250432472295497363567762431756884953708905) * 10 ^ 70 + 7349123246730419117141176786184305789190011101015182519210980090757177)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_90 : Polynomial.coeff recurrence4Scalar1First 90 = ((174173574157 * 10 ^ 70 + 7340211047549187189004366108599300666756665780580072747624381524303056) * 10 ^ 70 + 5834504675295748168244927221587658904116509594470943695902493407791817) * 10 ^ 70 + 3628372507257366154678270276877857789194367078136028059562227849723120

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_91 : Polynomial.coeff recurrence4Scalar1First 91 = -(((4537350519159 * 10 ^ 70 + 6507789569261842268531577390959851146454821528913465365659063259272297) * 10 ^ 70 + 7248503848920863063619762528067331823769310379869790019296612855440794) * 10 ^ 70 + 3165577597992377841148885275704131385081815447270249106883970151918168)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_92 : Polynomial.coeff recurrence4Scalar1First 92 = ((97296829658765 * 10 ^ 70 + 6389598356142480048509029672242416762466748558472745443682686441095928) * 10 ^ 70 + 3457546374661647548175556118810275809822264207625827206930552227516035) * 10 ^ 70 + 689837908975757826342084101668593401566733028613988310834339477996064

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_93 : Polynomial.coeff recurrence4Scalar1First 93 = -(((1863537184086566 * 10 ^ 70 + 2839666133780505989661094269695182505469786204946860584205683074103194) * 10 ^ 70 + 5400801058200702284100993265003561739991802078902483185764260672758120) * 10 ^ 70 + 1124366373936120581370192551141735061017537038514292505642647174450073)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_94 : Polynomial.coeff recurrence4Scalar1First 94 = ((32950586362758966 * 10 ^ 70 + 4946670358841852839500793586448888311105472392676456343535852508004319) * 10 ^ 70 + 2890233176193247856178590074518922912029528962239036345151318689215133) * 10 ^ 70 + 5293918115739390608937367914577743199941072588074512486497667108662829

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_95 : Polynomial.coeff recurrence4Scalar1First 95 = -(((547028759822439168 * 10 ^ 70 + 8431470849708890984391214131027939541063891974046216249351292407564531) * 10 ^ 70 + 3508889013039188984172449663509002516224039053260149296453688919083944) * 10 ^ 70 + 16051116159033015648965197315468591174342494600117008780848234956711)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_96 : Polynomial.coeff recurrence4Scalar1First 96 = ((8611823282704705050 * 10 ^ 70 + 1869499277446785642165410405942539370959356494421118714678131643652534) * 10 ^ 70 + 9499754229203941109810571003001490354313413985000764004239179803453118) * 10 ^ 70 + 2718130002077592607980158210788138172671807911813274288256618994268629