Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0LeftPart2.Coefficients408To435

Recurrence 5 lookup certificate: Scalar0Left coefficient convolution #

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_408 :

Polynomial.coeff recurrence5Scalar0Left 408 = -((((7061474289590 * 10 ^ 70 + 2610821083699713490259124417723726358539770117189007022780006062987749) * 10 ^ 70 + 7122660353602284555119052869587165923948603811572746513252383468763433) * 10 ^ 70 + 6508377885701753512479348309697656606426526031551011020460648488455827) * 10 ^ 70 + 472986651893834724401832254422942130029084318135379555644903441479667)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_409 :

Polynomial.coeff recurrence5Scalar0Left 409 = (((1029872966912 * 10 ^ 70 + 6296382449249277899264551311016924574555419754176922227571722516128969) * 10 ^ 70 + 5437118328121070207478686430753648694524362717326851667671107938427889) * 10 ^ 70 + 9477350209753963222478769371134480972250490246632977601372281353153217) * 10 ^ 70 + 9414656423006167547469621147343697506066219704849135409118991750179374

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_410 :

Polynomial.coeff recurrence5Scalar0Left 410 = -((((92865929598 * 10 ^ 70 + 400599713257677854349590050744368288217193266649429572476250851916453) * 10 ^ 70 + 6474557531719245722031219932879773305505230722823364010866995695646093) * 10 ^ 70 + 9854100258863312510332391479747332134634521130529821755467771390594719) * 10 ^ 70 + 7416377611676288773742656950378324629753468699148493836375909823879797)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_411 :

Polynomial.coeff recurrence5Scalar0Left 411 = -((((1152200656 * 10 ^ 70 + 3881802288937651878840302391971708018014845064345799038945646746813725) * 10 ^ 70 + 9182873912017559509592893165195770704820295231640517945453547665816503) * 10 ^ 70 + 1245570480512740668032149507708713338123659856246562965516402206246174) * 10 ^ 70 + 4797871442604470131951907685614434191209542531120922065168530749450007)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_412 :

Polynomial.coeff recurrence5Scalar0Left 412 = (((2524651511 * 10 ^ 70 + 4130074554570111952283289485971518826873394101903998687211430260390460) * 10 ^ 70 + 1722257029663482119323428992393624974466972412848520711815724742180788) * 10 ^ 70 + 8287189973696206286246186523949204858977084002467692172931451043259457) * 10 ^ 70 + 6215087939845551804301141685800238802319294783343044514154642152500749

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_413 :

Polynomial.coeff recurrence5Scalar0Left 413 = -((((638310567 * 10 ^ 70 + 6122092340130939485871303338035216917127282951545208967555709972057015) * 10 ^ 70 + 814954586266498654614933237857028968423117441787774966241476305574111) * 10 ^ 70 + 5321422040409743629871567445224286386895748252023936766942886721421176) * 10 ^ 70 + 490101822494893283514395398140706697201471991215408627460489558247022)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_414 :

Polynomial.coeff recurrence5Scalar0Left 414 = (((113827928 * 10 ^ 70 + 225432001097598550923196681209563380143905863401611403624787321275968) * 10 ^ 70 + 9103888784320746046604251876633355395953918852719214313666203378631211) * 10 ^ 70 + 4884099639041410232523648433473199620753717459138323642551892825026785) * 10 ^ 70 + 716210572063767096350125666377231821088429559100432828333267371643259

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_415 :

Polynomial.coeff recurrence5Scalar0Left 415 = -((((16901583 * 10 ^ 70 + 8695856372281827412129982618241077394149711198589395472782505509468782) * 10 ^ 70 + 9965409011616218797995273889430164028658990332830997051402703933954266) * 10 ^ 70 + 2583517360326776795598047801148249695307338403603793342766939981194683) * 10 ^ 70 + 9038314185420151957015023396626191781788538654526119379122768031139370)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_416 :

Polynomial.coeff recurrence5Scalar0Left 416 = (((2174900 * 10 ^ 70 + 1496857954204612922369599158850109340938202168592692127735727568715722) * 10 ^ 70 + 4532941644610152606285257674353768667552840798186844760193293105457390) * 10 ^ 70 + 5586189648684935306586955102447920074337695105790226386327916834060155) * 10 ^ 70 + 6414882894426311484898167376527865949338931016928073247271335747842083

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_417 :

