Recurrence 2 lookup certificate: Scalar2Shift 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.recurrence2Scalar2Shift_coeff_154 : Polynomial.coeff recurrence2Scalar2Shift 154 = -((317498696960507830868892740729744498111167 * 10 ^ 70 + 1701428666497134133939098505067224308489770612708232423251016468144489) * 10 ^ 70 + 6091911568593487179513153193668027368885741417388112738926550196331192)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_155 : Polynomial.coeff recurrence2Scalar2Shift 155 = (11860638941248606762639933930990231342981802 * 10 ^ 70 + 9377278707973965700377510421633044563342291749906922832559754088507179) * 10 ^ 70 + 7365384083539580755946786524143137372756634018850767814450665316505424

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_156 : Polynomial.coeff recurrence2Scalar2Shift 156 = -((38942493945039813944633037945585538406057793 * 10 ^ 70 + 8225582650190568019468568557581504068060060982862785392230516561905951) * 10 ^ 70 + 952738002085036757258817296637468658098626233507462878532103866968300)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_157 : Polynomial.coeff recurrence2Scalar2Shift 157 = -((2744697383340145051538781152788734634331729 * 10 ^ 70 + 7358712742768445359673008694458438785143535256623451988337048004046461) * 10 ^ 70 + 2665704690002788992630214466621558042706135960557447329640872669644717)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_158 : Polynomial.coeff recurrence2Scalar2Shift 158 = (480201032003374779351098062464456644241820309 * 10 ^ 70 + 951247105147283363144530691364450705214431896208500162284404359864827) * 10 ^ 70 + 675277909408055282619278860156917524846091200511923068307586168542109

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_159 : Polynomial.coeff recurrence2Scalar2Shift 159 = -((1754368785866049143684272158319487508128295644 * 10 ^ 70 + 8823671725466450318902734182644619809174045906719683060222717508674433) * 10 ^ 70 + 2266987478424832268195903164999534372800991141043328733652598192186654)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_160 : Polynomial.coeff recurrence2Scalar2Shift 160 = (961230610360929399358758680188191225162359806 * 10 ^ 70 + 8371682042160144322750758765382084752286294880024102354271361455131898) * 10 ^ 70 + 6672091966140978414483624717346048029633074228443942138497200595812241

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_161 : Polynomial.coeff recurrence2Scalar2Shift 161 = (16501961545096185034824506402227274272058582513 * 10 ^ 70 + 7027632609473932800830877293394640224082864194389457921288796380976591) * 10 ^ 70 + 8645680835705209768861476482982223267335667380661461408013694254705120

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_162 : Polynomial.coeff recurrence2Scalar2Shift 162 = -((73153133014968027974378192649184541871490644664 * 10 ^ 70 + 6022525529029163293972360895007648620848646893459831326736575725801511) * 10 ^ 70 + 7674894144477409270355072418969727499408314284999492489533355728467469)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_163 : Polynomial.coeff recurrence2Scalar2Shift 163 = (95069064124006197629645974469058429167960919486 * 10 ^ 70 + 4303634315905316247067946599844267823633704535008246640341021833778028) * 10 ^ 70 + 8155915090165431779925238544343529025406638325881766847889481749182106

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_164 : Polynomial.coeff recurrence2Scalar2Shift 164 = (429808669129348994270027070516776511312449235695 * 10 ^ 70 + 9716064033878360763262898462875020816696495576272651161692756591116850) * 10 ^ 70 + 9947773751380015052655591225294666024177409400382632350739234405117127

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_165 : Polynomial.coeff recurrence2Scalar2Shift 165 = -((2636615160041950292703266427876666790769292136111 * 10 ^ 70 + 4977542953105286982725787578267695167649104186080309678485558160412885) * 10 ^ 70 + 2240760778058620516583258956185070558597056489414757379565498032070564)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_166 : Polynomial.coeff recurrence2Scalar2Shift 166 = (5541000506154028671356461304519356544249916019326 * 10 ^ 70 + 117718271988014316965909004195424430871425679691015525578205806815616) * 10 ^ 70 + 7143959811815955984984372644948935387680437022704003499021309055344450

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_167 : Polynomial.coeff recurrence2Scalar2Shift 167 = (5811994733947214926841421562311510596868548393529 * 10 ^ 70 + 6720222561346358603847913365381860341316333783199565157798934945292688) * 10 ^ 70 + 7321632238484448033181100082881326618125892276676963450204914486126

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_168 : Polynomial.coeff recurrence2Scalar2Shift 168 = -((77306201594417622671044673798714537249838074377962 * 10 ^ 70 + 4680953663927573237803623188214607052701967457703803696074452033795001) * 10 ^ 70 + 8170571588674343086312313653650238240951182204719745464555409906742125)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_169 : Polynomial.coeff recurrence2Scalar2Shift 169 = (235812599645867128192047690954346197590636827136253 * 10 ^ 70 + 118011411859944239695469406571241720703047739855753004315781342003122) * 10 ^ 70 + 1081996355962033966231375229289990282634077709622839679933851574868589

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_170 : Polynomial.coeff recurrence2Scalar2Shift 170 = -((149073897145536265992507008511914529067440841917622 * 10 ^ 70 + 561961215458675138068246099988939922680017683564414622336061291208765) * 10 ^ 70 + 9703425717694818010333110412058273704043279319367986089242697705812401)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_171 : Polynomial.coeff recurrence2Scalar2Shift 171 = -((1664350583918369772615194644838546748934114008550875 * 10 ^ 70 + 4972882469232619188300384280984196150740471247125331921441098701972462) * 10 ^ 70 + 1768285373320407518568266209231361564924682718191179469697458958255455)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_172 : Polynomial.coeff recurrence2Scalar2Shift 172 = (7684661235925527157424006662795112741819659531332719 * 10 ^ 70 + 8342965667209532391151003421388940749752228561425837876934609876882454) * 10 ^ 70 + 4128546574302132676043720077699530462092806116139210570041133145084472

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_173 : Polynomial.coeff recurrence2Scalar2Shift 173 = -((13893144776536284050605699241921721149220848321220863 * 10 ^ 70 + 2151551154088169821487002401444981438753362086633993032140891197804926) * 10 ^ 70 + 5011334536897536318743177847071688997163863188314707909241114305247593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_174 : Polynomial.coeff recurrence2Scalar2Shift 174 = -((16425900106138680205982012139118684526589089756472923 * 10 ^ 70 + 4173324678732962215502294751335012303308077730709300791293176606816542) * 10 ^ 70 + 5177276099293136330802484330469395171222821364692087991538364788159655)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_175 : Polynomial.coeff recurrence2Scalar2Shift 175 = (185216301019727820223929994447601967435427860539045744 * 10 ^ 70 + 1021848339535431589678305940902890507701712323066732703901195927244081) * 10 ^ 70 + 7256681355034333824314669328541886142839196742263734130055210646101459

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_176 : Polynomial.coeff recurrence2Scalar2Shift 176 = -((560738377603631012465065176346687126588161405279710607 * 10 ^ 70 + 3600788585574904377627323771489337947315163899432932255723987416023187) * 10 ^ 70 + 2589707074232996695749253780788401160472187442879266585573233049388937)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_177 : Polynomial.coeff recurrence2Scalar2Shift 177 = (547393479154127547617949835781020668216649426300945390 * 10 ^ 70 + 453178626042243224292109131289901622566518008844190836870715705379019) * 10 ^ 70 + 6407400791540944402702757483141692692688639664761939475885682795413413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_178 : Polynomial.coeff recurrence2Scalar2Shift 178 = (2638193909353888995049011559310224800195399326548026845 * 10 ^ 70 + 3802549442384166970049651915157758420605652298983496770941112577747424) * 10 ^ 70 + 9476780367615223058725657923407587042612694617217300291658215938561841

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_179 : Polynomial.coeff recurrence2Scalar2Shift 179 = -((14603639700175327433504358669284916120000830422343175896 * 10 ^ 70 + 8466675922211580243469288719870892836826147848417821204009106371085099) * 10 ^ 70 + 3720133167027646553226655193459672625409887452768052418964439757620368)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_180 : Polynomial.coeff recurrence2Scalar2Shift 180 = (34310567269912866521598674789912148183971041436852941815 * 10 ^ 70 + 7053416967966369410605177862246521429223953882305879329058572579553251) * 10 ^ 70 + 7334801011149186019785838557554175520980350952442175099499968945443714

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_181 : Polynomial.coeff recurrence2Scalar2Shift 181 = -((14298803698542203376064095770323381685180677826292922639 * 10 ^ 70 + 7718773309422110931641790375564716266486357051665583756598787428932585) * 10 ^ 70 + 2228402929668787587283706176790187584457403746196259560057381478775747)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_182 : Polynomial.coeff recurrence2Scalar2Shift 182 = -((215364530751175360848511623707893175178187180611006451044 * 10 ^ 70 + 3185297311360971262584108291873568489147808467967054397839656302923433) * 10 ^ 70 + 4471340427283351777334778686501853133526277194608181469870809265920669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_183 : Polynomial.coeff recurrence2Scalar2Shift 183 = (936328339829682716317175186202729232581422609172756582908 * 10 ^ 70 + 8834975493646272841971940114280287175117426349971145151321851856320394) * 10 ^ 70 + 7460758690233227994560256311227821915881511567754605438023272456742039

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_184 : Polynomial.coeff recurrence2Scalar2Shift 184 = -((1955435089990704365937779673882434881589438772667610219621 * 10 ^ 70 + 5201315720496108608272237718597309156845646366374629736528588822575677) * 10 ^ 70 + 3662578805282840077831470450964148625011355538202557232255312688061432)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_185 : Polynomial.coeff recurrence2Scalar2Shift 185 = (514499706413231539646841181570618279504837096069007155633 * 10 ^ 70 + 7224861619003360240692088893664803740373511086223675693267427485222427) * 10 ^ 70 + 8475258182286869096618037328476514880842133356009110351099204975634775

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_186 : Polynomial.coeff recurrence2Scalar2Shift 186 = (12372594893599412754703973962560196240690866233577169987767 * 10 ^ 70 + 8343574642243166720466683142054664989042502175685787650038459160041471) * 10 ^ 70 + 1565984236814136199398980365273876191322750410740393855549208019995947

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_187 : Polynomial.coeff recurrence2Scalar2Shift 187 = -((51270617941752662346596558150620083043519857040597648862511 * 10 ^ 70 + 4605042575602511574630721155437187107833385933681412927962845626167277) * 10 ^ 70 + 9925529926752855654773121839351115267502925462553123630498732559513142)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_188 : Polynomial.coeff recurrence2Scalar2Shift 188 = (109569377601414025361513298892080527383895023791540006915407 * 10 ^ 70 + 8944390221521484556191312851881415868541257715653709716140995466489153) * 10 ^ 70 + 225819585000534752476143983189171737990152556821911507485953436114880

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_189 : Polynomial.coeff recurrence2Scalar2Shift 189 = -((64950541109100145618949843057337794195981728531126035630885 * 10 ^ 70 + 6068382654913313980557797586739558919091522668489471005487514617074166) * 10 ^ 70 + 7384160733775437057172265453117758339679193979291489844211269743424626)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_190 : Polynomial.coeff recurrence2Scalar2Shift 190 = -((498595228615811658362016745132672390912931894568349168418369 * 10 ^ 70 + 8975277966075134564156469555496455152399377410311156968571270187677209) * 10 ^ 70 + 3453407869965595197976475484725491450012362524302274538384292720845263)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_191 : Polynomial.coeff recurrence2Scalar2Shift 191 = (2355736406141405870342494739415640037495554621444502741694944 * 10 ^ 70 + 7469610532469451037557432082841118857737540199926232331331761173604263) * 10 ^ 70 + 6506608146583966818536799474872495796099617630690205497267544347959252

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_192 : Polynomial.coeff recurrence2Scalar2Shift 192 = -((5788478372450806695389387195091178755661978137215106603670614 * 10 ^ 70 + 7323808503235470603301532133526314648703304181534455247671661564557698) * 10 ^ 70 + 7106332512167404966551680116894597648142082075355934488902123214875713)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_193 : Polynomial.coeff recurrence2Scalar2Shift 193 = (7060332067746918285972289429428230666629509660765369131674219 * 10 ^ 70 + 1121625757449460979944896354963459327407146906793777415757818621200545) * 10 ^ 70 + 445251609436428145606884794229994766450407648154300907808278352923702

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_194 : Polynomial.coeff recurrence2Scalar2Shift 194 = (9559630197735222639911257093693553874243036600309077782440397 * 10 ^ 70 + 7870477321363276088787619379149643131170284279156928319916807158377058) * 10 ^ 70 + 539529999176669014987727853758739781274033653164545457268063858175341