Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_157 : Polynomial.coeff recurrence4Scalar2Second 157 = -((((7 * 10 ^ 70 + 3313620333024724055013686638859485839471052806620541453559653796858124) * 10 ^ 70 + 2932609444248122817573266895161505273327966413400090262175144449767852) * 10 ^ 70 + 1935415195386330839624172112053422498926551820285966675586601636839752) * 10 ^ 70 + 639858521840403748590101816675740843024800912948058493712051264991767)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_158 : Polynomial.coeff recurrence4Scalar2Second 158 = (((27 * 10 ^ 70 + 8307771020730729018863090747325350285042468696890238190970487810290043) * 10 ^ 70 + 2980960255869707886248815170017857672653990838375731192287303417714579) * 10 ^ 70 + 2456919679496768245811808895276590878672305342726061036018453297720513) * 10 ^ 70 + 8508369899810169348659174974120446931594104894858612278224643080451320

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_159 : Polynomial.coeff recurrence4Scalar2Second 159 = -((((103 * 10 ^ 70 + 9543959238042016690972193574948489511326502917950080230849223805081616) * 10 ^ 70 + 2823708381434518490623669965954762548202146897833198891351601025784150) * 10 ^ 70 + 8030217035059372112961467084062766144922355469439390383291524943841287) * 10 ^ 70 + 9012181125609054818537834826744104935720626458045976766596935994675725)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_160 : Polynomial.coeff recurrence4Scalar2Second 160 = (((382 * 10 ^ 70 + 961885338739942339961124863358510675276696750457777314157359286171759) * 10 ^ 70 + 5107269755010076065235212647242112616306877807020882660641135861788318) * 10 ^ 70 + 6747421660194932858221932353636964511387132214601583826128375466675302) * 10 ^ 70 + 1164159093556365848321708266482406162798485298123276246642183190605330

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_161 : Polynomial.coeff recurrence4Scalar2Second 161 = -((((1382 * 10 ^ 70 + 1311723447273302369704166254023671303527036727304784091877642106284610) * 10 ^ 70 + 3335284113296369697961260990832581386585810462688645940382436360699780) * 10 ^ 70 + 5995980839877761642721279001469021133054125230418222753367874302571038) * 10 ^ 70 + 2977451188620517098623401035799375341383680696930608863032770507961993)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_162 : Polynomial.coeff recurrence4Scalar2Second 162 = (((4920 * 10 ^ 70 + 4618607606282418134693657858824627465073831804001899280278371678734488) * 10 ^ 70 + 2967407598664785227450157059157825712548228939728827201508606481642027) * 10 ^ 70 + 1056969535798771859009453877486823617196102295940111439464609716457183) * 10 ^ 70 + 5544066918583770442219007281901237617903360029861405671305733885016928

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_163 : Polynomial.coeff recurrence4Scalar2Second 163 = -((((17241 * 10 ^ 70 + 4919601782642287727548353093473251063420997423507623284870064716462252) * 10 ^ 70 + 947248614095601563703317952792250087525442034729196846873484631086929) * 10 ^ 70 + 4969563065658037049771640773760009508120853187349995807024943221778446) * 10 ^ 70 + 1395121582599719256397194613126772906031046899966205123421525779968855)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_164 : Polynomial.coeff recurrence4Scalar2Second 164 = (((59468 * 10 ^ 70 + 5698670842800584941178310002303050016055180037745915332317634330316776) * 10 ^ 70 + 1174076417165483327317137728255306861188185062190164802576937662010297) * 10 ^ 70 + 1239482999336124338003502636527153729154101892287165116266033567033411) * 10 ^ 70 + 2001986686427835195998216613624114512723110993453689934163319607904999

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_165 : Polynomial.coeff recurrence4Scalar2Second 165 = -((((201917 * 10 ^ 70 + 5865810559236549735081880196589095631157126031950533897781268067961087) * 10 ^ 70 + 6254092042765489992338522745715383808465762284242788032267584805623289) * 10 ^ 70 + 624448958630692393599688342923090937834116076308660849520209631495481) * 10 ^ 70 + 6874570560734378175794925347812205228363007849012669387948923667952818)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_166 : Polynomial.coeff recurrence4Scalar2Second 166 = (((674938 * 10 ^ 70 + 4353480722536629928611956071731199545812723120334416828801744782358190) * 10 ^ 70 + 2303710163390392297428692620042263926670000566547788196944288536201123) * 10 ^ 70 + 6066718885743592730407762367507271532833370060578262830964858141817171) * 10 ^ 70 + 4859805080062088043706419205087205285286660935145290247183334657390436

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_167 : Polynomial.coeff recurrence4Scalar2Second 167 = -((((2221191 * 10 ^ 70 + 2187289515010708930236941520015134891768883107393783230072626079580371) * 10 ^ 70 + 9767735160735702230018332700928820523637324365365201791500174798996042) * 10 ^ 70 + 2278072078133944505080748144152466756194854369700929109539701921578801) * 10 ^ 70 + 1041116737069264884043898783130014522641988582690515483242403248018264)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_168 : Polynomial.coeff recurrence4Scalar2Second 168 = (((7197256 * 10 ^ 70 + 6770492490552049410964052351935061190997459651895375252926647841805819) * 10 ^ 70 + 8681648097903121426843972567770201192425232096691067588408214399297166) * 10 ^ 70 + 2424969491955143583670274331264336397554031222809011041107294089402308) * 10 ^ 70 + 7907794343543411960318625226424597449236192170312114243282946508997402

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_169 : Polynomial.coeff recurrence4Scalar2Second 169 = -((((22963276 * 10 ^ 70 + 6896395356480641574934841102395014811412310383882210419343234950146069) * 10 ^ 70 + 9531314220961993421670490877602477720932435998130917852246306075409239) * 10 ^ 70 + 7358561540951587255939376622527814916316315214522935415505041703562701) * 10 ^ 70 + 8158566747980086767439458461827138279245368789809798383183624594931000)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_170 : Polynomial.coeff recurrence4Scalar2Second 170 = (((72145993 * 10 ^ 70 + 7020129517561145946776923077863721090440312686657606567878107046958867) * 10 ^ 70 + 3561588680186888508122187698369321684663488831088372902951395886295770) * 10 ^ 70 + 770811703535004255416429615851534726668511374174407903513699540424114) * 10 ^ 70 + 9645507790310656253061317262483066256732537425134629252554112500060858

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_171 : Polynomial.coeff recurrence4Scalar2Second 171 = -((((223216789 * 10 ^ 70 + 9004591899046775369383943161625755057474191290742764568508594756325584) * 10 ^ 70 + 1332170535572711976504199443451246997849652890412401108109850302865885) * 10 ^ 70 + 3069355610501943609405918474364590819276747239510804770081544354281124) * 10 ^ 70 + 9715684896909982537898220282741258186072002119719168155238347743628251)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_172 : Polynomial.coeff recurrence4Scalar2Second 172 = (((680145278 * 10 ^ 70 + 8567424314195398412790271236971789057773579009208866206731877237259536) * 10 ^ 70 + 6925683188496765498821005872173550385500320354834036472246388338745549) * 10 ^ 70 + 837680879087690600912185392081906122743439516303090705108242749897390) * 10 ^ 70 + 151520457090932352002830953708835372718389279248223579554907303065236

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_173 : Polynomial.coeff recurrence4Scalar2Second 173 = -((((2041078752 * 10 ^ 70 + 7939325205842330345547882485802939338799274483386934569424235318930439) * 10 ^ 70 + 2923443928982501163046099842201852044075255158393155947434179845265398) * 10 ^ 70 + 9684175866087753667092935233338442665327827777928320761527787911578472) * 10 ^ 70 + 1634535607160979698566145886704003095103398020639944048270377118981930)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_174 : Polynomial.coeff recurrence4Scalar2Second 174 = (((6032860530 * 10 ^ 70 + 820404922312253598429538916908575835043398261117429524654675728518810) * 10 ^ 70 + 9740425568477050594835156459471724051291479087270165272497152739250791) * 10 ^ 70 + 4467074244726517990794871965357322725919240062690029636061533884007916) * 10 ^ 70 + 6759115462197051195653293860232539506881641097473952969122956269409457

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_175 : Polynomial.coeff recurrence4Scalar2Second 175 = -((((17563603505 * 10 ^ 70 + 6022543973685858761843005007378436627926129442476256824578599321353318) * 10 ^ 70 + 4778786785152908907195659164385431951776033937143480248503080382028522) * 10 ^ 70 + 3998129843860938383204895715589988279967112998867907786937189557181763) * 10 ^ 70 + 522344636683539630506497301009735385318785171540545389466819637010490)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_176 : Polynomial.coeff recurrence4Scalar2Second 176 = (((50367606776 * 10 ^ 70 + 5839930529790621525798059305885608289466520869788116721469580457807829) * 10 ^ 70 + 3619592314421819778172756070297723853812239420721355307592266403552073) * 10 ^ 70 + 9505654861786175035041595822415604344348518168278363046049227991429734) * 10 ^ 70 + 8157510248723624244441956335698754213279777505553128744731404676815231

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_177 : Polynomial.coeff recurrence4Scalar2Second 177 = -((((142284002407 * 10 ^ 70 + 4395710475194304402251720836321959018379332772451227430686506583689011) * 10 ^ 70 + 6842342382372668806501768609448802536399293011707691859057859474700110) * 10 ^ 70 + 5135640428408017102785150780852410508285481076050266159035648131069645) * 10 ^ 70 + 7454615543416550799316237739778604481487853946729083938905538570007277)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_178 : Polynomial.coeff recurrence4Scalar2Second 178 = (((395955878187 * 10 ^ 70 + 8684985799396297035312906387169868860252932768272892820673626469844334) * 10 ^ 70 + 2030816371159017724722812420678787566239070008938334887870422414776723) * 10 ^ 70 + 7286444024872485544905439731098222725547710217208824351938526181608839) * 10 ^ 70 + 2330648732430415488153697392221367543821073544258170639699910670377271

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_179 : Polynomial.coeff recurrence4Scalar2Second 179 = -((((1085529341443 * 10 ^ 70 + 926297751641284277243233419976153423072986168920392654308650129455139) * 10 ^ 70 + 4136497934786110903103495453484646901359373402399911433445669619811180) * 10 ^ 70 + 6712020867553003759778765383154015794707542412071697554012318363201102) * 10 ^ 70 + 7931002371754993064151364268486702038260889114265041347120684025520265)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_180 : Polynomial.coeff recurrence4Scalar2Second 180 = (((2931957485719 * 10 ^ 70 + 5238928131160108641864223219193334393506613398823734631245740298971913) * 10 ^ 70 + 6922818962358887497462408311143531966365696957671362124995999119691557) * 10 ^ 70 + 6316511100369888325111142432826698893957282408909285855460630078304807) * 10 ^ 70 + 1350064350359788210648888430537321402579866755121803749798919874336061

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_181 : Polynomial.coeff recurrence4Scalar2Second 181 = -((((7802101107919 * 10 ^ 70 + 5912630796961496180114481702312120712471123736422241906105239234526493) * 10 ^ 70 + 885851191308281466731098063134555090366136986903400951962754116758463) * 10 ^ 70 + 3158700524308182917867233166531870215476017414550198424703874314849454) * 10 ^ 70 + 5758114549847164683948124403677533778432802265384451317476395408327017)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_182 : Polynomial.coeff recurrence4Scalar2Second 182 = (((20455916973096 * 10 ^ 70 + 629142873913741583234153001464571074637191647064125912079097919038778) * 10 ^ 70 + 3841623640518959867487261911388976518993276533037673433586043121769566) * 10 ^ 70 + 9108773009679163326277238753968075533811789020637406365783205420714831) * 10 ^ 70 + 2919152956687300480234750297693802418516511357049046804868283725342901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_183 : Polynomial.coeff recurrence4Scalar2Second 183 = -((((52843876263808 * 10 ^ 70 + 7813323591526975818916764854412535319790543057567524518238629738021244) * 10 ^ 70 + 4829629437654609644842684725836230461080569002397954225203284169642326) * 10 ^ 70 + 2146993909858714758371468932498820841971461097182288795477681493312056) * 10 ^ 70 + 492763487448916926571660230294161484770814109063801663569149501168738)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_184 : Polynomial.coeff recurrence4Scalar2Second 184 = (((134509442783461 * 10 ^ 70 + 7334037551123808925758930819694774628605529798902037443375776028865613) * 10 ^ 70 + 6567225970693174859701660623353853714296164273296091637834153487128671) * 10 ^ 70 + 7011898528926900574567734935918464005751511940984035886047944277556314) * 10 ^ 70 + 9235357968320824457295682617686118774476714123352665085323393954438315

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_185 : Polynomial.coeff recurrence4Scalar2Second 185 = -((((337370041938363 * 10 ^ 70 + 5453131464496378876638916012165115786643203741546324190589639365407774) * 10 ^ 70 + 6389836133597014881290121130318763887727745169324822190095567887308888) * 10 ^ 70 + 4917155047768786808408822035901178322804046357784033863034838603451878) * 10 ^ 70 + 4647852612034019319885615535265178597114815751935950031108106779260836)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_186 : Polynomial.coeff recurrence4Scalar2Second 186 = (((833812335111696 * 10 ^ 70 + 8117978518819967472051113981491683558812017761705549918641309213284071) * 10 ^ 70 + 2345190284639074729373605231561339377432596228118965382263073109089727) * 10 ^ 70 + 8370237786617835917736144449839732083672667466759440698726798429563944) * 10 ^ 70 + 4896526014817849214756302210775083907816120453350534541429989548359412

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_187 : Polynomial.coeff recurrence4Scalar2Second 187 = -((((2030718717484386 * 10 ^ 70 + 5247386039087932795072709946778889550605711275354878460055844614506098) * 10 ^ 70 + 8687258168960562523670545774241736095132574605234392866186926122296753) * 10 ^ 70 + 1310511763335711337713836776446711686428895230994258816087900662065942) * 10 ^ 70 + 3569821708324448349186758016195567249393708851659999576633740279685554)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_188 : Polynomial.coeff recurrence4Scalar2Second 188 = (((4873731978191837 * 10 ^ 70 + 2875325943328287488856625895292737849550509920056763069584683669314984) * 10 ^ 70 + 2644085565227781720992456494241337119068399556151032425411787015527169) * 10 ^ 70 + 3471587473354538840947257633110372257759956268218685199767420528579290) * 10 ^ 70 + 6366752000304747406466917519587934066060840411948777869357588871714375