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_115 : Polynomial.coeff recurrence4Scalar2Second 115 = -(((3246202953326465396305448031078004816272 * 10 ^ 70 + 2514534764477998380141559861150106931038634038068400557720229963502125) * 10 ^ 70 + 4355131266166525772591966225629569843233733716062005183981630174933887) * 10 ^ 70 + 2453218442507881595870489065407018697371336969270876557210292487414854)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_116 : Polynomial.coeff recurrence4Scalar2Second 116 = ((27418511920547538430758836526247172449994 * 10 ^ 70 + 3645570038449488609572357494515960794243879918981953086934803843633408) * 10 ^ 70 + 3729487926717280805656518553645837323809188485052049476681000811307084) * 10 ^ 70 + 7267453814635774979237036206492690541306796417236285626504931879007901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_117 : Polynomial.coeff recurrence4Scalar2Second 117 = -(((226238740504639036522822287657396386085485 * 10 ^ 70 + 3163948655515330692088160594174557915011004045825625394405258345702065) * 10 ^ 70 + 4103655899095554546410885210629699072753575647158277103000883251608245) * 10 ^ 70 + 4399841967454295613625085277966145203380754411473818999345557843289069)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_118 : Polynomial.coeff recurrence4Scalar2Second 118 = ((1824277857568715956884194901178753194267920 * 10 ^ 70 + 3179520418412672060455643331903037078135029460324370961270311743564769) * 10 ^ 70 + 4512203115186277498301502988352615670065618169839386877826206260810885) * 10 ^ 70 + 7515816441491318098042084659669453642030148890904467933392275097461189

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_119 : Polynomial.coeff recurrence4Scalar2Second 119 = -(((14379852285551879765528573467819495739342394 * 10 ^ 70 + 7215108065646878226611986193764829906788311543698015813194914058826462) * 10 ^ 70 + 5374179037744682820301620849667988945587753815113385709433067934806209) * 10 ^ 70 + 6883249220787872193154566463049528181321104806842257676002414559009809)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_120 : Polynomial.coeff recurrence4Scalar2Second 120 = ((110838083983102502372176118282031321332255946 * 10 ^ 70 + 2560720659242003751983250118999864502087214922748724756321711537380013) * 10 ^ 70 + 297789233476251546606354108827791513347509768225579691733785468133576) * 10 ^ 70 + 3413717292796954921769440118040603382461813162102087807598957051934400

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_121 : Polynomial.coeff recurrence4Scalar2Second 121 = -(((835642101918079925340579338257179272199723040 * 10 ^ 70 + 1449400151324803445235244882927805375072629658263638792830015719965167) * 10 ^ 70 + 81523132998966694683475183526940701460331322180477137785862581686494) * 10 ^ 70 + 704647232923934245768293026904276864511714257947053780433081344321659)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_122 : Polynomial.coeff recurrence4Scalar2Second 122 = ((6164080489554067023919492662849379072770863223 * 10 ^ 70 + 7744286611376376691005392831084391344224828497929195888825308246686848) * 10 ^ 70 + 1354850666188000133420285181097420703236632215687300969425135489833918) * 10 ^ 70 + 8676151941998025427407070865469422931680075290941551800314847085256602

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_123 : Polynomial.coeff recurrence4Scalar2Second 123 = -(((44498749567058463078665743163459370575342850679 * 10 ^ 70 + 8135213947129707003118106548367996586956337288082390410385823570451935) * 10 ^ 70 + 7951695709774439827208832523009069057301984388344220313118446082213195) * 10 ^ 70 + 8630592648005092323604383338208480684699538888165741233113785466136103)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_124 : Polynomial.coeff recurrence4Scalar2Second 124 = ((314462555309080638851389768440465908177723103584 * 10 ^ 70 + 6850350376307798037933471426560423159643286456693942761988643560960415) * 10 ^ 70 + 3785059892584524610958323720946606631388625935441653826474429282243053) * 10 ^ 70 + 3356289313510532519212526776014258708940723704934030901657503172731726

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_125 : Polynomial.coeff recurrence4Scalar2Second 125 = -(((2175892500797444509262505325699373037132358428462 * 10 ^ 70 + 5831655147071950317172751916628199168185244880421874126118156414005869) * 10 ^ 70 + 4514343850324782592928103404562752296942682745665243485473222675684133) * 10 ^ 70 + 5416837838856101705957091893906427407664810022286125370571730765823363)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_126 : Polynomial.coeff recurrence4Scalar2Second 126 = ((14745346376653907683947931974352018525862641565522 * 10 ^ 70 + 9736368183827904764220332085769018355127230122808263821467377912484865) * 10 ^ 70 + 3067462558458444005138229061068371133508263469035256596471688341783767) * 10 ^ 70 + 4686490503181759099716819570324754159901704711485024542996269744645841

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_127 : Polynomial.coeff recurrence4Scalar2Second 127 = -(((97885749861353806999632137078832971342721197268017 * 10 ^ 70 + 3601368138360132929829444655096299737824267047453801143338252372162066) * 10 ^ 70 + 4025679878325415042722482445058603220857429874979008122764802078659866) * 10 ^ 70 + 1268589105038779041873271674660006424693895260849829174033518654368316)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_128 : Polynomial.coeff recurrence4Scalar2Second 128 = ((636685972904229379524524559785168399327379787362477 * 10 ^ 70 + 7861835385634343718203995595602871519665171104931764199314549770537457) * 10 ^ 70 + 4635200182194010005505230198355429520176219542150400563121558530893137) * 10 ^ 70 + 626010277080108850392758554450825645365974281994065134139621853509376

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_129 : Polynomial.coeff recurrence4Scalar2Second 129 = -(((4058480426635912607171760613634136650689745278121381 * 10 ^ 70 + 8455570679136819253881373411902757509838206921757591039922850404330772) * 10 ^ 70 + 7494205043501853903875865816971519156259695259063136726361188302309799) * 10 ^ 70 + 6166725003594539698540266308288933310365740526602348154502819990252013)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_130 : Polynomial.coeff recurrence4Scalar2Second 130 = ((25358404017510691696033621294240595781273517994422066 * 10 ^ 70 + 4627284999189500994108820642201249743084871354590636778966111425921572) * 10 ^ 70 + 4610335431200848370019954881922286878935098309524575983214300162097709) * 10 ^ 70 + 125982547001429555760659483383239182439184620442247743324363749290366

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_131 : Polynomial.coeff recurrence4Scalar2Second 131 = -(((155340835702729222605850624514905018372819295462316786 * 10 ^ 70 + 4514730978633686624923938665982693239503074148998888175862409190136192) * 10 ^ 70 + 7365778215558646577103512051750123605383453751052105449832722369193706) * 10 ^ 70 + 1617985594157657899959918141546301491700530379694502672667458352968866)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_132 : Polynomial.coeff recurrence4Scalar2Second 132 = ((933118489418185596948912976203127468106334948041736375 * 10 ^ 70 + 5870792274633873119501049603209448192627966877068303570488281679414369) * 10 ^ 70 + 6464637428423686470371990162447944299441743779056767257875277406481236) * 10 ^ 70 + 2162727436528399917179297523871570938697415187167074786974456813996320

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_133 : Polynomial.coeff recurrence4Scalar2Second 133 = -(((5497369332275514294755083413474673393530363358049312931 * 10 ^ 70 + 5427592229614253011196030666056677263385562707050375425410338837791599) * 10 ^ 70 + 529182654668468463611152040580210210546140347306680485175370307395028) * 10 ^ 70 + 8655881169601006303679449802432460814810811853767870033165190647536974)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_134 : Polynomial.coeff recurrence4Scalar2Second 134 = ((31769984285743978625343318859441327809878601342867584708 * 10 ^ 70 + 9564356989240934847844639663149363533871172150644820046220451549587604) * 10 ^ 70 + 785319202243967879246777762366085970846284858011898394528529310501225) * 10 ^ 70 + 3401189559389786904977937973686908424808175713522395729416008706731686

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_135 : Polynomial.coeff recurrence4Scalar2Second 135 = -(((180134808940821470947501365448614856951041553095539798200 * 10 ^ 70 + 1536508890182036793093747070288216482752716850572159322356109570412658) * 10 ^ 70 + 741776368274037963462286884263993877391879889632726748013504438183486) * 10 ^ 70 + 167032475084996219908705227317146592693202577977880736947928263200196)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_136 : Polynomial.coeff recurrence4Scalar2Second 136 = ((1002234017069652638571952441319834768508881974272075786151 * 10 ^ 70 + 2908169254205600206162894320310535863191057702117678959608607458198948) * 10 ^ 70 + 7508367980120851298225074657515548011718849788261408431883606870563503) * 10 ^ 70 + 4036146604814320920474295383669886352850912188556367568316167889440873

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_137 : Polynomial.coeff recurrence4Scalar2Second 137 = -(((5472699214431687145784748625065934970855908226889730718005 * 10 ^ 70 + 910129188464958054964459846352569103317624483715922156390095231774567) * 10 ^ 70 + 1129614225589435325673388699132809990680139534224885171353167612870804) * 10 ^ 70 + 2510844648734605000383422710971292616197548764688390972221818382207427)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_138 : Polynomial.coeff recurrence4Scalar2Second 138 = ((29333436426348903757243148293418277838276041751693745701498 * 10 ^ 70 + 9385649524632294783008125654141447115267064135872204434716217204223042) * 10 ^ 70 + 3671639965506065709027217966568229678697157850018023070131900247582687) * 10 ^ 70 + 2537064804231411224077684728103972552761354160622339844132347948608633

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_139 : Polynomial.coeff recurrence4Scalar2Second 139 = -(((154354459825311923069012885817593074819337610597435016662059 * 10 ^ 70 + 6598548609819700927843512431979050600954021456856930410281697847604212) * 10 ^ 70 + 453037935742870974924604534821090542626796226931355629785848307004682) * 10 ^ 70 + 1513043662802078578314291667676385795688240049066418133496629222213993)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_140 : Polynomial.coeff recurrence4Scalar2Second 140 = ((797506612735728062560019672802394793200706734487765070999605 * 10 ^ 70 + 5035099213983802897194115949346873498166460019912698051418915216700139) * 10 ^ 70 + 6228504759387419528860775973253042829502181571438728702317128926962798) * 10 ^ 70 + 9633275360754025875456230575262110339765262247568963079801864916915022

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_141 : Polynomial.coeff recurrence4Scalar2Second 141 = -(((4046414724033965653151902492176764147204228552420366255295635 * 10 ^ 70 + 8792531641871198197149912630038996111396662744451223526176475991527296) * 10 ^ 70 + 2485657512966931239541323572321775571417825840821760618497525291488361) * 10 ^ 70 + 6734223493756201711672638212508298730383042838353381272143565560692703)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_142 : Polynomial.coeff recurrence4Scalar2Second 142 = ((20164515098520038962441575887374040814049591584144464318214494 * 10 ^ 70 + 3242094488172151555121692875914932108262618121067098533666467930368779) * 10 ^ 70 + 5277578256601098321973609169051559480269005620602442112985185168055192) * 10 ^ 70 + 8502226419701178043676684862885270071682855227346794843367871388448647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_143 : Polynomial.coeff recurrence4Scalar2Second 143 = -(((98706332085755950042446802569194845919138867023280813075037620 * 10 ^ 70 + 6820298966756314529805633553137645575745710358756346892227910484762562) * 10 ^ 70 + 5103967371936649396576948127053431423586169741218951475534266940846002) * 10 ^ 70 + 4707506620581240391657160589303234957586346613421408585019956416901273)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_144 : Polynomial.coeff recurrence4Scalar2Second 144 = ((474677820783567688129748399179461313423399051185408223162768074 * 10 ^ 70 + 5982221091305307695765367889354951608083595577304098350527673189444544) * 10 ^ 70 + 7889874985551565749615589739196523253236525428257451861382422252551670) * 10 ^ 70 + 9534348074694182929497087379581842503654808374304108177480828275925203

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_145 : Polynomial.coeff recurrence4Scalar2Second 145 = -(((2242873475405397237598090923018367800488542416750986587130465812 * 10 ^ 70 + 7451207092853374840741841580052743242121317143450258583273980404840872) * 10 ^ 70 + 5716753256444410452675442559850488108024189282524721600583530937535011) * 10 ^ 70 + 9586796844953553034330647186570418002933185230822323054330107769786855)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_146 : Polynomial.coeff recurrence4Scalar2Second 146 = ((10413965718905676913871876664443315840460709455641996390158616302 * 10 ^ 70 + 4078270598404052644134774933672821587784343900699145752287445692637013) * 10 ^ 70 + 6720530240806940634346296908996613215774548144421406791928735982728074) * 10 ^ 70 + 1026152624755040525703894099466501226648615127569542295511712767996413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_147 : Polynomial.coeff recurrence4Scalar2Second 147 = -(((47520951704258527895899948809378198203211454906688889384872569976 * 10 ^ 70 + 397714385965585010465771879145838489246788165843514764133126846465733) * 10 ^ 70 + 7848333866315778490660547338120558904986870069786739355109170774157498) * 10 ^ 70 + 2670613307793733658782661363647637815758657632065182519118716596388660)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_148 : Polynomial.coeff recurrence4Scalar2Second 148 = ((213138703938694147497754895984808420793901172956916062545075547675 * 10 ^ 70 + 8178477760298723051122932218795258600068118640927167470426257366307181) * 10 ^ 70 + 8652451679263247155831528191346619377179850141038107915804203738652400) * 10 ^ 70 + 5482895563834839792390014016642370954956564546097347583867523998471568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_149 : Polynomial.coeff recurrence4Scalar2Second 149 = -(((939716497553435268607495019861326916931692517713195908698559149359 * 10 ^ 70 + 6869888498854714016263849811345341648622019133723086122496627369052934) * 10 ^ 70 + 8984985430024589772473230092854125551868779725342886670823407540650665) * 10 ^ 70 + 868575301654833662081009680156201703261876458793025375909734876069308)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_150 : Polynomial.coeff recurrence4Scalar2Second 150 = ((4073206658788866523911778204273267276315136104210132896594764832527 * 10 ^ 70 + 5628831766103847281111671412980908007230685947451497530982839077213753) * 10 ^ 70 + 6354117111943577348386131791601241903172212363606892835044518423299294) * 10 ^ 70 + 35843755023290354393926934024458543102076212127068199725360823781680

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_151 : Polynomial.coeff recurrence4Scalar2Second 151 = -(((17359109858968852173892856778194042587511286127267871134116894513506 * 10 ^ 70 + 8484876582196133733095152065783042432893142714639464581118286334070777) * 10 ^ 70 + 1357321099735813689543484203965641618005334267069194671499953255394764) * 10 ^ 70 + 2502857455390081608613579168182589319182308093437615341137211108223957)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_152 : Polynomial.coeff recurrence4Scalar2Second 152 = ((72746965893900696466705129368868556759422483445272397576115759783170 * 10 ^ 70 + 2973680615252669568759622828585733836541597933198573914119237822955653) * 10 ^ 70 + 5550298147564543701307510729011986067063279465360380852186342186643066) * 10 ^ 70 + 5657659239789449623060981134616063927603623378315173016777428858602473

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_153 : Polynomial.coeff recurrence4Scalar2Second 153 = -(((299807474711121626988118385901511826812878575421734877995908094215214 * 10 ^ 70 + 1709379153934336512031789379198061321697935782508119670259973728251593) * 10 ^ 70 + 8254416731182558780838695832743909550953781892929930772922874452053415) * 10 ^ 70 + 5289419495063654527209426971616009498889394849625890584064573497066877)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_154 : Polynomial.coeff recurrence4Scalar2Second 154 = ((1215213572307428011942431630158983617141184110722044489670236877485173 * 10 ^ 70 + 3638940765409059585726393608131679294195900394920506740300287857328678) * 10 ^ 70 + 8421243204000104675516977625863162682164237703841098053308011749162969) * 10 ^ 70 + 2036273012716367427712980823707941669565258158280825076402187180326316

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_155 : Polynomial.coeff recurrence4Scalar2Second 155 = -(((4844919421082908184102158711321914980303903295909257679816296815519659 * 10 ^ 70 + 3541976112264241802346869739606341837463644208537177842708963033096380) * 10 ^ 70 + 457651737666029622925377450617036049635184485356060067509496375551250) * 10 ^ 70 + 4573856836155816515355169035679736240517299409468190180453715186851934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_156 : Polynomial.coeff recurrence4Scalar2Second 156 = (((1 * 10 ^ 70 + 9001343143873514160402824088546988945032789689286583266395577535900629) * 10 ^ 70 + 8000141681388661049312784879157563321861574881232079158161306350271138) * 10 ^ 70 + 5974361619969642604152703657888783338580455028600566034474168317249751) * 10 ^ 70 + 3637430261807916662505368851245031931666051232146380294825543203777585