Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_153 : Polynomial.coeff recurrence2Scalar2Main 153 = -((1441638645949383759390599662860639397142932 * 10 ^ 70 + 1703483906128295940717941520531465825101646615635362766759089023712461) * 10 ^ 70 + 348900761221758878233868624479866591276438973726423270131640622261497)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_154 : Polynomial.coeff recurrence2Scalar2Main 154 = (8730960381700249696173712842165181926504409 * 10 ^ 70 + 9263218558309758781517884105800348526781138826072390824638494725882263) * 10 ^ 70 + 5953571576967832080519845055910524438958191620260697934876197330061406

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_155 : Polynomial.coeff recurrence2Scalar2Main 155 = -((14936164363001835161697355191382438638619850 * 10 ^ 70 + 763342379933923313508464303218437445954185223083736445814480412278199) * 10 ^ 70 + 8433151318195741017675540097566172640492565840658581218231591217272002)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_156 : Polynomial.coeff recurrence2Scalar2Main 156 = -((48730265626786239023925741980105969123690663 * 10 ^ 70 + 2560815872370466468050611664149477462073178952648671314806028030726412) * 10 ^ 70 + 4909739250871840715913821316906835789583115257202155902676110895467950)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_157 : Polynomial.coeff recurrence2Scalar2Main 157 = (350963535823145499590395901656652486502609081 * 10 ^ 70 + 6630031168719885107815436977992072187045926729887942401793425881843143) * 10 ^ 70 + 3144943752838500656098497989478242881990873872552192377055378798897312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_158 : Polynomial.coeff recurrence2Scalar2Main 158 = -((705880920158951093968040548102675201812341986 * 10 ^ 70 + 5710438192888033948741901009536723302000645930953918605203273241965003) * 10 ^ 70 + 2088074490278710569816748103104646309355559662821009640766374596844548)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_159 : Polynomial.coeff recurrence2Scalar2Main 159 = -((1449407974341019669923346311375676210563538826 * 10 ^ 70 + 2153470319996621314411772729795754940736235757838318238667226048569026) * 10 ^ 70 + 9820758306311579508517922624814253926394544617656683670245760747264331)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_160 : Polynomial.coeff recurrence2Scalar2Main 160 = (13123491895567280674438102088505034595338981397 * 10 ^ 70 + 4264318515494519539242902714564775782368220478306508201350972115881856) * 10 ^ 70 + 1862287008973405831461886963364664221776311229235443019217280592840252

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_161 : Polynomial.coeff recurrence2Scalar2Main 161 = -((30840263804366443953143927845138057921449826501 * 10 ^ 70 + 2779411086599557751749816562849165990524755926955070653999681909621943) * 10 ^ 70 + 5366665344392726092554432269358947502446785337922604312034684476650933)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_162 : Polynomial.coeff recurrence2Scalar2Main 162 = -((34828331176213477516396987348979394072980732403 * 10 ^ 70 + 5623106062101144797196391927070294517317378536813719565706895267002782) * 10 ^ 70 + 4336184555006246776595377056136925464074144602688878668471293690395313)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_163 : Polynomial.coeff recurrence2Scalar2Main 163 = (467983132084550456040991200583938409005979161812 * 10 ^ 70 + 9759242426275161026756069857121991637626609037119365165237089088280672) * 10 ^ 70 + 6722058010201563073497802533857171702560533176817410664233630696839538

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_164 : Polynomial.coeff recurrence2Scalar2Main 164 = -((1336229493481215088851260485445624902215518689756 * 10 ^ 70 + 1668080056435247256716458955509268304407866099544985305040632298257795) * 10 ^ 70 + 4026466871056601231866254164810357131556079684891437642690329040961495)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_165 : Polynomial.coeff recurrence2Scalar2Main 165 = -((134376134833256417009703926308426610105782363082 * 10 ^ 70 + 9107584524875342310232091793476226008058532516743706076835604704690086) * 10 ^ 70 + 8933932050705268779794058186381682901365194130818058834390357561821942)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_166 : Polynomial.coeff recurrence2Scalar2Main 166 = (14861871457020198867550452785169827782361657947572 * 10 ^ 70 + 9967132112056967034171086058710276487441542492296828351223168748286309) * 10 ^ 70 + 1884085835184585334596816049315279579032680518162902547736205784432715

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_167 : Polynomial.coeff recurrence2Scalar2Main 167 = -((54664854113128733950089935411702435186390827255323 * 10 ^ 70 + 6288359904892876660874203113965882980744405907019500299153578114362931) * 10 ^ 70 + 6037511981397673914863478366107846342552190623337254715793385671347231)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_168 : Polynomial.coeff recurrence2Scalar2Main 168 = (52937652315206331451626018213520077380371719048301 * 10 ^ 70 + 9379507933359128901384898493150548720193249045300182229723952419535254) * 10 ^ 70 + 1681655463939647893173422977586054769047688924909316173891172610300743

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_169 : Polynomial.coeff recurrence2Scalar2Main 169 = (356120918268205878304277686779267829151457826126850 * 10 ^ 70 + 9883142763382247435846122309337954880347769123734185959379250819184449) * 10 ^ 70 + 4284968452636461825457950827314699763616620241186780278525410460804781

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_170 : Polynomial.coeff recurrence2Scalar2Main 170 = -((1890736668630311484594832175022980606539351712143690 * 10 ^ 70 + 214903876966533998646258748143015660956052758578217528498902906815043) * 10 ^ 70 + 1399275492466997006334403920280133982488044782340901364545225642534153)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_171 : Polynomial.coeff recurrence2Scalar2Main 171 = (3746234560853927071524454182785329870959243715578636 * 10 ^ 70 + 3233545025599102425185445244184533194732746236231727601359202117462167) * 10 ^ 70 + 6040907905872231651438377062006321594031784820372080561703147548891851

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_172 : Polynomial.coeff recurrence2Scalar2Main 172 = (3803897387504099881095473843378071563789003730042691 * 10 ^ 70 + 449956530987444026072391706450649190106770485756993093463974205442281) * 10 ^ 70 + 8838751083515538910066234603949974171026097975774355688919392407126470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_173 : Polynomial.coeff recurrence2Scalar2Main 173 = -((49756747913293379334345932894304461902551871365142393 * 10 ^ 70 + 413058299449755638882991962111004304559859776309183803021566984705702) * 10 ^ 70 + 7468853674002123298305951020173453300401792913921105473050086442318136)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_174 : Polynomial.coeff recurrence2Scalar2Main 174 = (155065493619634024842212067477059304111825376130238023 * 10 ^ 70 + 2751839111028426178479692950926271116390041945868898812074437759835653) * 10 ^ 70 + 4849178226571002282674910366359318226763416019421432514267305650304340

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_175 : Polynomial.coeff recurrence2Scalar2Main 175 = -((142263302139801581071850377844160861492397021803144099 * 10 ^ 70 + 6779706999397690209702931400249323621770751606676129186299197990908113) * 10 ^ 70 + 8321594531451202950744601452709231880005896714269514867029629306422195)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_176 : Polynomial.coeff recurrence2Scalar2Main 176 = -((832882274823618544724622950958310640649673248308275206 * 10 ^ 70 + 8759893727660584769121409790691616413727204287699713015079630845924055) * 10 ^ 70 + 6580981943235010684918201915165360403727377626675932459112884571972945)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_177 : Polynomial.coeff recurrence2Scalar2Main 177 = (4413929309351417067482660261573221600160418539902625643 * 10 ^ 70 + 5493045062190240769644588210474492258636737823848194757643182707669858) * 10 ^ 70 + 6418697530272012051529479929967083378020133406772767840633420647756862

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_178 : Polynomial.coeff recurrence2Scalar2Main 178 = -((9684796343207333334817581606993529337667383336655080197 * 10 ^ 70 + 7119951653048419030133234088835933872403153359227285795167088085247263) * 10 ^ 70 + 9551934174574417481347613034844679374817258070723466830339906000178637)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_179 : Polynomial.coeff recurrence2Scalar2Main 179 = -((282260917899151081588048408644450514816270396482996557 * 10 ^ 70 + 7598798328021308578303571661189302728952002161830327263898697186057685) * 10 ^ 70 + 9977081233217137105597207556595887828915935866839932043102108454396295)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_180 : Polynomial.coeff recurrence2Scalar2Main 180 = (81425357215319724822794250961147492919305469265901862671 * 10 ^ 70 + 6521953287223018221465031974782819129343623212821356217726783140141496) * 10 ^ 70 + 3213658008288055926111213916254324905594757772289462569915456772182488

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_181 : Polynomial.coeff recurrence2Scalar2Main 181 = -((308862979799554889494607823250576013184656590465503519297 * 10 ^ 70 + 755917842985844804331985387484034110274427653957313099246714162416405) * 10 ^ 70 + 4025311443604729166590655735108182340911429839022319002119955818330702)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_182 : Polynomial.coeff recurrence2Scalar2Main 182 = (527744015280276195154724415059888588997768986752030209117 * 10 ^ 70 + 4433197833597473473174358166547956108537887851540945417290463513310657) * 10 ^ 70 + 509422312774846269819231643425019966498969787636210239282976720152164

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_183 : Polynomial.coeff recurrence2Scalar2Main 183 = (419263697759710007008427096429584726149972127356702063083 * 10 ^ 70 + 8020381280937083358386424569098787346017637743497166818257629863982407) * 10 ^ 70 + 2513139718301499902783070683369663017574381158937292611402569658942727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_184 : Polynomial.coeff recurrence2Scalar2Main 184 = -((5714546914872151676753573568591464806214238568716551017457 * 10 ^ 70 + 8855851933828295235575157095800662143851039528625065450674711007258889) * 10 ^ 70 + 2938613039826787229148879733721038512443977343928327319959926845922012)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_185 : Polynomial.coeff recurrence2Scalar2Main 185 = (18764759670320657310853357758786492133056189446837592744564 * 10 ^ 70 + 1125604270612112060976820186246263930662630208268195964892002797311234) * 10 ^ 70 + 9489533303599867504349574697273083754109623682400878228145618363394446

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_186 : Polynomial.coeff recurrence2Scalar2Main 186 = -((29275691792024957230969708037001600804456271033819117343038 * 10 ^ 70 + 8600446437479316620138395433349953960077248717373877228699542522528001) * 10 ^ 70 + 3291764219708833819243991565709984009347093314177726546561973493644737)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_187 : Polynomial.coeff recurrence2Scalar2Main 187 = -((25801914646185671232892470428220134915659945570532933746498 * 10 ^ 70 + 1800635170526650397322941981134096497467267180402974129540095895004018) * 10 ^ 70 + 9328492984153421521686332990080302778916664213333352399017404410017093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_188 : Polynomial.coeff recurrence2Scalar2Main 188 = (311924119030704272773748043043632331721421840494914750154987 * 10 ^ 70 + 9854955046159630076449405180205645771053384848967947801688859950748484) * 10 ^ 70 + 5728068006767877073024959671861000862155612210356693893870431826257256

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_189 : Polynomial.coeff recurrence2Scalar2Main 189 = -((1019557048247799845667138511952189600432157183117041408318045 * 10 ^ 70 + 241800906426371879717329643337581190281603899784258885925553680906198) * 10 ^ 70 + 6023765564538497444181767728011321148987268443138281764053179575844287)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_190 : Polynomial.coeff recurrence2Scalar2Main 190 = (1751788352511627712061916435055281840251016291544069901217735 * 10 ^ 70 + 5130919282240061906455839687722886245602109833059278377946389808256613) * 10 ^ 70 + 5062176092594206099697069592306016090789422220635958192144960348567435

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_191 : Polynomial.coeff recurrence2Scalar2Main 191 = (245757585795853263979002144991979672119931720178974725169166 * 10 ^ 70 + 2100932675069903256305931426443652389038159505919971148019836419631156) * 10 ^ 70 + 6399893891971801990069808962274388960777684679421783719622269463666939

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_192 : Polynomial.coeff recurrence2Scalar2Main 192 = -((12779083898079634373604155349151846795305549368520390216883746 * 10 ^ 70 + 8873002974971357717081917851526820635319165137876432239871310415736827) * 10 ^ 70 + 8488684290656915486614154287808262029960645861278830284901666249062249)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_193 : Polynomial.coeff recurrence2Scalar2Main 193 = (47749348049122264133587870865637025599453511673914435455596775 * 10 ^ 70 + 9280463737993619556424120193064512602812614679430783103372865302864000) * 10 ^ 70 + 8659764120763568609464558412220304525731405036178390436282067454563652