Recurrence 4 lookup certificate: A4Square 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.recurrence4A4Square_coeff_121 : Polynomial.coeff recurrence4A4Square 121 = -((116009269042441852720328432731476135236176 * 10 ^ 70 + 9722719309355879984668302983697821006022387342978247760207247048269878) * 10 ^ 70 + 7372325851057002018304042295554807247792795672751983555784046136972640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_122 : Polynomial.coeff recurrence4A4Square 122 = (366997656242311311811704556721613110340491 * 10 ^ 70 + 5022573584107096745970358618095891368778573763311789277948064030036889) * 10 ^ 70 + 6712827239850517648891740575056165015765889040762627528438671609160846

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_123 : Polynomial.coeff recurrence4A4Square 123 = -((1137609190715598051702148969578334268181821 * 10 ^ 70 + 3173805012108829450530100543396333649157315403844861909173058133982972) * 10 ^ 70 + 6558408467297319629647858919278954002126224224556491510208703853337126)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_124 : Polynomial.coeff recurrence4A4Square 124 = (3455670413405688074530237671156686260051269 * 10 ^ 70 + 5943309364065925794097253963019569079717264138997275246700898822651108) * 10 ^ 70 + 2304936569226453739743859041672289823769056688575064890227544715629272

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_125 : Polynomial.coeff recurrence4A4Square 125 = -((10287972858233739962584954620877398331027236 * 10 ^ 70 + 4123502461168793824050558328968271156926032624535055333918817651173165) * 10 ^ 70 + 9468628305170761053883440545702287271611532696767733346114955173131730)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_126 : Polynomial.coeff recurrence4A4Square 126 = (30021548367210151162878443578298128337615855 * 10 ^ 70 + 1967483514366229133127123569764929337139834910104436077196153038840917) * 10 ^ 70 + 3801333566053970953527576527857419251015896123367562523180103613321816

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_127 : Polynomial.coeff recurrence4A4Square 127 = -((85879269676727458762588286581004881497068832 * 10 ^ 70 + 6684918244634158534931459260396443783877048297140098010994877945868938) * 10 ^ 70 + 9039339880816718410428318962428071823156304992628989870109126638183600)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_128 : Polynomial.coeff recurrence4A4Square 128 = (240846579165004518527851426370427938370466660 * 10 ^ 70 + 3384477249335635765348939134753525889378235029464635427769602222349101) * 10 ^ 70 + 4242543411091847857818677283264552372530681081702132632103781408039041

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_129 : Polynomial.coeff recurrence4A4Square 129 = -((662267052792101979415196405611436414752391792 * 10 ^ 70 + 383563217652800314658314328972248342957551442181981841602969319106702) * 10 ^ 70 + 869921532979493955825270105209784130222511725672912390993934192978210)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_130 : Polynomial.coeff recurrence4A4Square 130 = (1785701030151546051933777733904548140764448619 * 10 ^ 70 + 407071967863805100674718687397221012006751084692370896613669437755957) * 10 ^ 70 + 9203098614624584834318276278827325655367551438164224918739799508151911

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_131 : Polynomial.coeff recurrence4A4Square 131 = -((4721809572096308525674762018219595694306063653 * 10 ^ 70 + 9317797526973619909720440013776210844997749805018544684405360691347235) * 10 ^ 70 + 3810736566876736645868142201898123149123109646870157193059162106658948)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_132 : Polynomial.coeff recurrence4A4Square 132 = (12245380980808774970811934617469185384299384231 * 10 ^ 70 + 3547653041937712957108581027779498982031289874967014733517065683373307) * 10 ^ 70 + 4831473941716684844268574032537280973314487679616296732357941981577749

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_133 : Polynomial.coeff recurrence4A4Square 133 = -((31148638734403906502628113311914357907419839591 * 10 ^ 70 + 10924342816463319918776249008329786479139516797199612549593769560275) * 10 ^ 70 + 9141263765881934229059939903932527648585316031999288458393309500009028)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_134 : Polynomial.coeff recurrence4A4Square 134 = (77722444416709017441169896808424669185098572572 * 10 ^ 70 + 2060364635212768924176945218992456615467048442990516179378945884572136) * 10 ^ 70 + 4260768505397094906047618983947749520961909533777497032670739914239427

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_135 : Polynomial.coeff recurrence4A4Square 135 = -((190252766505959382408693403548234090826868173116 * 10 ^ 70 + 8264471528589725400512593420802855152878686404605036208628762657565737) * 10 ^ 70 + 2862962972796265110995444015024190718718370017671200114859513539581754)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_136 : Polynomial.coeff recurrence4A4Square 136 = (456907294360938763443100234061656748882704848489 * 10 ^ 70 + 751493926274368296985849759020286646464043091594200173451715185577218) * 10 ^ 70 + 4830160831559495689514480844430767763979586109778117724070594222863034

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_137 : Polynomial.coeff recurrence4A4Square 137 = -((1076643993704583677851088142572549245486350109402 * 10 ^ 70 + 9831294125047671693179098730018844053621113032916320227562700998070868) * 10 ^ 70 + 6502641517815811306342869756733926252830457161097321456702221229927446)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_138 : Polynomial.coeff recurrence4A4Square 138 = (2489409466607374341443467012416756401653526210231 * 10 ^ 70 + 4923704469054431466193797996538942607084174437997476225730888020575058) * 10 ^ 70 + 3991848530901806451230164591051438098482085800081456545251145448983090

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_139 : Polynomial.coeff recurrence4A4Square 139 = -((5648497543184008379525920617929465471016328060250 * 10 ^ 70 + 7252048055945060120042255115400159603869404884838726253178712515825523) * 10 ^ 70 + 3484489276980894197941703324194138506265540118770793458643736440493668)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_140 : Polynomial.coeff recurrence4A4Square 140 = (12578044105099352385171764260834292499369031477065 * 10 ^ 70 + 4349817055732352028987500226819165451060443146473053296665538886028170) * 10 ^ 70 + 4111192611623542641712376125955219680775003331768429361621503785525889

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_141 : Polynomial.coeff recurrence4A4Square 141 = -((27489509437162762786731787726698171688208231531277 * 10 ^ 70 + 3776089390472489519088748628713649423754225166502499545239129205263837) * 10 ^ 70 + 6810942512910692419902608689651148331393319820322771346914264881253802)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_142 : Polynomial.coeff recurrence4A4Square 142 = (58968993074554401430096299118164546981466211655565 * 10 ^ 70 + 3506298810403992445579497689803217091777346437626443975913989522778279) * 10 ^ 70 + 296719147310971776559141776686432918786624495506224630436528376969938

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_143 : Polynomial.coeff recurrence4A4Square 143 = -((124168497611773931341913520654010124485825217650403 * 10 ^ 70 + 9064244943505790714088256353105198081842348340741837501812937511176585) * 10 ^ 70 + 3051571059309356447657590261282360260680379356442644442770848157149018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_144 : Polynomial.coeff recurrence4A4Square 144 = (256659474775194694143476002021568984033717095210282 * 10 ^ 70 + 7920163399090856925838319331604729376502310134483766270032432397942205) * 10 ^ 70 + 4038968906884971157064560062904359927750139324593860386522911403321125

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_145 : Polynomial.coeff recurrence4A4Square 145 = -((520819865900038236453359753632454680014121237853782 * 10 ^ 70 + 560218479704036083770269566416677939189315480072724435329957923896876) * 10 ^ 70 + 9059214889744476186986811042061603027255069101836593269369775011193276)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_146 : Polynomial.coeff recurrence4A4Square 146 = (1037593880456711304616975349335301765107527661513103 * 10 ^ 70 + 2384347627485168275684455966702911155954235987167772826767913032762811) * 10 ^ 70 + 9121900121349952787705174520599136721630365485210556092830280209774667

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_147 : Polynomial.coeff recurrence4A4Square 147 = -((2029556751062258105822932369028884437433513000289994 * 10 ^ 70 + 5806581796862441853750525763716777358138647435949606658550562841989420) * 10 ^ 70 + 9921431928589130506860253274421261875136660440474224834233129853034050)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_148 : Polynomial.coeff recurrence4A4Square 148 = (3897914676281399686960899990669065239183630680539299 * 10 ^ 70 + 7640821223119268648263239430401765671708132183381231584636248057524466) * 10 ^ 70 + 8997604844915243273050774884883850638917696957339177515241234054672177

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_149 : Polynomial.coeff recurrence4A4Square 149 = -((7350946602560983597487550577607140054973683493067092 * 10 ^ 70 + 1179718059487628871874131324715757316649113498067520266116037261805529) * 10 ^ 70 + 8437459442178283982429756685230815224923818411545819727462827212525100)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_150 : Polynomial.coeff recurrence4A4Square 150 = (13613054962056286650629435548039232360682126110625936 * 10 ^ 70 + 1938090543446556573496236773824006935498637183837713141680629693101749) * 10 ^ 70 + 8847619428029310130588084969164091043273564268753217085612639429865423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_151 : Polynomial.coeff recurrence4A4Square 151 = -((24756543433837161941111237251089989569578849829123863 * 10 ^ 70 + 3333237179601244312573145734686737654603591072799717862020470128967693) * 10 ^ 70 + 3350366283353160354505762886238536656508944478767928376133375883010076)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_152 : Polynomial.coeff recurrence4A4Square 152 = (44214661665395639689613886524611916690842026815189053 * 10 ^ 70 + 8623143135686226438237953483048922749666540291644186480618600397403586) * 10 ^ 70 + 2370591443714154428777814263945189463866818661968361030321572881664341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_153 : Polynomial.coeff recurrence4A4Square 153 = -((77553862935789723426461232935124387766341074998827947 * 10 ^ 70 + 3967356203435824751229105085603052033151650194868355468040235681022604) * 10 ^ 70 + 8360851949812058801746143470477685982180431805917827254126972569177934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_154 : Polynomial.coeff recurrence4A4Square 154 = (133604004239997743181925463519917954316779752905348491 * 10 ^ 70 + 3202695738039366318512857980622861010823131245429932260755108105771222) * 10 ^ 70 + 1473671352842445249412855371805181228461737102669775368573488996111116

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_155 : Polynomial.coeff recurrence4A4Square 155 = -((226064129470722424792510674253623380169234523670377031 * 10 ^ 70 + 8550730252317765612462987678992920130547048074841312731881463333671787) * 10 ^ 70 + 2658463749217420055363271930900658773786712217607609985439629404272324)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_156 : Polynomial.coeff recurrence4A4Square 156 = (375713128230057224490336055443358052216668998639243404 * 10 ^ 70 + 3042335415623380132929938215580143333585537441905375446329757249650298) * 10 ^ 70 + 7052035506706129579237858616482353581732283565434472591234436507171213

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_157 : Polynomial.coeff recurrence4A4Square 157 = -((613351135750687989117321412056376771304429778689329063 * 10 ^ 70 + 9337565587929164833417794715656251167199327389175504324569414679046682) * 10 ^ 70 + 9342684447938841244098374265978817602395082696260241429158075625346362)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_158 : Polynomial.coeff recurrence4A4Square 158 = (983568924890009997384442510795555512306924003403772376 * 10 ^ 70 + 7914930081878629513848269702267942343867980293190781859851021387358175) * 10 ^ 70 + 5537381954669417049312712820528896570290904962684090985404724333794238

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_159 : Polynomial.coeff recurrence4A4Square 159 = -((1549377205574492019042045753661207542795854405909322667 * 10 ^ 70 + 4506453770502700216551554077134071530876669306784516238848378568180283) * 10 ^ 70 + 5260688313258446339359266516664621492217958974247554609105182709996782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_160 : Polynomial.coeff recurrence4A4Square 160 = (2397614576139228211493664763696786624707473581189847476 * 10 ^ 70 + 5799849624340713816963271650582931556404131979536589562579743036175225) * 10 ^ 70 + 5245942617185485498467067773050273300201232422432957499750292881568036

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_161 : Polynomial.coeff recurrence4A4Square 161 = -((3644884132020079043416321673331994132602705033836165263 * 10 ^ 70 + 6300121079619921114043495948752651765331918031821555500728455027093419) * 10 ^ 70 + 1980978322902138107058878554261528969058377877047574804042756761792222)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_162 : Polynomial.coeff recurrence4A4Square 162 = (5443544046271666360608902159098243477739808934493862109 * 10 ^ 70 + 2303330289518620717088474399923609131377844445401688235076785659050281) * 10 ^ 70 + 8465486447317185576651342235639559484969601782210337692708670215100027

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_163 : Polynomial.coeff recurrence4A4Square 163 = -((7987008242103645963749311733125018024252311487408627468 * 10 ^ 70 + 8265264658583330289362538730105021664224322197049944364922302810196738) * 10 ^ 70 + 6103025617152651343684228902771396898576683069981504739000577891684782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_164 : Polynomial.coeff recurrence4A4Square 164 = (11513326922956313947033515190776923544693665536898008066 * 10 ^ 70 + 3870622364939914304738065050316565608628067849288478456190346571017135) * 10 ^ 70 + 8173981011422384740754458215512286325337393774216696933935377667704748

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_165 : Polynomial.coeff recurrence4A4Square 165 = -((16305758729489339144784383612141978238992512818406211920 * 10 ^ 70 + 1974316246943728648324944443207094841926184445633122977926152959416008) * 10 ^ 70 + 6376848095206852549989984157127043067537491945814150744071052461677850)