Polynomial.coeff recurrence5Scalar0Left 417 = -((((233966 * 10 ^ 70 + 4174573487741795494116832407489896351034040097147296518060123877510571) * 10 ^ 70 + 8424710578264653169024583908147017823708748887103712037760960005445002) * 10 ^ 70 + 5775260290463826810613995783311729296162175577945873413661025315564564) * 10 ^ 70 + 4179716141619744995087458237974654126907710072883911724662382183250003)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_418 :

Polynomial.coeff recurrence5Scalar0Left 418 = (((17861 * 10 ^ 70 + 8708964405125674189008049774955270488179650577042314648338252185388261) * 10 ^ 70 + 8794906192433271596139300497502336662082276157031157723513063422360532) * 10 ^ 70 + 7946394753931508437280371411018154667925627948545501682598737695782736) * 10 ^ 70 + 1865699270792094936429486867486973869961599690823740784941023320458220

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_419 :

Polynomial.coeff recurrence5Scalar0Left 419 = -((((232 * 10 ^ 70 + 1660204892691531715173329844636584496180951636172405353911856726899473) * 10 ^ 70 + 6739195481377220588377193474454473323013865734973001930007620730713257) * 10 ^ 70 + 3132087410225437115444520658756059002974572306465232004891814124615084) * 10 ^ 70 + 7311044070060553753670657075882866422644097145697144571504705465727705)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_420 :

Polynomial.coeff recurrence5Scalar0Left 420 = -((((197 * 10 ^ 70 + 8200262486286069092134800221371422837986768170409350330287656013608682) * 10 ^ 70 + 1764299856430234317916101911849498711417741337579326487771844651637589) * 10 ^ 70 + 2417855319137439337635061147566220378435835074842225021894897575930299) * 10 ^ 70 + 7456832264315565960551245348619778870626275583096336341397185456249746)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_421 :

Polynomial.coeff recurrence5Scalar0Left 421 = (((36 * 10 ^ 70 + 4890137481063994888412403212589097957763927210744442127495334101928890) * 10 ^ 70 + 7643966643712568217093146847390368625498062002483803137976740647595469) * 10 ^ 70 + 8025357088380804978809296896790807487424143286221904782756839890798713) * 10 ^ 70 + 1713225400411325866049823502195084846646555705817891414918794568169908

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_422 :

Polynomial.coeff recurrence5Scalar0Left 422 = -((((3 * 10 ^ 70 + 4365778350905829730755730600709179055766524279480419954680569984460396) * 10 ^ 70 + 6747923350007900324327674123410194348844229756677144467557620334452126) * 10 ^ 70 + 9281038516045835778375245448419474364722086815557725415227251896891017) * 10 ^ 70 + 6342089070620044681572993679348160802145567389071810931564494055125146)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_423 :

Polynomial.coeff recurrence5Scalar0Left 423 = ((1210097005709893494907305570256606545556577456662755199581528966710780 * 10 ^ 70 + 7596848197467726388818065794700965604915740819232025160909762890191946) * 10 ^ 70 + 2309308537974618071238347204372486585254660473760432127023164358569144) * 10 ^ 70 + 6102989389550981392813646337828908718161310361096265013414484490108023

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_424 :

Polynomial.coeff recurrence5Scalar0Left 424 = ((141015528194102200610086077528394466247982954555789585131781033917027 * 10 ^ 70 + 5512419019505986470025919727045529776711398962145954446192462244067037) * 10 ^ 70 + 385910064024094712860012708096040987508233211353969229396171572462769) * 10 ^ 70 + 6252343593479703908756242965837015559577355158824426329399541429045623

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_425 :

Polynomial.coeff recurrence5Scalar0Left 425 = -(((24046525455483726455406566125683451918486869628119881878380072865257 * 10 ^ 70 + 5101583203743148900737325938215546971294853597703826877660164383662087) * 10 ^ 70 + 5633374405310968357677318457857374112651013861433297785775663268595054) * 10 ^ 70 + 5996079688874844785136512390513186120575371127248491244242569954519364)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_426 :

