Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0MainPart2.Coefficients329To355

Recurrence 4 lookup certificate: Scalar0Main 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.recurrence4Scalar0Main_coeff_329 :

Polynomial.coeff recurrence4Scalar0Main 329 = -((((84658320589887583 * 10 ^ 70 + 4088416817424897263689281238781894809754419193046844164070311364196481) * 10 ^ 70 + 2681541387013921862707714068336364235660785058561018921341747241624632) * 10 ^ 70 + 3600936993269608758030784622380404955172965000764091741213704733941589) * 10 ^ 70 + 8844755505421373616561427513630260122516425721873876663312071913429513)

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

Polynomial.coeff recurrence4Scalar0Main 330 = (((47983854090135507 * 10 ^ 70 + 3665305210652681248921987087994426918778164470487092676435102273969444) * 10 ^ 70 + 1136943165691628434857742467948137053976897473151863156938949486829588) * 10 ^ 70 + 3374901995992484648379779571492532046069471234696479156355256218453227) * 10 ^ 70 + 3383596131237052988098444362745866904557424495066458746812875036474004

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

Polynomial.coeff recurrence4Scalar0Main 331 = -((((27014565131625658 * 10 ^ 70 + 6973138997300841562396366295337530180143768878461896608904336772408687) * 10 ^ 70 + 7623569520093175392815558977210510875603824604558477199845982521930356) * 10 ^ 70 + 8633296369269778755126535207904914063383149207109447015424472368675258) * 10 ^ 70 + 3988226608768284703297907857179572957100681027330969961814237280273514)

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

Polynomial.coeff recurrence4Scalar0Main 332 = (((15068920576032673 * 10 ^ 70 + 2830323721946742171451086441209980960448595887487161663311877724545097) * 10 ^ 70 + 2397915478287676101261359397216765394476087647885942048103791099581942) * 10 ^ 70 + 1604189636592723457836956016462136722816358833046814541777655821365761) * 10 ^ 70 + 2376090586430467909186383802233021719291239096883807737943207071063360

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

Polynomial.coeff recurrence4Scalar0Main 333 = -((((8311318352549153 * 10 ^ 70 + 7863728257942956266561502197856095758587350685432070120781268230666118) * 10 ^ 70 + 1228588992654369652774656103303852644702862875204152478220799085965201) * 10 ^ 70 + 6381900142471107519630396532414151948186547268840876686777677494556549) * 10 ^ 70 + 8723435588662153689549817065995273398997402077979769998893078140762038)

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

Polynomial.coeff recurrence4Scalar0Main 334 = (((4525626902120899 * 10 ^ 70 + 3230738860795925036243668720915590994206323022393151707184259644218453) * 10 ^ 70 + 2671945368543225941921713891123373772570072967892282225137290545233615) * 10 ^ 70 + 1488569063351393699287907141638403002542523963182007755209186295093274) * 10 ^ 70 + 2289725216415865031099005205685159502104519568879393537033861823521715

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

Polynomial.coeff recurrence4Scalar0Main 335 = -((((2429896605482107 * 10 ^ 70 + 8305403052866005465263072993362183294775885368586101235255728553691860) * 10 ^ 70 + 8748602012330098164426658691836746335924904961930395664767496501795839) * 10 ^ 70 + 2955237043688575425020067385134176380184179330247694850945962290708597) * 10 ^ 70 + 8990819963050133336448409726568244973016358774933487949354252965582363)

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

Polynomial.coeff recurrence4Scalar0Main 336 = (((1285296373263172 * 10 ^ 70 + 7232608922704346675049612231208392498778964738501171631882012653450598) * 10 ^ 70 + 46565044083288909723436391280841729197168306292447354001596845971289) * 10 ^ 70 + 6907735324040254373568567223319429519839303942644514529321305702392564) * 10 ^ 70 + 1846491357165540322839461626203903675564512760579461812865468870992164

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

Polynomial.coeff recurrence4Scalar0Main 337 = -((((669309750864956 * 10 ^ 70 + 1655137897445877063161503048149018996347674212099551310523770705497381) * 10 ^ 70 + 2547611060547754960047656825746982178638883789190494717890432492733674) * 10 ^ 70 + 3940401118266215736756562036368371719514387433692424562220267687627816) * 10 ^ 70 + 2703841172468696233978507750883120028641945908231171401171344557432803)

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

