Recurrence 2 lookup certificate: Scalar0Left 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.recurrence2Scalar0Left_coeff_309 :
Polynomial.coeff recurrence2Scalar0Left 309 = -((712962873099537560374187841228764282319280473690977 * 10 ^ 70 + 8844435594556174377119947966475031016773457264354599616965564776345761) * 10 ^ 70 + 3878244708157871164715832310740781631386036021628251059131907382503343)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_310 :
Polynomial.coeff recurrence2Scalar0Left 310 = -((12264364436915593515187237120153698001495300200604 * 10 ^ 70 + 2743533861390257399537049213284567280760775492337117375202076785018530) * 10 ^ 70 + 9026657986236607194756109683053713376067593848029322600709847713270527)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_311 :
Polynomial.coeff recurrence2Scalar0Left 311 = (26733877445043090053021017976408944130743120178293 * 10 ^ 70 + 4100997798023990539952999158928308610507151661407259264101288766864363) * 10 ^ 70 + 4657848271894697582576087627609768677274038072354397412718657038363097
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_312 :
Polynomial.coeff recurrence2Scalar0Left 312 = -((8284550868544655167606285717090721499841659087872 * 10 ^ 70 + 8553969551543811383594166751989606324898507024330137071154641697864304) * 10 ^ 70 + 4521720802511470759656454347398224507254777927888718815236188329858526)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_313 :
Polynomial.coeff recurrence2Scalar0Left 313 = (1847661331918508174561333732266335081642824243033 * 10 ^ 70 + 3411232299387669555955080798968493084022330403273502369300864140471732) * 10 ^ 70 + 7196925113096043949495976517629522302954577924991412161948948597834381
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_314 :
Polynomial.coeff recurrence2Scalar0Left 314 = -((343175472794464526948799310473127807372768033169 * 10 ^ 70 + 8536561665142901897258323792833130790607352747884312823942444193990836) * 10 ^ 70 + 2088878704761916281836484094765725530916756804313926221134943669434418)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_315 :
Polynomial.coeff recurrence2Scalar0Left 315 = (55379129825453295911318901353116781182489827066 * 10 ^ 70 + 7737382595968321927352926688470191433237770111919880575765727674316044) * 10 ^ 70 + 4300372748600282266911781495921864504471037688373206026185942658721875
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_316 :
Polynomial.coeff recurrence2Scalar0Left 316 = -((7848291173427261641914610215848601839396637977 * 10 ^ 70 + 6657213134710602827204356482840337282497564280355895242107197005353812) * 10 ^ 70 + 9489133861135769802741738501928944995986508416939122327312632358651350)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_317 :
Polynomial.coeff recurrence2Scalar0Left 317 = (967339076056192062211058122078539914301116190 * 10 ^ 70 + 8105579500496733652365268416571111167319830131054130131763124993298588) * 10 ^ 70 + 8890700381039839384807475711664219132209697957940384258436264394975133
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_318 :
Polynomial.coeff recurrence2Scalar0Left 318 = -((99556399345891246265946547571755902815731541 * 10 ^ 70 + 463820928499923380432893812899084716164023371785671644790090478987543) * 10 ^ 70 + 5444407229391590149292198701044284688555873468864665753224027394435623)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_319 :
Polynomial.coeff recurrence2Scalar0Left 319 = (7443756064830287147589435292702190514737787 * 10 ^ 70 + 4394201308646465426984484099909496562849582666951522786501526625128811) * 10 ^ 70 + 2169328829767090274396548866729798221869534125936263849731266046383161
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_320 :
Polynomial.coeff recurrence2Scalar0Left 320 = -((107574314259787404500494314479812290076573 * 10 ^ 70 + 3001304442184782888327447980237589917983853435940566654567594266958601) * 10 ^ 70 + 6227117309777665479919706882606208063015001407030354830474632630678632)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_321 :
Polynomial.coeff recurrence2Scalar0Left 321 = -((94603000283693962999864298631117375336937 * 10 ^ 70 + 9454768483480598774936618943310160961736550709081779549042088112339919) * 10 ^ 70 + 9429496421633346259938502293813117126480725130935985940007893919498699)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_322 :
Polynomial.coeff recurrence2Scalar0Left 322 = (23126533298365890953945634367788197400776 * 10 ^ 70 + 7445132615917295443803174991084436146216592866757280749199427365957789) * 10 ^ 70 + 2604970998308944474207423949269803473521351242127934245215308930615927
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_323 :
Polynomial.coeff recurrence2Scalar0Left 323 = -((3717451970750719365740929602494948098318 * 10 ^ 70 + 6758118429903228123122238781622899638157199851159284578588670054574380) * 10 ^ 70 + 4153082109016000596114459757357276880976677420201401918119551276383960)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_324 :
Polynomial.coeff recurrence2Scalar0Left 324 = (474060458432510695705727790452460784489 * 10 ^ 70 + 6155295560804926434504721916807468441373796857746052545933325578286793) * 10 ^ 70 + 6609330451247941504628306834339755244743564364661327974211062427043778
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_325 :
Polynomial.coeff recurrence2Scalar0Left 325 = -((49360163516387917409765693543920757769 * 10 ^ 70 + 2104021297921792757407451521636766213115234226029001072003281473315959) * 10 ^ 70 + 7189518213979376708822454150224703040994915825013694228152213663752883)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_326 :
Polynomial.coeff recurrence2Scalar0Left 326 = (4031095699685929672625689051365031035 * 10 ^ 70 + 4824021659353191184655637806680214463644384721421253585730357502020532) * 10 ^ 70 + 1691180267720746117866822102808071189329062760343341151211698284013854
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_327 :
Polynomial.coeff recurrence2Scalar0Left 327 = -((212574222187937997110349061246290100 * 10 ^ 70 + 3501441487244692224632336449808558032945578950293488978242022951402526) * 10 ^ 70 + 284803163143519144381546828018071511068755358798978356637862516140147)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_328 :
Polynomial.coeff recurrence2Scalar0Left 328 = -((2436934416261168005066180035820634 * 10 ^ 70 + 2630656957700349934270667193710056115478107002674296362399644364983244) * 10 ^ 70 + 573694522727805195878450148935724382762932668052598611460951328064221)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_329 :
Polynomial.coeff recurrence2Scalar0Left 329 = (2276908397891162044679189310621014 * 10 ^ 70 + 6126982286713715086390827577259747607972033425252759194016393514018837) * 10 ^ 70 + 6860994693743217238154894172634298169503903181436789788736598608808257
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_330 :
Polynomial.coeff recurrence2Scalar0Left 330 = -((328000199020455480878410794994615 * 10 ^ 70 + 3692697383158801701402553091457179087564818913499410786153256336582757) * 10 ^ 70 + 8079795598906857969362026880416043431137248363520187503777367091600876)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_331 :
Polynomial.coeff recurrence2Scalar0Left 331 = (30289266453481083047987681683454 * 10 ^ 70 + 5192420908923345793156829412041193299613796573109532801435206422163705) * 10 ^ 70 + 5372187810326948069233029169685778983229762777549408266159037306220983
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_332 :
Polynomial.coeff recurrence2Scalar0Left 332 = -((1877565466017358150315406870413 * 10 ^ 70 + 7273303939825340610418376311756744358292752115165034450585943070175148) * 10 ^ 70 + 8257061776693460194594414820571144426548417441928390198756959519416086)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_333 :
Polynomial.coeff recurrence2Scalar0Left 333 = (51938218172851430573973218944 * 10 ^ 70 + 3734634440296300047667437339967947488398274928824318803216079386252584) * 10 ^ 70 + 5453058312934622657510530499717464378816205687491223394394429257144562
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_334 :
Polynomial.coeff recurrence2Scalar0Left 334 = (4327438710950299821951868937 * 10 ^ 70 + 6275307830457282291960176288274549536381271987301728466326310201585977) * 10 ^ 70 + 3760307617089374523917652358800626377789343760162407225801574246992400
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_335 :
Polynomial.coeff recurrence2Scalar0Left 335 = -((750476104334396943556657867 * 10 ^ 70 + 731026664822022661757592555010043023592035214684071840974833056698808) * 10 ^ 70 + 2401350957728846956928751263665522803281105561229929656231076677245003)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_336 :
Polynomial.coeff recurrence2Scalar0Left 336 = (59347853580521987605126635 * 10 ^ 70 + 9519826663423166588735270623665825457166513954421685688285332307700541) * 10 ^ 70 + 4895429556879968398805332066564666493610408152135351864165148495156127
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_337 :
Polynomial.coeff recurrence2Scalar0Left 337 = -((2796558143084206163998519 * 10 ^ 70 + 2622771000069686896847216048190250143206818177069275064117842848333427) * 10 ^ 70 + 7631400923800996633581841992312825764285146993775564580086410533846337)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_338 :
Polynomial.coeff recurrence2Scalar0Left 338 = (44178320123045435906191 * 10 ^ 70 + 6832291671091440564004707608711961340793807484898927781596068750480387) * 10 ^ 70 + 3637859132658620029497639542782192505526812275228568339421168931166087
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_339 :
Polynomial.coeff recurrence2Scalar0Left 339 = (4907344720404843491479 * 10 ^ 70 + 2743351997742545161632276194934237692924151732699024294891025351691799) * 10 ^ 70 + 6139367732896310915435009285816852099394904218441565639006227746178427
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_340 :
Polynomial.coeff recurrence2Scalar0Left 340 = -((494219462829885113804 * 10 ^ 70 + 7429452543483805472558517225927060119489932739701429870198869003891746) * 10 ^ 70 + 2534906102650049350828980787342221750105745227377991754775398638904305)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_341 :
Polynomial.coeff recurrence2Scalar0Left 341 = (23516903397011475492 * 10 ^ 70 + 9814022138006174367482648981675391700452341334182933987821210760582501) * 10 ^ 70 + 8578556763017035651396329290299390289381779860404483932413620857653341
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_342 :
Polynomial.coeff recurrence2Scalar0Left 342 = -((550568247034722056 * 10 ^ 70 + 2684324187440794783439940547229206780731207105480609615034309092966226) * 10 ^ 70 + 1701707854510239589028277453647529759293905323336564497709692377505697)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_343 :
Polynomial.coeff recurrence2Scalar0Left 343 = -((5732490478757103 * 10 ^ 70 + 8633932084050728484170110615688300161123979792218303911581298124673250) * 10 ^ 70 + 7925498374039214318693934792690873538806289250127551625490336932771063)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_344 :
Polynomial.coeff recurrence2Scalar0Left 344 = (991165877872832 * 10 ^ 70 + 821429387209375484822415480441219272011214143188471053806466308295721) * 10 ^ 70 + 718322112443478334898250270964540816191941883826103683253968232599781
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Left_coeff_345 :
Polynomial.coeff recurrence2Scalar0Left 345 = -((37460510214738 * 10 ^ 70 + 1914458488732155291162844510124718789850432698854440119330637323173312) * 10 ^ 70 + 5782222826185269523623708409991914956338366303387753575295715294508986)