Polynomial.coeff recurrence5Scalar0Left 426 = ((1388833997720180666905220176758805983601227461579994623685779935505 * 10 ^ 70 + 4192762797743440741587677430723566518634060651080553233407026252123043) * 10 ^ 70 + 1058508406311071809544257455405142575910463630545294723306424889726493) * 10 ^ 70 + 7633512360852601555543765547345000812934489623007874291733191778624824

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_427 :

Polynomial.coeff recurrence5Scalar0Left 427 = ((14454541632932519951000980401653042318661867253225974146145929312 * 10 ^ 70 + 1542697311739197078505698381876879591088984047370581365620585929288769) * 10 ^ 70 + 1746972842151223364964027223313514196154758634966833222374983854162968) * 10 ^ 70 + 8075684877460009815426084589993925772284436362249819596281193460314215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_428 :

Polynomial.coeff recurrence5Scalar0Left 428 = -(((7169067624637569583178166895701488122696389775696959505065815601 * 10 ^ 70 + 5759816561682405615044153395224353872780491544417325534417643851279529) * 10 ^ 70 + 1961624213786843828356656685876500095131213239916226963371586116902707) * 10 ^ 70 + 3155117220832214457402291617184522984375577037536616359888779576080111)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_429 :

Polynomial.coeff recurrence5Scalar0Left 429 = ((357724589051188181488435227340176119557469604182557866855338722 * 10 ^ 70 + 4642269943358587532544944847258384228986216621307908558570102405031788) * 10 ^ 70 + 5565168508014561125346339444063247887646666535757906110479049266840218) * 10 ^ 70 + 2993571885098097556460351341283645757829992825797029416841118496160198

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_430 :

Polynomial.coeff recurrence5Scalar0Left 430 = ((4499177402060529411627715808180107102223629980381684020419833 * 10 ^ 70 + 8300573342523398262234528565515498704883942254372933783126825462613642) * 10 ^ 70 + 1154864673946967891627111872626973252413773011750893339388591222669204) * 10 ^ 70 + 3561764842338332292245213742548428429129783262965425414872452090659721

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_431 :

Polynomial.coeff recurrence5Scalar0Left 431 = -(((937841017244245965529205845239786560750266111606270387676667 * 10 ^ 70 + 8335471288941764693850662040494806574408167983342166097899118456338884) * 10 ^ 70 + 8690673371732107735489595409575073107846099977288265688847101123252366) * 10 ^ 70 + 1955874694147553786245720107856903280425199271542013335622008215419695)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_432 :

Polynomial.coeff recurrence5Scalar0Left 432 = ((11081085625433426905522862217341566829825466887676675910630 * 10 ^ 70 + 9280378822287726050174365469604627470798355077047666999981509186600729) * 10 ^ 70 + 8602291139337548957953678923078199161145130839954394789649646209201544) * 10 ^ 70 + 518719925758986682395692092569522504843432911500370127267718669429632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_433 :

Polynomial.coeff recurrence5Scalar0Left 433 = ((1139651947579055546376003330673182612617132655447692033505 * 10 ^ 70 + 8580159922077179099604606408336246314760528427354974197140201928389192) * 10 ^ 70 + 8855834757264716190325949813859751240689922028527823087995604163049287) * 10 ^ 70 + 2304801407515718801484908130209928206657005049177218650205377319429441

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_434 :

Polynomial.coeff recurrence5Scalar0Left 434 = -(((11278622389481156858521458343226713891545437557763874469 * 10 ^ 70 + 8075626617621888618862282963009487180455738143938693365536733296999704) * 10 ^ 70 + 9760884136027376297586516085674496688038501039311985573337832632046436) * 10 ^ 70 + 4245982201737312536043352075870896748220196045882727358761781683708813)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_435 :

Polynomial.coeff recurrence5Scalar0Left 435 = -(((882903559521579243531370917526574745915813999481956905 * 10 ^ 70 + 1918304764341073743058356521062912439880727534765182970354223757012552) * 10 ^ 70 + 6605811401021930006220541261654677276726757402158455264805154403157337) * 10 ^ 70 + 4278763811980571539285434940856876335381908844933266355163008134028281)