Polynomial.coeff recurrence4Scalar0Main 338 = (((342949922362243 * 10 ^ 70 + 443945828185621899282430987038620269071581597928063555595352330691152) * 10 ^ 70 + 7799081703029850172738234935885294268244732114830053990365239950934219) * 10 ^ 70 + 2444104707045848524077079444552073961596511054645032520793033190534465) * 10 ^ 70 + 8997828040119081525917413310737427738536481025849571680220132779708743

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

Polynomial.coeff recurrence4Scalar0Main 339 = -((((172835669764725 * 10 ^ 70 + 389271136846012791182617400705475791008559399357074253230673977641009) * 10 ^ 70 + 166667787427866180380181224280838645343110221597470120670012680180902) * 10 ^ 70 + 8620610783651635948346817457854474611674104205166259658464187906706384) * 10 ^ 70 + 9809132913752413040619313463247927641940652412636273362901332346810794)

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

Polynomial.coeff recurrence4Scalar0Main 340 = (((85641838320593 * 10 ^ 70 + 1408015483942806124582007971261120368025812484461700282779756249842259) * 10 ^ 70 + 2016279968781398093665968779469250182369170446525075157961125404243831) * 10 ^ 70 + 6182483353100454036305653419892088236882219577538272810350521147914413) * 10 ^ 70 + 1644387891798750698631861445475399027818990989619940652134719461410069

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

Polynomial.coeff recurrence4Scalar0Main 341 = -((((41711684834977 * 10 ^ 70 + 1209822143783894211040878594224778655845928358147530236469794348185819) * 10 ^ 70 + 5594935101527814375428030054740999409312149378395986909106043400798229) * 10 ^ 70 + 5730873653142773734834398913037530579874354999094698938370370922122244) * 10 ^ 70 + 896546916609947486680018400307598818051949947873981841364980230966245)

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

Polynomial.coeff recurrence4Scalar0Main 342 = (((19963014259772 * 10 ^ 70 + 8057397470788796326113301909804104053308841315366464500300457138525515) * 10 ^ 70 + 7040039677913672122877477618258616665590465712638196998056568328157875) * 10 ^ 70 + 6026099335298582991160014584416898345393761560488917500750903339501669) * 10 ^ 70 + 1455976589517647071793536242253266940616648389753450602655786408232448

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

Polynomial.coeff recurrence4Scalar0Main 343 = -((((9385750269045 * 10 ^ 70 + 7294495796210869223840277450050001713051763351700444029738825202139850) * 10 ^ 70 + 8510445388630084490470858271012337394522734772555853835933563650949377) * 10 ^ 70 + 7229169301854606720644620065206284531294744912961111062096751476408829) * 10 ^ 70 + 2478841271013367101422659941857162378136563456860278427222209181897343)

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

Polynomial.coeff recurrence4Scalar0Main 344 = (((4333695355405 * 10 ^ 70 + 3272250080994465663740852567189655521098084514636878393800671852147755) * 10 ^ 70 + 9738943993615263421002701694804605133405725754096919670638718098029839) * 10 ^ 70 + 6315897423015739738337416893549559734047061186507249589850527799571881) * 10 ^ 70 + 1643600542032086297420514964249836259909661434130924794922733100637052

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

Polynomial.coeff recurrence4Scalar0Main 345 = -((((1964515830109 * 10 ^ 70 + 5819361534418221693902090926543201513316912295294318800008871594148670) * 10 ^ 70 + 1945624179898694065007239165069780447299627656260114112810107922546551) * 10 ^ 70 + 48608075174456848256452596281742963469093551379002766900141729090297) * 10 ^ 70 + 532136578798222131568215573993310074488783972698236702790303054202291)

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

Polynomial.coeff recurrence4Scalar0Main 346 = (((873991501845 * 10 ^ 70 + 6996920013163988726944570077233974971689070819949005041312677494787885) * 10 ^ 70 + 7565337796994479807039179585921327759699482816578029471293438012148193) * 10 ^ 70 + 6031060315034529906918215559027795937102226226877940046720577566561121) * 10 ^ 70 + 7148987302450175144461385147078732297487120059407993287892619614994178

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

