Recurrence 2 lookup certificate: Scalar4Shift coefficient convolution

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_152 : Polynomial.coeff recurrence2Scalar4Shift 152 = (46148597423960214555185545278343747632925 * 10 ^ 70 + 6946624665099231725384206755101364505475130238989091770004772506154891) * 10 ^ 70 + 5664639186898165266273487370532906007403859730862122146963022319764901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_153 : Polynomial.coeff recurrence2Scalar4Shift 153 = (97296630767805381291513602230612831773471 * 10 ^ 70 + 724896822986290193260123474571546818367834928126320514676293718387503) * 10 ^ 70 + 1871259667137869863709386660402057805059933487153101510962827644851075

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_154 : Polynomial.coeff recurrence2Scalar4Shift 154 = -((852080630877178872895506230031752117607835 * 10 ^ 70 + 8202759640587931521911667039313031283592576857183650742652624342961202) * 10 ^ 70 + 8171090655613607349882191518201248307589601526039667718539799942619648)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_155 : Polynomial.coeff recurrence2Scalar4Shift 155 = (1876127067117239826268999761670823650370482 * 10 ^ 70 + 4432027940263876371706133676408057912192399988697743089406172940308083) * 10 ^ 70 + 3752042231233034394228815041179201239018289676883100688507262277409858

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_156 : Polynomial.coeff recurrence2Scalar4Shift 156 = (2857458522121874493482454917877703758261838 * 10 ^ 70 + 6796234199479469093377095587066144404842222444104010610886784363821901) * 10 ^ 70 + 9932488678171111668835837203516188149068838719169134931175475453851652

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_157 : Polynomial.coeff recurrence2Scalar4Shift 157 = -((30052461072181840827804224294407607869496547 * 10 ^ 70 + 6319231734959257847513560022200327362947396413427750738111997004248936) * 10 ^ 70 + 7289495364174025730248698161301047719668124991018870179461519468489342)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_158 : Polynomial.coeff recurrence2Scalar4Shift 158 = (70965473425768327358384177520974589881662388 * 10 ^ 70 + 2593613598046638750596703954135055815886117601095050087427776052823485) * 10 ^ 70 + 3681034726229623503366668713131383487864216401825372125284272330145317

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_159 : Polynomial.coeff recurrence2Scalar4Shift 159 = (86103177158371757512340164795243212286433857 * 10 ^ 70 + 8589639482902323906178925966312809050013179191491288101689473534224433) * 10 ^ 70 + 5927551967386361656139886794948915342724502059676395373386983679390431

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_160 : Polynomial.coeff recurrence2Scalar4Shift 160 = -((1082181852158121840723071935139182086455279132 * 10 ^ 70 + 7753696420732647941916530970955480832068520806757339403624172774507953) * 10 ^ 70 + 3680770087950434694672610994479476247775463896553525757389453679603029)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_161 : Polynomial.coeff recurrence2Scalar4Shift 161 = (2890854795062077784213333208352358802999451251 * 10 ^ 70 + 3911289632346029598219206250006408915791529244396008794211833299665591) * 10 ^ 70 + 7627483654859411602770793169332874678915195698867640945237993298764986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_162 : Polynomial.coeff recurrence2Scalar4Shift 162 = (1442044665568601857081877866730042385576104950 * 10 ^ 70 + 6033131179720316820385983715590371428872941306151495413184158152720573) * 10 ^ 70 + 7917982768812455548093823933760839599933191628030920358225619270803804

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_163 : Polynomial.coeff recurrence2Scalar4Shift 163 = -((36781896709884275484131157953832813410991407192 * 10 ^ 70 + 1038645502571677024798713486991428466830093625456699081586687690762828) * 10 ^ 70 + 1276957460168705479309434079913238415141934479617076539954607488569644)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_164 : Polynomial.coeff recurrence2Scalar4Shift 164 = (121632310249555637426712626311072414559597416309 * 10 ^ 70 + 1378084675566524730908094084687664576519378715503102702910797115459182) * 10 ^ 70 + 3191136418637951090328646812386916215278875316723348871876682211051689

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_165 : Polynomial.coeff recurrence2Scalar4Shift 165 = -((70553379016254960550638034761694277246044440999 * 10 ^ 70 + 8619152790056128569398846426635066811825406991384103746712697044629963) * 10 ^ 70 + 9802213032230680457816638126385403074448023882939743652686260220266088)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_166 : Polynomial.coeff recurrence2Scalar4Shift 166 = -((985581658804627471407197084465565457811112499360 * 10 ^ 70 + 2382591414009825063119578540400702157698107335479497944035303806538532) * 10 ^ 70 + 150074783860199549909801416059335263546293373464189679261896111117519)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_167 : Polynomial.coeff recurrence2Scalar4Shift 167 = (4452159693929128363356009099672895833799577545241 * 10 ^ 70 + 469693625232277990545090424867145164200634394702480342621765863605264) * 10 ^ 70 + 7747712306799927461052013958652716851278759243802507628736914065159063

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_168 : Polynomial.coeff recurrence2Scalar4Shift 168 = -((7239239948300803105487677667458791540367864965945 * 10 ^ 70 + 2870847012181367099371901095715494244556006601113955130205044474465296) * 10 ^ 70 + 9537127398955429662092145878307785852530263800059930870780457937825257)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_169 : Polynomial.coeff recurrence2Scalar4Shift 169 = -((15194444414796040705709091335313232141048048071250 * 10 ^ 70 + 1635705333171719528230110681327087976492640057196687708549375975802991) * 10 ^ 70 + 8896010288616568145844170202353979870669824139383015743243566544719736)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_170 : Polynomial.coeff recurrence2Scalar4Shift 170 = (125340227630069243021803756266091223498867120439068 * 10 ^ 70 + 8041547128320093916645264464653576263807970395026950917654065316981127) * 10 ^ 70 + 8291985914005091501224209826156996668852106529509663125403125575296388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_171 : Polynomial.coeff recurrence2Scalar4Shift 171 = -((334560326302547415854522837540608598865262862672407 * 10 ^ 70 + 4215797242277708579673986572948364334211067656927352226626975326583190) * 10 ^ 70 + 6694530143155059483682731472065640242293621747673649757568465969485162)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_172 : Polynomial.coeff recurrence2Scalar4Shift 172 = (137791903638307144791140118030946860492374853544293 * 10 ^ 70 + 1911002670305081144082963154791314123111254599035042949664713842712588) * 10 ^ 70 + 429989444870315255336657666957541625300172520925989908462806906677109

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_173 : Polynomial.coeff recurrence2Scalar4Shift 173 = (2420976431968944912290697573212369884275288479863036 * 10 ^ 70 + 4100901138338871723199698975400815888080683513965242576702699126059334) * 10 ^ 70 + 1784793777080787212231396530203827605550923067959648000975883896561938

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_174 : Polynomial.coeff recurrence2Scalar4Shift 174 = -((10278270093061916721252540398901040585269003006079646 * 10 ^ 70 + 6646130270199656923626598927918667776848067884336092171199581719805053) * 10 ^ 70 + 5553370933344425917471512312903717949643932289805574328790496615245115)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_175 : Polynomial.coeff recurrence2Scalar4Shift 175 = (18038120610841587472962667463726025740516546238047397 * 10 ^ 70 + 7579003040300875410422638985508172315409327650174128408882282213439592) * 10 ^ 70 + 9252146689000428871459493261207694011922880592826924444211520223803457

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_176 : Polynomial.coeff recurrence2Scalar4Shift 176 = (18041156355619640164283957928671667056775604216930241 * 10 ^ 70 + 5138551679426566222678139631714673255008310459549353638577149361483090) * 10 ^ 70 + 6507973064303709646194980547595086750901437035742893177220857994618913

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_177 : Polynomial.coeff recurrence2Scalar4Shift 177 = -((215832999491779827598944849713353309494328366104532017 * 10 ^ 70 + 1831405008054401486425002307479393801054540916446827043786119388053413) * 10 ^ 70 + 4793389223210885773291848196499066824679209939789137261372919387834012)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_178 : Polynomial.coeff recurrence2Scalar4Shift 178 = (665824597958332351045753097872240465066190331257392823 * 10 ^ 70 + 6135273787781107053649530771136020769426492215694586953958696387785013) * 10 ^ 70 + 4812506894891778301048796712211018685669855621309278865685366415390677

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_179 : Polynomial.coeff recurrence2Scalar4Shift 179 = -((790869484200933648597426282875745788394222766216829073 * 10 ^ 70 + 9102268747692990947310205922543562210204365411203400884990320662772455) * 10 ^ 70 + 9180917981719423249083974559897073727879134406437291145421547387615458)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_180 : Polynomial.coeff recurrence2Scalar4Shift 180 = -((2229420738889432025073858045350336979883945841640483058 * 10 ^ 70 + 5083190144914343138142490462169915097979279828962295285228724448032406) * 10 ^ 70 + 2807184184782081612569287124325413363649823070789853837338593160624086)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_181 : Polynomial.coeff recurrence2Scalar4Shift 181 = (14526680550047390528941049287749600439788501321569575267 * 10 ^ 70 + 2543664074758860014608449530835959215573110962986845804378837009045890) * 10 ^ 70 + 4517628796454425615649452255231784791092791409584415245234955255327198

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_182 : Polynomial.coeff recurrence2Scalar4Shift 182 = -((38158445693141505328996861216709810406408231875060921251 * 10 ^ 70 + 3270615697817934155443187803251666450869216900948460995535257517934489) * 10 ^ 70 + 2144978481500744434982167311285978287343411807522097780360256381763223)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_183 : Polynomial.coeff recurrence2Scalar4Shift 183 = (36677614924570206173531587775417093119928601315657282892 * 10 ^ 70 + 5363640460923718969260493641261919137323935469750663283689314013688060) * 10 ^ 70 + 1726194453448200187817415519505595421100767180356706267722472528475755

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_184 : Polynomial.coeff recurrence2Scalar4Shift 184 = (139631300020505561035574559977690660832593835900453777494 * 10 ^ 70 + 4798543362551711579620553724702686837558801801737433761571399993041583) * 10 ^ 70 + 9261881033942329199480852278181939169818105819494656734578242608923842

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_185 : Polynomial.coeff recurrence2Scalar4Shift 185 = -((794209501127382386289644861692838894941177873034049019371 * 10 ^ 70 + 7016317971749573275475948696159660263168945507984842300831880832746516) * 10 ^ 70 + 9055214903284510763675137559413822958476633599028748693978814450419823)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_186 : Polynomial.coeff recurrence2Scalar4Shift 186 = (2037481516624352133079829212315498213657464946704164104019 * 10 ^ 70 + 4254777825209655284129819459568531585414408177835291413653770370456550) * 10 ^ 70 + 3727615050942030291661954191771702808202934126403835514634232508801430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_187 : Polynomial.coeff recurrence2Scalar4Shift 187 = -((2260089237257892926270357523174335176880496949924776124167 * 10 ^ 70 + 8151317351416078177233771951574376723976458805732020126729462213165848) * 10 ^ 70 + 9583698683055509703507503878865721147596549934787006819796427611995172)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_188 : Polynomial.coeff recurrence2Scalar4Shift 188 = -((5233322646569849960173822965802286338961607173369690112710 * 10 ^ 70 + 5734505392171708018692454472012551013458106447864855441544203236353665) * 10 ^ 70 + 1290666164008474981076931953178580573076205108277259473947707603120323)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_189 : Polynomial.coeff recurrence2Scalar4Shift 189 = (35002384644545478029089898853434778740620371708785569760508 * 10 ^ 70 + 7664810884930355776107520760930899839419854614079920506837174157638212) * 10 ^ 70 + 8531334801957678964821898956949116189477676550138867400102556290017042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_190 : Polynomial.coeff recurrence2Scalar4Shift 190 = -((99102079935362638978517320742051343305972508274765084738565 * 10 ^ 70 + 2658568202316803220380268201902781535510140703018234829051613978315122) * 10 ^ 70 + 4282277547799879784277786612056228237806192516993484031297510994782559)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_191 : Polynomial.coeff recurrence2Scalar4Shift 191 = (152778470363842121663879497835837475367809742351159948172761 * 10 ^ 70 + 3092089623863695311716306626731528609820229120608855845303614242966461) * 10 ^ 70 + 84193460884283200611569194033979217130925669138842324842906344513568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_192 : Polynomial.coeff recurrence2Scalar4Shift 192 = (42622597331428445003537106563192669645530489250865799015526 * 10 ^ 70 + 5815401958086437951588811614880421494990321472193316225358528154279198) * 10 ^ 70 + 8394365278647885033496901929451033237857033598535592145923865841626831