Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_274 :
Polynomial.coeff recurrence2Scalar1Left 274 = (21055517629568190952699267792651781848915790188399982282409959748750 * 10 ^ 70 + 475089836201608082209637800593347577475663819733780149728045723526641) * 10 ^ 70 + 2577363889795556882222684272597949382354534378767366797687149481879325
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_275 :
Polynomial.coeff recurrence2Scalar1Left 275 = -((6094144413796805878799801645075398716530762957957187722289410249564 * 10 ^ 70 + 8600671964501807169763697782552831203046447471787476622332999340159294) * 10 ^ 70 + 1921902415404197666827773019034383971471538201797881146883253363892538)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_276 :
Polynomial.coeff recurrence2Scalar1Left 276 = (1165836880865001513293617551871954061383438086982592636163015250568 * 10 ^ 70 + 2496454647384411910387853008354946479630648008984292874660292170389190) * 10 ^ 70 + 8530966533609078654378822260737938727860502834661535664336446406706038
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_277 :
Polynomial.coeff recurrence2Scalar1Left 277 = (121544299068746842267414002476465437733591245358090991551151412304 * 10 ^ 70 + 5109160732124460119871100459479757820254412087850677616251661684229396) * 10 ^ 70 + 4456243132565516333616657497293264319083911310364638634609702654582729
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_278 :
Polynomial.coeff recurrence2Scalar1Left 278 = -((284574299530861078886686208081027859560970181398673861875894417807 * 10 ^ 70 + 942582729342548081779290439849460447539519708598194257438089698012652) * 10 ^ 70 + 8804429750464772736323088932819435245050830028290115687110279209806553)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_279 :
Polynomial.coeff recurrence2Scalar1Left 279 = (195295372457606685079411151693524559920405203363324370989796536421 * 10 ^ 70 + 7598690876371237925822959765126267658322245675846026674017268295425131) * 10 ^ 70 + 3326302165917122179397458976308670609084365167758318429098325468847202
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_280 :
Polynomial.coeff recurrence2Scalar1Left 280 = -((100982167587682916015998586375170859322484936537304320516466703727 * 10 ^ 70 + 3403271100618238143369389344051805924048723278153816896745563139724879) * 10 ^ 70 + 7604229452586044094999539328090662436874882952827114595050197841967826)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_281 :
Polynomial.coeff recurrence2Scalar1Left 281 = (44517022541602015104202659036063767558976966861665882582467276120 * 10 ^ 70 + 4341390025560278917290367501305892076699750190662237847760853650984762) * 10 ^ 70 + 9773222267977808026307789984046267765451204235224718285629723250435857
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_282 :
Polynomial.coeff recurrence2Scalar1Left 282 = -((17365366924748419294820806551176528388749491027712527542168240415 * 10 ^ 70 + 8865170387072461164846652607563934870473878396902065507567593082093687) * 10 ^ 70 + 535719870784663189496475224042370536815507090069005870445991179982542)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_283 :
Polynomial.coeff recurrence2Scalar1Left 283 = (6050096431335251644153674519749048550733291654688622945901014035 * 10 ^ 70 + 8212121701107258648738260973510981034929643524683596853672134833603538) * 10 ^ 70 + 9914040301473014223944740653506174265107429872918487867417782976708599
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_284 :
Polynomial.coeff recurrence2Scalar1Left 284 = -((1866800344328814394350698886943052844513386050403472658597833611 * 10 ^ 70 + 3109012576806640076269306438705724372564349706665242353718494455271007) * 10 ^ 70 + 6126011049167763297953913179480077357555994583092127600201808381046171)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_285 :
Polynomial.coeff recurrence2Scalar1Left 285 = (493551809768574292313670662765715791329444477677754605572893090 * 10 ^ 70 + 2563389364353323036265952044938552678806330225524870338177090209657285) * 10 ^ 70 + 8784219178549367050764816742196542210211432841697234587446615337561054
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_286 :
Polynomial.coeff recurrence2Scalar1Left 286 = -((101047753475421628158672885055993073752704684980817028857140366 * 10 ^ 70 + 5500953642112004386078794253548665437682414391985089888185548290913509) * 10 ^ 70 + 337678845983199700166154036043842720356387349822540138018788703189197)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_287 :
Polynomial.coeff recurrence2Scalar1Left 287 = (9138224297033329258716902775199048262964888222348302901581791 * 10 ^ 70 + 2224117565462249203258249959925032486985061824666300962687494522492031) * 10 ^ 70 + 2254295276396385097047318260980431548257799540865247490903843530787099
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_288 :
Polynomial.coeff recurrence2Scalar1Left 288 = (4840621586437811488852919244520877961933454960730966616591537 * 10 ^ 70 + 1968892108930800934909483946630452182223930867458817455052033384317002) * 10 ^ 70 + 7238153255165674041108270502212785927677064751026401778721879843767410
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_289 :
Polynomial.coeff recurrence2Scalar1Left 289 = -((3695647168258096054525608997002435648054875381453816593648262 * 10 ^ 70 + 7757537767956827836228602352793943895715320584108347521855211460141606) * 10 ^ 70 + 8553916776567103825089616306241608016134298997741786002365667397671381)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_290 :
Polynomial.coeff recurrence2Scalar1Left 290 = (1639842703302018965024805120735933355885698191574083156772586 * 10 ^ 70 + 6724115602254570038204047215512646744615374257008048246784131346619521) * 10 ^ 70 + 7590650678480884734742179686461517604555623444039888511315962980424195
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_291 :
Polynomial.coeff recurrence2Scalar1Left 291 = -((575777939635962422280987617703292202753179874784826149396464 * 10 ^ 70 + 90275007422439875482048763933543650171511875162508456043529123894876) * 10 ^ 70 + 4573371620103536460817977593047609486796285417597607228040251507387373)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_292 :
Polynomial.coeff recurrence2Scalar1Left 292 = (170278106061509030605728471545884782879730837263296639047000 * 10 ^ 70 + 2207286775779882111956491269241684451408138123495152766098309147192594) * 10 ^ 70 + 6103458231346223763656262337659963714559662182041121637259904684350153
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_293 :
Polynomial.coeff recurrence2Scalar1Left 293 = -((42536933925813190154153503647042851955069115442332366832008 * 10 ^ 70 + 5201155251488046597698584719808033260265660684407644193669153705093386) * 10 ^ 70 + 7400694824914488622345267996279742692048253886623075163807750695252242)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_294 :
Polynomial.coeff recurrence2Scalar1Left 294 = (8547255569011395160375176556697406932122609822960184917669 * 10 ^ 70 + 8709634069865947793050975209164411347734130790159492342646058150914339) * 10 ^ 70 + 3427141585064952743479146663690509551760736301237217057972067364315035
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_295 :
Polynomial.coeff recurrence2Scalar1Left 295 = -((1116670723557411746223029112756740310523245729005691338576 * 10 ^ 70 + 4129391326675228677143687846380308622613628100966879697319876841446997) * 10 ^ 70 + 9795407946447300260271415867152570394816289112852053486258346811629001)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_296 :
Polynomial.coeff recurrence2Scalar1Left 296 = -((57346061397437972357519173931352793710297942299134405910 * 10 ^ 70 + 7335466087029298099793225665163559307679853900499585008315381261129074) * 10 ^ 70 + 2325722056673912526456593835761331602980142424085891970204497043614178)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_297 :
Polynomial.coeff recurrence2Scalar1Left 297 = (100335536818710936982120972167691196318478802573547538043 * 10 ^ 70 + 2718778939931598436692128670307699891153411813220630747020076682587970) * 10 ^ 70 + 8869902473094196423110943628621517992966394979025180148399561300686524
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_298 :
Polynomial.coeff recurrence2Scalar1Left 298 = -((41731294986354804459782994994619833827156437878890368146 * 10 ^ 70 + 1973518903926542672431780610754864066371429478747909428099552046371471) * 10 ^ 70 + 1940354719188576781885562581563173182436729913760724058799817878861832)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_299 :
Polynomial.coeff recurrence2Scalar1Left 299 = (12296672402587081317962604475461544545397292227497871873 * 10 ^ 70 + 642134431484620195975559622395904344135750383078002419513312247916834) * 10 ^ 70 + 8781957015233609525152019649033392706936988506597155157268765392657462
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_300 :
Polynomial.coeff recurrence2Scalar1Left 300 = -((2849262658949844923188744913756131818787811052553961714 * 10 ^ 70 + 760366221475146724834971551903033875216139269272436357263624902426171) * 10 ^ 70 + 1975011546952965613634618028764204369962197515665891442207558287418967)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_301 :
Polynomial.coeff recurrence2Scalar1Left 301 = (503878432383144652859784802042196423807690671024216228 * 10 ^ 70 + 5852021464441120445375472694151040239958705532795133653285098120166104) * 10 ^ 70 + 5404769039557794901340067562297834558800624430567614773409823702979478
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_302 :
Polynomial.coeff recurrence2Scalar1Left 302 = -((51636171412378848378233127251526425694089147406226764 * 10 ^ 70 + 9139675155071533486210261034502121631057074326131149721341332984448393) * 10 ^ 70 + 104512917658395826896099704867945436228943979433749488701350188345470)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_303 :
Polynomial.coeff recurrence2Scalar1Left 303 = -((5984983092154620320400095622173454888187897622155843 * 10 ^ 70 + 3989199740342495796824089974547763402578522944693623468622342810217560) * 10 ^ 70 + 7330222088962003750071912802612146985759488725720976395913010565122681)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_304 :
Polynomial.coeff recurrence2Scalar1Left 304 = (5111161000820839736465909427883080938607750409601306 * 10 ^ 70 + 423031268774651322690761821830873650206946319348490331221926195901151) * 10 ^ 70 + 8375354949782978709222729204675304308715128674097692607466889234367639
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_305 :
Polynomial.coeff recurrence2Scalar1Left 305 = -((1730634444651650483716661532653303383111576206836360 * 10 ^ 70 + 8046024249901494594952971154024050294136725409555909369268211544952661) * 10 ^ 70 + 2848048496745583565090905063134453742141557322051903155808607482603198)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_306 :
Polynomial.coeff recurrence2Scalar1Left 306 = (429699300398752270133578731083145366975836063752356 * 10 ^ 70 + 8758309891133314629297694052695753437743458319080081385889785840457477) * 10 ^ 70 + 2899688119590769543862955099860241756499597947470732549007673202996742