Polynomial.coeff recurrence4Scalar0Main 347 = -((((381454804180 * 10 ^ 70 + 3067061455418643277437975176222641220104802356353217725361400319262272) * 10 ^ 70 + 7313376295211919001112584940474401170972962350764433406300691152684123) * 10 ^ 70 + 7723872403506792491300840179252796920711754766955009981157926972725603) * 10 ^ 70 + 3074802203918713729048605223407809525666032276787033510752762103663828)

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

Polynomial.coeff recurrence4Scalar0Main 348 = (((163258117992 * 10 ^ 70 + 4736202974401253630431739384551979145814852568683182788757887149244412) * 10 ^ 70 + 3861799732753990158544186020432471063480268762615593822912228449048393) * 10 ^ 70 + 3699565408722498156732398632291811689543863586405283569341586191005158) * 10 ^ 70 + 3481829241873012791010697042237974560875021617358152554457789176756992

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

Polynomial.coeff recurrence4Scalar0Main 349 = -((((68485291458 * 10 ^ 70 + 6711643731726708776924429260177186967547573231184046595149394257438700) * 10 ^ 70 + 4834766984934901249440221959047547788062148038803921436894701298011171) * 10 ^ 70 + 5179308139048330489024846905907057187627550026267902510846281819623703) * 10 ^ 70 + 4937713057703260398356710988999600686884208141319759874174588183110)

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

Polynomial.coeff recurrence4Scalar0Main 350 = (((28144571709 * 10 ^ 70 + 213497559858259760210065567468190939393636196092193779069637516037099) * 10 ^ 70 + 2169188890235769541002340366780915141242634878758989378494800552301741) * 10 ^ 70 + 6861539671787971854857210399176535454960275750161579762438679098088752) * 10 ^ 70 + 4621206702195345932717688218224026138868782615781483178268988431643584

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

Polynomial.coeff recurrence4Scalar0Main 351 = -((((11325373892 * 10 ^ 70 + 4330782262748878082295183204680029739542224146018410411840937052726799) * 10 ^ 70 + 8569337265251710569818856236900189818094502209377413505364017733422720) * 10 ^ 70 + 5922802671591648287132589106772930094417375891480449803596854385016829) * 10 ^ 70 + 4394919080980915525724063055005097164643434456132770796123878793685555)

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

Polynomial.coeff recurrence4Scalar0Main 352 = (((4460504472 * 10 ^ 70 + 9622405940383050346920937490335101624588959464046559226728070203516877) * 10 ^ 70 + 9069960536223493445175828635935224848005079967025457213792972993707378) * 10 ^ 70 + 8365927164249954467447235405370843260244440567360244960174719137164892) * 10 ^ 70 + 1433760780648682989046227155311450882750269334332330665805040565227161

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

Polynomial.coeff recurrence4Scalar0Main 353 = -((((1719003037 * 10 ^ 70 + 9399211482844304035368770803500356551053106192006231471208842331407799) * 10 ^ 70 + 7050331311938284887635553544894907633387039511375583944647014049957482) * 10 ^ 70 + 7145144869791898447938135241309237447569594144012646330247226788288167) * 10 ^ 70 + 9706616347108431876486910982585626028817483952602507488001652110872190)

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

Polynomial.coeff recurrence4Scalar0Main 354 = (((648304059 * 10 ^ 70 + 6896842405259993320674317731501197733347803408115321128209767399789029) * 10 ^ 70 + 43487853522241719283180348636009713262147489734809180021831922308835) * 10 ^ 70 + 5000984152336906473719388417432340247019549818049221604607351913082703) * 10 ^ 70 + 622730898733675246318920958263765369779855366076383137303549477240392

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

Polynomial.coeff recurrence4Scalar0Main 355 = -((((239468796 * 10 ^ 70 + 3017236773840912118150580298365267917917025839028503141037899609698987) * 10 ^ 70 + 6580381095305175848180389686725544759691668688145169499144054775063582) * 10 ^ 70 + 7369366567850793695069125211562870347466853831814546122756932089465566) * 10 ^ 70 + 3292243712529387930692846338818693179144127186237285153201516221313618)