Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar4LeftPart0.Coefficients141To185

Recurrence 2 lookup certificate: Scalar4Left 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.recurrence2Scalar4Left_coeff_141 :
Polynomial.coeff recurrence2Scalar4Left 141 = (43886235980854821754821154885988881 * 10 ^ 70 + 3161588410774097564634156194046218065021168621761663292310760216586904) * 10 ^ 70 + 40693833354824169555193406470037593046316059988821867876909628079161
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_142 :
Polynomial.coeff recurrence2Scalar4Left 142 = -((47961917039214965160427338289058468 * 10 ^ 70 + 3919506867417923249372834421185725870011745276751426384591043437053549) * 10 ^ 70 + 9044668638176510951608491298570365101328577510081821414782836631196114)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_143 :
Polynomial.coeff recurrence2Scalar4Left 143 = -((423186580490919511151734353116647072 * 10 ^ 70 + 7976305021074112228700125692126543207048395746945503942387848032197882) * 10 ^ 70 + 8871300997941545039852296753376411360037347978539294967661439142682609)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_144 :
Polynomial.coeff recurrence2Scalar4Left 144 = (2023155248354868351355587285156572075 * 10 ^ 70 + 4884372143122318941832521086375589632769905475830640389169226549293436) * 10 ^ 70 + 9366945050052385132298820151286886873138789480843014047685297703518228
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_145 :
Polynomial.coeff recurrence2Scalar4Left 145 = -((1134086474517799524630003660133573024 * 10 ^ 70 + 791645750594411997848101336559458368327371848122928291336711731391272) * 10 ^ 70 + 751278205749629430337096856800404969663187786337026695493262805021966)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_146 :
Polynomial.coeff recurrence2Scalar4Left 146 = -((22110752005525530241212165658307786385 * 10 ^ 70 + 1848163292687920337356111786523282469584540284747178390647900874023788) * 10 ^ 70 + 7860181527433204922056698109351730427405287644130629263175065844072903)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_147 :
Polynomial.coeff recurrence2Scalar4Left 147 = (84086394949574660032975700606475689665 * 10 ^ 70 + 7376895011745317975646298871030439380676923418186338736350170648870930) * 10 ^ 70 + 6168772018030592902963427207615639518683213324978974565854652238997496
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_148 :
Polynomial.coeff recurrence2Scalar4Left 148 = (19030239086501714855346587319795399690 * 10 ^ 70 + 89251001301894383493119235165142783285452574844560003136073906707868) * 10 ^ 70 + 845941435744947391025980858002013463696455990014391815612846114724038
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_149 :
Polynomial.coeff recurrence2Scalar4Left 149 = -((1152646211265298055523698385065082399747 * 10 ^ 70 + 5675792620965682501920294636130788633156816199044135035028902958349361) * 10 ^ 70 + 5248316321436094543030351493870614944150882891908213936281585470942768)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_150 :
Polynomial.coeff recurrence2Scalar4Left 150 = (3488809287594225980100346116583649755388 * 10 ^ 70 + 5362042784332438194052717636204380765654376431347046199908763362551906) * 10 ^ 70 + 1291836465334437341633893201403415321021553747437385487293612764498704
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_151 :
Polynomial.coeff recurrence2Scalar4Left 151 = (3691120595969250517862542997146589302571 * 10 ^ 70 + 2821173629571587207249960563444493652133377684865377088440015321980150) * 10 ^ 70 + 8088840705398153244977220619392960113578448971325063436395978330582962
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_152 :
Polynomial.coeff recurrence2Scalar4Left 152 = -((59356012823588566275641733107201565038180 * 10 ^ 70 + 9531209901176503255301905046465229424569308204877310986105593665873935) * 10 ^ 70 + 1111051712037449483764197423959800059200245566532740558297728497964933)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_153 :
Polynomial.coeff recurrence2Scalar4Left 153 = (162205208915403929653617191810771875037183 * 10 ^ 70 + 6503525016215698603743652654428883045135716460080680349239756488592115) * 10 ^ 70 + 170085243040418535249029985068427904831360662149131920465323171604082
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_154 :
Polynomial.coeff recurrence2Scalar4Left 154 = (184484120363571790395532168863970735187704 * 10 ^ 70 + 9113678719400519422922495873190272559979817115220823368993016563273086) * 10 ^ 70 + 9362515525109531578678965313749295946580072882436146967771536626761257
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_155 :
Polynomial.coeff recurrence2Scalar4Left 155 = -((2750637285253598605453399906689973701197065 * 10 ^ 70 + 1837974658454399255386477863519728837914161952172645210650475587508568) * 10 ^ 70 + 2792664146065191024454584588207824814173499337295300121832396697716531)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_156 :
Polynomial.coeff recurrence2Scalar4Left 156 = (7937907304371841097827554388151839247667749 * 10 ^ 70 + 2966591634437003083557539860245941298278181314644225461446333962313536) * 10 ^ 70 + 1280155989915309489772028385300320551490502649466260473331861889258512
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_157 :
Polynomial.coeff recurrence2Scalar4Left 157 = (3716394600907540583604121411683579062354679 * 10 ^ 70 + 5472222306048290346240776200283877202475943906239200461633566904911019) * 10 ^ 70 + 1052686496773699869041851118250476628873059477377435615744387583064336
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_158 :
Polynomial.coeff recurrence2Scalar4Left 158 = -((107909514947551584099607675338699703792978165 * 10 ^ 70 + 5033570539982971392803600894332614938642346398734415228860332123187237) * 10 ^ 70 + 1733717116062920093634991920876412039519162277646385002534564873676681)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_159 :
Polynomial.coeff recurrence2Scalar4Left 159 = (362046759673773106128143270428309188097888746 * 10 ^ 70 + 8384240027524053392507395988975833349617888679988026623028260472919572) * 10 ^ 70 + 6223238741879188236173422507695046951475954918957695373081916892389173
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_160 :
Polynomial.coeff recurrence2Scalar4Left 160 = -((143744135169124506820509696818796067723042129 * 10 ^ 70 + 7350686398735372726440324168179295916058365304748149592131166057320834) * 10 ^ 70 + 4747711864899158015680085832012198407275598682158514900712913702940528)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_161 :
Polynomial.coeff recurrence2Scalar4Left 161 = -((3430935731897317067368722610176726410787984558 * 10 ^ 70 + 3598648487153604254816243012411012183563791637857005401317038372203093) * 10 ^ 70 + 8846825433422899224974766935011877261862812690709478931181778547388882)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_162 :
Polynomial.coeff recurrence2Scalar4Left 162 = (14314145447881452826295458900853761996954786714 * 10 ^ 70 + 6155936712724919412498353802876699351157740760829283443065474538334901) * 10 ^ 70 + 4672639511936085733169872327323540774658269992016623651790690838572719
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_163 :
Polynomial.coeff recurrence2Scalar4Left 163 = -((17215159279104187118593767092012485116660633363 * 10 ^ 70 + 6429083218019836491905769919692890815980392040849039030398207763757776) * 10 ^ 70 + 9629694160808283358764288843260914767421370155213280449775162188555549)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_164 :
Polynomial.coeff recurrence2Scalar4Left 164 = -((82985856118093275622980456589221000788652426847 * 10 ^ 70 + 5242298366313574022589415382981853220029974165427914712462309743424629) * 10 ^ 70 + 489659050096070214790978411791104285036471901241365253648286076989138)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_165 :
Polynomial.coeff recurrence2Scalar4Left 165 = (478973487238661385658073099470157747211623594479 * 10 ^ 70 + 158611186654498514673304504645520394563965511663878179232466262169324) * 10 ^ 70 + 6784193925707764666556795638950534004669252526876047258848218223893879
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_166 :
Polynomial.coeff recurrence2Scalar4Left 166 = -((943846181480528333816212225137081644254918324047 * 10 ^ 70 + 1096832959011199483204311579837364271051978722077372123571709397696165) * 10 ^ 70 + 7330325602601859336714123533273684058399688071512166315108290635079919)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_167 :
Polynomial.coeff recurrence2Scalar4Left 167 = -((1177263971484134200742054739801034695455967752827 * 10 ^ 70 + 1079812441308948497361728021802906523513996678458036208148040542780263) * 10 ^ 70 + 3523503974653972417267125397923126606496049164616281907247389165038009)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_168 :
Polynomial.coeff recurrence2Scalar4Left 168 = (13338385552444384851869141872638977088674115703057 * 10 ^ 70 + 163023392348896429906455106916096463250914293045152057239132747252295) * 10 ^ 70 + 2551672661082386114203206021715392563065907693127390045761985131977953
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_169 :
Polynomial.coeff recurrence2Scalar4Left 169 = -((37979896281591786772564534680682588304940843096671 * 10 ^ 70 + 9948199555082672235704218444749361455784669819275718860499934733773170) * 10 ^ 70 + 1176243502617786154809950024319158919107091259084768553540165368053019)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_170 :
Polynomial.coeff recurrence2Scalar4Left 170 = (16263695733934571592531681281430319925735165392871 * 10 ^ 70 + 4321787044914537598204363813522557419896463812499629095744499175263399) * 10 ^ 70 + 5115176822724786324134945257336060987593143445968496913817436071529407
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_171 :
Polynomial.coeff recurrence2Scalar4Left 171 = (286944791261925270779768795125868463070235714779998 * 10 ^ 70 + 6109577591419549744201803592768889996401150534935306070225885812025831) * 10 ^ 70 + 6651305979154359954263137942637450977226820140511849008980999439209663
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_172 :
Polynomial.coeff recurrence2Scalar4Left 172 = -((1208862559061915942560483517415666402254076955894127 * 10 ^ 70 + 2022606332133481180823780748351958219267015277249387418401044771947644) * 10 ^ 70 + 4376583745198986899471248078253452081109311200634954973810984020734947)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_173 :
Polynomial.coeff recurrence2Scalar4Left 173 = (1944649495381908230751871555470610628689982373686726 * 10 ^ 70 + 2311815590192251769053786790570029315890800683166041814350560100608291) * 10 ^ 70 + 8628569647439590186811314863482528879088910523112751664866587153304222
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_174 :
Polynomial.coeff recurrence2Scalar4Left 174 = (3310043034431278706132791349508831970130291970377013 * 10 ^ 70 + 3784312701604503486396895183005522266789538435656311609519367104650450) * 10 ^ 70 + 2279669670603707463436379976324633042642623024086923573005431124279432
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_175 :
Polynomial.coeff recurrence2Scalar4Left 175 = -((29061050217685026169877826640027394948860171141597404 * 10 ^ 70 + 7277660562960406941743413635955631688392335628862656522672681486832388) * 10 ^ 70 + 2127343978106603247628682619067864606451602924025835890297432385277675)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_176 :
Polynomial.coeff recurrence2Scalar4Left 176 = (80825932310029386705821028756098804614795735037079068 * 10 ^ 70 + 4085109126660501332869830315525943721125271612726280554321638432475411) * 10 ^ 70 + 3021652844204206490032054976489382734493840688875591958910255211603098
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_177 :
Polynomial.coeff recurrence2Scalar4Left 177 = -((61970203960130356132636825075908766614562126517586612 * 10 ^ 70 + 4876554090696777156001916193836856149248949267382987813406093841068468) * 10 ^ 70 + 4482815863403884914568746737446165959388232385865736227674537947815581)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_178 :
Polynomial.coeff recurrence2Scalar4Left 178 = -((426087980785212255659370950123505758694131086019762168 * 10 ^ 70 + 6684490784841802762298083783306112889597781633274850221029535925591314) * 10 ^ 70 + 7415414294079044882849891806252066165271151665992027294453487206054109)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_179 :
Polynomial.coeff recurrence2Scalar4Left 179 = (2098395723081014029648560913694401880597755219555454633 * 10 ^ 70 + 6055684643016852534480475299517296517559097131702814217458639220629342) * 10 ^ 70 + 8695655559960289536625130173431011498896002241059128918111888579755700
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_180 :
Polynomial.coeff recurrence2Scalar4Left 180 = -((4548310284950352531535502164462727678752003103018853255 * 10 ^ 70 + 8910352023674990250774479966830806257240171688222449793989232974886566) * 10 ^ 70 + 2894028945952269975696267998066321314447263964873669689682607294730213)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_181 :
Polynomial.coeff recurrence2Scalar4Left 181 = (930650417028740722153572982980585055506137209729230118 * 10 ^ 70 + 9941868031456872276531526909954051170662821157423594792351393160202450) * 10 ^ 70 + 9805627973980275765636957004668318501493169790655660030125051308581598
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_182 :
Polynomial.coeff recurrence2Scalar4Left 182 = (30985261269171846391695202295104082774271385064874635563 * 10 ^ 70 + 6593695642197639137334378812284003164320300457882700590438043821519630) * 10 ^ 70 + 8470215367710283775064876798475571257300135570571940031442938149520675
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_183 :
Polynomial.coeff recurrence2Scalar4Left 183 = -((123819398060667256963134803376031425418983013355495633838 * 10 ^ 70 + 2368927255270219720139657370663425099710489451490048545627709334438177) * 10 ^ 70 + 5858707677040474769943149758830197859640607974994746229614190136786971)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_184 :
Polynomial.coeff recurrence2Scalar4Left 184 = (240675603875707876309311350996783298829195105055060281530 * 10 ^ 70 + 2221521732625550731739786859486467723487335352708003341356401305042033) * 10 ^ 70 + 1219322979791680560319581526628695072615651550819343993209444122649605
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_185 :
Polynomial.coeff recurrence2Scalar4Left 185 = -((19061527746200405627412436892680053291234266644377944787 * 10 ^ 70 + 1757302780837601444609218649191323100561269200624478351501461013420924) * 10 ^ 70 + 9936066401481808488360429887187074968710222987563222542464987081514290)