Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_171 : Polynomial.coeff recurrence4Scalar2First 171 = -((((241079209 * 10 ^ 70 + 9381030105053601149449731200938843776488175225285764839573571733877051) * 10 ^ 70 + 869378571345891739344836394863873122581514367850998498086776962891516) * 10 ^ 70 + 7267920684986803734863033023644669144765535209383512840000963608995273) * 10 ^ 70 + 6524924455526068106865218144070266540976213677751705668284023928912282)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_172 : Polynomial.coeff recurrence4Scalar2First 172 = (((737593409 * 10 ^ 70 + 5773800110745300170212888060703209762583476881150713367297462478011814) * 10 ^ 70 + 4462210830952338790997132055518640952996710030609752119217228279893992) * 10 ^ 70 + 6421035358026931505127433029168577822512098578840389477853745935611155) * 10 ^ 70 + 1282562391150544937446598356297343919287055027539927217310839434856419

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_173 : Polynomial.coeff recurrence4Scalar2First 173 = -((((2222911756 * 10 ^ 70 + 4187699473442366043418865197064618661937699826773778335746516163887710) * 10 ^ 70 + 138742471988491538657542291090500867331237556693335136142972159226789) * 10 ^ 70 + 3471485880077124332794717591084575504009979205430957168534017809813238) * 10 ^ 70 + 2895808652672387400357766084668569727630813926165809166794724538031947)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_174 : Polynomial.coeff recurrence4Scalar2First 174 = (((6599330389 * 10 ^ 70 + 3495945544027281891016073009056218423266039104646174469058103086194845) * 10 ^ 70 + 3369232764256985484731683078615263886657356864950321201319404777988459) * 10 ^ 70 + 3494159243143734884358204142069466602651408255395945346524025440215420) * 10 ^ 70 + 6704504829380914565694817405930927535514956056400673844729933412312393

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_175 : Polynomial.coeff recurrence4Scalar2First 175 = -((((19300731266 * 10 ^ 70 + 7310835759145566160745815989630900819475401991192630548507962016456669) * 10 ^ 70 + 3011765450926358623052009312898219025814388857174258165712249865377157) * 10 ^ 70 + 7277202361586505342378005538056122792677058133439491304521624131993220) * 10 ^ 70 + 8144384455857393655004215359702384820370681683147875933931367118394229)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_176 : Polynomial.coeff recurrence4Scalar2First 176 = (((55611801887 * 10 ^ 70 + 6947610307497093433194125762156053800750696058348888536399982263271349) * 10 ^ 70 + 7490738371286997676095293389877364959359730952136135064455624381324383) * 10 ^ 70 + 6591812522122683879547336717816971916940178999449115247496357129030722) * 10 ^ 70 + 5056118988920061276254024376811230661452687808040359232602031561555899

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_177 : Polynomial.coeff recurrence4Scalar2First 177 = -((((157870810029 * 10 ^ 70 + 7307067922524107190654116568348765660573129709887863402745757674600633) * 10 ^ 70 + 1691763281460415259552410763761123971308309952225386374727097014691567) * 10 ^ 70 + 4555634195274004953040376891213239566291611344254177319166822025241534) * 10 ^ 70 + 7861717025602298536287495864925680652611706600921280428422153060173839)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_178 : Polynomial.coeff recurrence4Scalar2First 178 = (((441570481406 * 10 ^ 70 + 2522227689140765206405951047194541841937087562523568381694000922245650) * 10 ^ 70 + 1944342415183742333854987240459634654510274331517919211134789406132584) * 10 ^ 70 + 6653841705431619514900983990778386678824365435742492305774190417068481) * 10 ^ 70 + 5732001211851683950617893088295385500398215494564313941642322809469228

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_179 : Polynomial.coeff recurrence4Scalar2First 179 = -((((1216977439645 * 10 ^ 70 + 5243839027997053670059817198293458838473476894321533185707771924206761) * 10 ^ 70 + 4939232857579554418637088161704390583417098418158844397038152379868042) * 10 ^ 70 + 8140111853859234249941087014816752653226324062000542546424506231597460) * 10 ^ 70 + 6969007224226846501380558445586717862551038455960986157604564794136769)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_180 : Polynomial.coeff recurrence4Scalar2First 180 = (((3304985930460 * 10 ^ 70 + 6928809673796225910619795646817356104571011799174477478400062574758190) * 10 ^ 70 + 8237651788283101157170081724599457251539849156576188872261760585900991) * 10 ^ 70 + 9985846081225998513061623576657873992838892116597362748094292578322115) * 10 ^ 70 + 3064492200406854673452374179111833202200799276495659645756887788139460

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_181 : Polynomial.coeff recurrence4Scalar2First 181 = -((((8844655607596 * 10 ^ 70 + 5318281309700019213364584485452093609292664686970126110872136328117075) * 10 ^ 70 + 8702015821478119344709385703477103761370234088613810326085652575537631) * 10 ^ 70 + 6438618170748649195290583992228237866480297353968332557980182326346265) * 10 ^ 70 + 7685436698398295748196404679094215909293615089733891053602798012797835)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_182 : Polynomial.coeff recurrence4Scalar2First 182 = (((23325740408793 * 10 ^ 70 + 7594099256754098626449209084634365735572840959556672793256010514200820) * 10 ^ 70 + 5204882134129129130682840357970766071449790036358435638748915255672249) * 10 ^ 70 + 7101582098378375110042207437746499098635139552573288694410378765073819) * 10 ^ 70 + 5151621285005506072830453332550368451993558334533532196307977015859945

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_183 : Polynomial.coeff recurrence4Scalar2First 183 = -((((60624961457440 * 10 ^ 70 + 4963834766430232402961137348711543060844410846855263380216364168604376) * 10 ^ 70 + 9918206358947204739651237088824941782148324016837017518528397532181358) * 10 ^ 70 + 7451135053972781952817453264761814741656573962618005437276282695009574) * 10 ^ 70 + 7523093066970800702259217271627272775601793529381114353236247327194499)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_184 : Polynomial.coeff recurrence4Scalar2First 184 = (((155291157784187 * 10 ^ 70 + 4544780764725475732405744093625772266990748188116773455457636396140970) * 10 ^ 70 + 3694592304061184403155603844956071721243737749497326227449164900024092) * 10 ^ 70 + 3485671500022760634695014205974043499699664158165209868381719263503975) * 10 ^ 70 + 1592222361121353927956790956704658773232379696903698557061166850271792

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_185 : Polynomial.coeff recurrence4Scalar2First 185 = -((((392047105942178 * 10 ^ 70 + 395426612813609522725426840468881050348408208261300370832375794615971) * 10 ^ 70 + 1088512509043124102337963792832518550643010656988999755006398591389257) * 10 ^ 70 + 1598053122936816096557222696546503852985342363719131630693565719113907) * 10 ^ 70 + 9230144854491581746880193796800073439257774471274266884411299350547398)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_186 : Polynomial.coeff recurrence4Scalar2First 186 = (((975534159064079 * 10 ^ 70 + 4959396778396677078583870727045084629106975609247830031413050025059146) * 10 ^ 70 + 6782499945662050761007702103062506008406014359188513052149404068506536) * 10 ^ 70 + 279680266231875251915053373647399296099962014548595008144181055527714) * 10 ^ 70 + 8083659413601152710881075008032931293312306047468340771715276962507603

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_187 : Polynomial.coeff recurrence4Scalar2First 187 = -((((2392628261836013 * 10 ^ 70 + 7623090773876025342524437974913711316226890723141930513524614539451822) * 10 ^ 70 + 1513554665964531304152461253301551036329009663780435561845049165919301) * 10 ^ 70 + 1770628203515130674560515618328498248325937850385117285404465452375018) * 10 ^ 70 + 8264890779637394460699829062670032819329330553425669092379256227285388)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_188 : Polynomial.coeff recurrence4Scalar2First 188 = (((5784311788478297 * 10 ^ 70 + 1690801766450052672183496657122004079591048412592785529790744117402896) * 10 ^ 70 + 230972719401433777188999038273520623643394973293947062033984350497726) * 10 ^ 70 + 276314309791883733664952067204673156059582010061680719225788987330950) * 10 ^ 70 + 3608799108740181011257400077937424441374046493296155610833508220790487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_189 : Polynomial.coeff recurrence4Scalar2First 189 = -((((13784355699294081 * 10 ^ 70 + 7098034837858080183907528213773588034844922483177616616336842764405600) * 10 ^ 70 + 4792473673412787525395519003744757828263161929859648069437067056516569) * 10 ^ 70 + 49818726413331496666726111082654799703577859762493622188051709278936) * 10 ^ 70 + 8807023765411246781820134590315649429056614422309864156294020359381281)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_190 : Polynomial.coeff recurrence4Scalar2First 190 = (((32381245257927927 * 10 ^ 70 + 1442431716195842442647604874945403360262631911182250542828693290345601) * 10 ^ 70 + 9991093779441766926384830028332564654334709369376191182589353419475948) * 10 ^ 70 + 3588080426032654336749846338795794257425438641782933786020397728178427) * 10 ^ 70 + 4934090647519218347144556405981244608082034062014734241561042189895177

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_191 : Polynomial.coeff recurrence4Scalar2First 191 = -((((74987055983252408 * 10 ^ 70 + 1131905462800670697582743445084531651551889311916703998462830086331789) * 10 ^ 70 + 9703752717968123514954868346716178719303441591969887683137112650894854) * 10 ^ 70 + 3355495131088718369508634288791924264834591299853431226425446742106530) * 10 ^ 70 + 2861542584453833769206849149066729315347774416620992984392614148663635)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_192 : Polynomial.coeff recurrence4Scalar2First 192 = (((171189659646209543 * 10 ^ 70 + 3982270515015781570735378270264308397407631126718213676955567786481124) * 10 ^ 70 + 6024990305988771905653409808231902678648129206667467611693599167257415) * 10 ^ 70 + 4552773585463754586849360977724343485932899202492637307011133865356852) * 10 ^ 70 + 6035235044798203897402349728058178327403714734546725696481680122765035

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_193 : Polynomial.coeff recurrence4Scalar2First 193 = -((((385282610356699744 * 10 ^ 70 + 6894919657586028442132660137071710017695726301402184091196585566407978) * 10 ^ 70 + 6137156854058748564208989861621485670526017592437866449800163521985082) * 10 ^ 70 + 3953086457224612905464057537779855473045095169674371094700432563882758) * 10 ^ 70 + 5694466841624597864227978546765351716953251217848853734012850278682423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_194 : Polynomial.coeff recurrence4Scalar2First 194 = (((854876795581158144 * 10 ^ 70 + 4071526780779400870511258587126754126843932531848527850424670667258355) * 10 ^ 70 + 1369771757563277422912051366675587967576550648825356830408429843113477) * 10 ^ 70 + 1263838793786150158285163401124519678336092895380482969569545583521801) * 10 ^ 70 + 3940616591358084991380754134942431153553338838423086546854416325442673

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_195 : Polynomial.coeff recurrence4Scalar2First 195 = -((((1870082995272205631 * 10 ^ 70 + 4056800262556395233124358886959906183591321268586836450794939013041065) * 10 ^ 70 + 9754457871881064652705922238097529852889006594086415143445124902985971) * 10 ^ 70 + 2763837261621533550328668675371623119332246763445941089670947664847082) * 10 ^ 70 + 2188517084700853122879775248593147000748350478930512110995328152615616)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_196 : Polynomial.coeff recurrence4Scalar2First 196 = (((4033312316734543360 * 10 ^ 70 + 5603151527714262748869151652945642430456970406899161962680316279671863) * 10 ^ 70 + 9478942711152633874691493792963581176588931009681242019951093400348503) * 10 ^ 70 + 9734371260777055012840473972177555928474272296721296170515224191096581) * 10 ^ 70 + 2858557915258548796236059204922375882658092892213263549898288497490698

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_197 : Polynomial.coeff recurrence4Scalar2First 197 = -((((8576621173821210402 * 10 ^ 70 + 5445189167835915356057430683265476239156453547696800039138965402619066) * 10 ^ 70 + 5748183803729365226157079944704499829714099543567048352954836018410025) * 10 ^ 70 + 499387089506555317886574175441460961487830635144347084984099702890876) * 10 ^ 70 + 258004804830938869717738962959945228346476078938146848069972945812109)