Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_135 : Polynomial.coeff recurrence4Scalar1First 135 = -(((57688373631331675802272961329344138188138146323062393168 * 10 ^ 70 + 2427213202614100786826521684869297056500593045711023215651876350601032) * 10 ^ 70 + 8736250824155577877579237399418164760780339657639336980819071792411736) * 10 ^ 70 + 5295300498600935297021682407752596935593989294473790894964626007149803)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_136 : Polynomial.coeff recurrence4Scalar1First 136 = ((326331081614476619983418811630711980643716409969637560065 * 10 ^ 70 + 2957638663164903254818260761944343492408530911067451224235126622692107) * 10 ^ 70 + 3247295407049621090743268703477359231982380067339999003738962719188380) * 10 ^ 70 + 2591825587334240664602318295496310172517530028197398320762715592841215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_137 : Polynomial.coeff recurrence4Scalar1First 137 = -(((1811802804099962655069747366982639532658928086978106346978 * 10 ^ 70 + 4755005367071994146614965298205051248225107777539824177695702722759647) * 10 ^ 70 + 3274076434145088210112208306416733883668438872047456015636748958754914) * 10 ^ 70 + 2575785435428715224389999522900116354208694840715803221482210533965686)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_138 : Polynomial.coeff recurrence4Scalar1First 138 = ((9874471946000233980709942952109336434878424644672089327598 * 10 ^ 70 + 9253131836639057029471609154019430066229182328434038108913229646205365) * 10 ^ 70 + 279285171749563050668526585734511335663914379458680796042943273635344) * 10 ^ 70 + 7292798746595280611940282488467746810273357439398757669753116904778742

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_139 : Polynomial.coeff recurrence4Scalar1First 139 = -(((52836433757357793537788085392867175765072269355978637349932 * 10 ^ 70 + 1323973489620273511374309800632074907152028295516394889262678397928008) * 10 ^ 70 + 3176436841206711261368024421817085961812603482536743027682255537932511) * 10 ^ 70 + 2671622814217157356898705029256224665549471992706408445568209946321872)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_140 : Polynomial.coeff recurrence4Scalar1First 140 = ((277609370975637940516984627007792492356029634652774648005430 * 10 ^ 70 + 8303218029754268361781859829399742684687064506944602187258451164337510) * 10 ^ 70 + 8542990035202191261765068615963955492975904764910490917355865096136721) * 10 ^ 70 + 5431660246942779463033052987082819083387577059607664255730699895175229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_141 : Polynomial.coeff recurrence4Scalar1First 141 = -(((1432446186892163545980920052379456927679613935063600143634138 * 10 ^ 70 + 6492359074364340641531199732006450905261693228192632099319680891801097) * 10 ^ 70 + 2647469866980646646340803727013918121546990124289676053413210795262799) * 10 ^ 70 + 2211218082646058201054587734759237093160240581418007540127722490728093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_142 : Polynomial.coeff recurrence4Scalar1First 142 = ((7259837759778302680043559288763521635577585060824416996163736 * 10 ^ 70 + 9687372479484295114842605230000159321239602740371870582672147125522860) * 10 ^ 70 + 2820450664043908468529081604734844312570040969900271433345239754405715) * 10 ^ 70 + 8790197874602568292972162081105521989042665766028891431351845959786305

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_143 : Polynomial.coeff recurrence4Scalar1First 143 = -(((36144239877334468848595920293454821188808132049143533107020163 * 10 ^ 70 + 5015205203537719734976667695508387517917751173720188067403066667871706) * 10 ^ 70 + 6602265514666462608822415588826889367582380372119189119982362958557638) * 10 ^ 70 + 1133976293060081628845188060574209521512617463407492533429161698530490)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_144 : Polynomial.coeff recurrence4Scalar1First 144 = ((176795995796967319558097450036283058861719131596435137889356686 * 10 ^ 70 + 8008301066080474389210422937808397664028209705885263754910553292145125) * 10 ^ 70 + 5059523416206518242503238697510749103656124666746229244267072791984707) * 10 ^ 70 + 4257128264299692511527936444903607430465597556102465199097981352853238

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_145 : Polynomial.coeff recurrence4Scalar1First 145 = -(((849733839298766695255422624512645996109006411426551364351227898 * 10 ^ 70 + 4584932709322077269442922802933050193584649163818412206624184934397230) * 10 ^ 70 + 3821661168314631393824483827378599700681812909070802237407178262584768) * 10 ^ 70 + 6208331994334690496482414109055471990546081141997621858076914261300931)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_146 : Polynomial.coeff recurrence4Scalar1First 146 = ((4013516653152477121319941197478318760979907591057222145138788025 * 10 ^ 70 + 2066379588788019656215853053812889786769391718076155201308204682341696) * 10 ^ 70 + 8645448786827374854538943170583552739212449649823493945378604519635589) * 10 ^ 70 + 9032285498634739126448848872134624326651218607200413469163625871714192

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_147 : Polynomial.coeff recurrence4Scalar1First 147 = -(((18631676631160124036951687531340473344828177205321941318045714295 * 10 ^ 70 + 83523021328962529740708597788796126612339782255561466201609613858540) * 10 ^ 70 + 2362746593890759245473662171130431075670643728914571102575887712696866) * 10 ^ 70 + 6586469262908327754039064841029189378893840850192827331298225023488038)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_148 : Polynomial.coeff recurrence4Scalar1First 148 = ((85018835231421096668023663214355540159379215080747709424352796371 * 10 ^ 70 + 9294150747168670440853409924324259525539878190209045525569032678001926) * 10 ^ 70 + 8736484880374007365132425108800409128419062978531538490357891745572615) * 10 ^ 70 + 7072996809694191710029966594200975479923456300332180006417265805058642

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_149 : Polynomial.coeff recurrence4Scalar1First 149 = -(((381386191267867426044511262734948937255217743589106560279042281310 * 10 ^ 70 + 8143375200993869627616146014360499414163639290426239236181942100752038) * 10 ^ 70 + 7218267389117742173147063789565129363777682355093407644892312983125705) * 10 ^ 70 + 2266089036210426158208968212113416188729349808565046842088159758340558)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_150 : Polynomial.coeff recurrence4Scalar1First 150 = ((1682094157639884494037225621442543750660210597397170048629383867274 * 10 ^ 70 + 8671979419876510281468226484251697014614717323835257896402446049082841) * 10 ^ 70 + 1260859465230893401112165492334905202673380491890115355232982503877638) * 10 ^ 70 + 4951044870841440610596008826866288096974368613101423441075331337141933

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_151 : Polynomial.coeff recurrence4Scalar1First 151 = -(((7294890720916563859303346631688106889110751452099726894328657103107 * 10 ^ 70 + 8856324311623333698968951318559840948453836111150396284968553730596844) * 10 ^ 70 + 3109226592266269409062780706277530594152682407173304960755384212657209) * 10 ^ 70 + 1153069681618151252548756465793354871877463931985213801665069457676850)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_152 : Polynomial.coeff recurrence4Scalar1First 152 = ((31111202286538449944955261439643363952579006142318057064633887701533 * 10 ^ 70 + 2516797038628614828877462887503477159379129721695947540500415280679441) * 10 ^ 70 + 2125052472155339453424507868297301658371359693170140906753894248093210) * 10 ^ 70 + 7291703686053322913104133314068305418727835395653402378895853010509904

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_153 : Polynomial.coeff recurrence4Scalar1First 153 = -(((130493672846739412842273529336190190722315416107084450970504829019371 * 10 ^ 70 + 1903187464733736977809869613116506807562932039012920310300998366466318) * 10 ^ 70 + 3103841156520696528675127082762989606558149607489799141181707111762159) * 10 ^ 70 + 2582921524933124311127004507392933080858906108658992764574676706417822)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_154 : Polynomial.coeff recurrence4Scalar1First 154 = ((538369834346519325169379493854918168449798724385623817585710979103087 * 10 ^ 70 + 6272517397321164771791476104799979848508533770179494508625449178041116) * 10 ^ 70 + 1825896537665266200428621269302742653047728140250870972793366655940513) * 10 ^ 70 + 6245308504040193974433331468583476127007819281259498363924824362674731

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_155 : Polynomial.coeff recurrence4Scalar1First 155 = -(((2184909074503572199809609334314141311413078125761375073201425750410045 * 10 ^ 70 + 5442997063893502162930186125000049410451834012727779242187601514606412) * 10 ^ 70 + 4598937011148805022210468383654421192173774769543303667549354221898309) * 10 ^ 70 + 5057607585275853592186006628311159967979870672879607518487216639224654)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_156 : Polynomial.coeff recurrence4Scalar1First 156 = ((8723465758486117495419774032910021072094119248117952572584566488291493 * 10 ^ 70 + 5355815114459683619836599887509740231091431679012757756129262324182472) * 10 ^ 70 + 9732727116412660135653100844349646073399029003933467656643406774635526) * 10 ^ 70 + 6188212001946032194514265278644797053980891373793623147224527317476547

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_157 : Polynomial.coeff recurrence4Scalar1First 157 = -((((3 * 10 ^ 70 + 4267967489432985947352036652879780398100344783709120898747866831360610) * 10 ^ 70 + 2388625531819034686627146309992612034097519358921963400737158967269196) * 10 ^ 70 + 8382805989277702316812851987023113884310353068580494556567197600348163) * 10 ^ 70 + 1264127921663919184575675415646950091657028996341980667325326322841643)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_158 : Polynomial.coeff recurrence4Scalar1First 158 = (((13 * 10 ^ 70 + 2455715290548143982765684675426357714943521550086579731554295763552440) * 10 ^ 70 + 7751300376570718611327596037401537215205418484538906293057693173402842) * 10 ^ 70 + 655305930065700372288482100622968710084231274127926675344795096714734) * 10 ^ 70 + 5189300104729500877282881045950292492559730894510566302829624710377997

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_159 : Polynomial.coeff recurrence4Scalar1First 159 = -((((50 * 10 ^ 70 + 3819020184388137425672251607412449270496347068009738524854809391920369) * 10 ^ 70 + 610853847140297040655971508534072969282329828534607738967683995399556) * 10 ^ 70 + 8031386133294015807464318142528950034675384577266492102075782429483559) * 10 ^ 70 + 6054078248814978052950698298011016526743835001002240320528371631898344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_160 : Polynomial.coeff recurrence4Scalar1First 160 = (((188 * 10 ^ 70 + 5981051144336518103337076348631570389442958173832961158164136909101386) * 10 ^ 70 + 4486921723891906398347521859826185006966572617744977765154293230573797) * 10 ^ 70 + 3089507662092962800577923092672713642469148821040017610371046212816541) * 10 ^ 70 + 3988792303189554069242006383127842499304376097178892780475224909944463

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_161 : Polynomial.coeff recurrence4Scalar1First 161 = -((((694 * 10 ^ 70 + 8569611468916670466865635724903017699007332673583049011958060086661806) * 10 ^ 70 + 2970732491231334792850565994912749017164372070769984561830733521677783) * 10 ^ 70 + 1371541958763852296512146098484167228555198603873689422488892145794188) * 10 ^ 70 + 5769720048723013454012678394525386279197996925542437516185064886661100)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_162 : Polynomial.coeff recurrence4Scalar1First 162 = (((2519 * 10 ^ 70 + 9055455867315514481903928856497157986012014989200775968271312610575185) * 10 ^ 70 + 2039199791827158454446805462928367164010108767514568027277167447921028) * 10 ^ 70 + 5584427900511414345116766949971620013918970209359326125261741201795232) * 10 ^ 70 + 2978174567019601221037741190275672531901331266849038001769280158986255

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_163 : Polynomial.coeff recurrence4Scalar1First 163 = -((((8995 * 10 ^ 70 + 7704581856136851449615952889967925626601248908331356388173189758622967) * 10 ^ 70 + 1686973289191469859355323551314551833258737743761972888118338070186259) * 10 ^ 70 + 6421485465806721793805788211191444441346209930611656755346989705085673) * 10 ^ 70 + 3523674885449205906417244690206771804708968321257836898032599438520877)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_164 : Polynomial.coeff recurrence4Scalar1First 164 = (((31614 * 10 ^ 70 + 8617039373880430844286395647277597159439644419972955698240008109298803) * 10 ^ 70 + 1227574831977048611064694346285889362696236098496204275868840905600439) * 10 ^ 70 + 7914275127278653443423468435338617674389614666231659736212871538180200) * 10 ^ 70 + 1868883647083744865292156852180086107032669731535970017642499144101446

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_165 : Polynomial.coeff recurrence4Scalar1First 165 = -((((109389 * 10 ^ 70 + 5123863631919108133567584919745505719572927134462223152606640025294812) * 10 ^ 70 + 4161116086086867936038596467662502285069034846491262907577357064907358) * 10 ^ 70 + 2959784863232612530479303526578654167267744736605589992527359080459223) * 10 ^ 70 + 9366709071691576487432141947942338538336976669250155347670020398353767)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_166 : Polynomial.coeff recurrence4Scalar1First 166 = (((372669 * 10 ^ 70 + 638113284571282477956297995838104530146320848175217001957440012102365) * 10 ^ 70 + 6637128869538721454959657058052474761918295479986855052733840339209551) * 10 ^ 70 + 2204751348997537002288784782782484768990124929257903427276320366338930) * 10 ^ 70 + 9582925995584639091451763413929659961333913115772657883603790611657785

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_167 : Polynomial.coeff recurrence4Scalar1First 167 = -((((1250158 * 10 ^ 70 + 7593700921199363533315826430013491544716282471545741716385403184410587) * 10 ^ 70 + 3369059332269473661789267300209347175207882928631880630020718287075805) * 10 ^ 70 + 9526824134806112050993054969062886017674621360816872027577119737287428) * 10 ^ 70 + 1947487046997200421814006498185249979731162127345745990384541251104004)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_168 : Polynomial.coeff recurrence4Scalar1First 168 = (((4129821 * 10 ^ 70 + 565751418866779850329968749500210973959936367025398323117615145092064) * 10 ^ 70 + 739819954692473996217158928431096288434857724654192858505743477739361) * 10 ^ 70 + 227731389255940450205122724715533333926660272732214380296715378675696) * 10 ^ 70 + 8813887265003234576646737845147898794274527994919472290036426128389832

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_169 : Polynomial.coeff recurrence4Scalar1First 169 = -((((13435405 * 10 ^ 70 + 7537136954609990347489017200692624451693390861809719573653559014849505) * 10 ^ 70 + 5453209989373573093881375927414750429833968436800855470890797311201901) * 10 ^ 70 + 1414246776809663467353734150637642437157202765019585801840106595928992) * 10 ^ 70 + 8596968900838905484570132677906829603342420664095241124263658307722291)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_170 : Polynomial.coeff recurrence4Scalar1First 170 = (((43047929 * 10 ^ 70 + 3131165868554641397005368402516187585552207958524581760557583386589883) * 10 ^ 70 + 7042819105642659265381420639116216183876617249760696200447412044311777) * 10 ^ 70 + 4970151567202322057937521974609862877669199024025334672221494597487894) * 10 ^ 70 + 5377938626231457310282902299271655489757478866416011161237411760704392