Recurrence 5 lookup certificate: Scalar1Second 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.recurrence5Scalar1Second_coeff_338 :
Polynomial.coeff recurrence5Scalar1Second 338 = (((38598546701800529991774694965596449275972407378944 * 10 ^ 70 + 8326145887228343204439783964492693654629666587135877412564907932161772) * 10 ^ 70 + 5336972106367828148346541471418029767609003913841604616737907974692038) * 10 ^ 70 + 5266627040521565591513010463109432724976795316726093416241439369738970) * 10 ^ 70 + 7155425551317541813655288979831830818977694826678934338932965649816186
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_339 :
Polynomial.coeff recurrence5Scalar1Second 339 = -((((15339100553447471413713988993413984171407740605548 * 10 ^ 70 + 6932848794296020502792178059927767380127063391999673619668456510368885) * 10 ^ 70 + 5536867433420274677481897234641725089789020196640385560010222499946964) * 10 ^ 70 + 1296211234003044281980560186231628070979251078314700443813737835669853) * 10 ^ 70 + 6553821125423267466469375499648004125328413713353737457295805893091477)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_340 :
Polynomial.coeff recurrence5Scalar1Second 340 = (((5994004594942406626260159694580470861160071010187 * 10 ^ 70 + 6903873569581314615729225622283245203259848939593893273875779356909950) * 10 ^ 70 + 2158527094044550287898649995044012230249358485847538864634280888320570) * 10 ^ 70 + 4656523035095172775002684999419682532392774037860596550667297407942888) * 10 ^ 70 + 9664186414375006485772472621068396177820814767046827143558477936698958
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_341 :
Polynomial.coeff recurrence5Scalar1Second 341 = -((((2297535362288852518071321729032267122541796262281 * 10 ^ 70 + 816341277380389166288757343103829880693950052139521012543717801563275) * 10 ^ 70 + 7457574983550834266882332507205651640276120405402438899114086317689622) * 10 ^ 70 + 4344811500378743570914616185722846940296932477020073306270597609656544) * 10 ^ 70 + 3284461724550669945139249376032304251352454777340451423549090185009849)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_342 :
Polynomial.coeff recurrence5Scalar1Second 342 = (((861666381814727643718985956638270145544438545253 * 10 ^ 70 + 5724865464560371672574024390585887643218356822582261854420594525639454) * 10 ^ 70 + 7695415641361030177982053695173882563694556393436488564038972890833851) * 10 ^ 70 + 3881965371984118973678012855386686659768089337678370043157847161884828) * 10 ^ 70 + 2740980225134179008437724753176250517038981480321588311774371708762469
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_343 :
Polynomial.coeff recurrence5Scalar1Second 343 = -((((315450555584257392077962914709188339354209140962 * 10 ^ 70 + 646328894100113640810748998421943871309571080135831494127160029051442) * 10 ^ 70 + 2898729034626967118552948067469125158310558415333311835093687953610787) * 10 ^ 70 + 4401797000155599854334623230551722141172741760256211283781146632290821) * 10 ^ 70 + 7256371225541648112435857975333906693530813641461626355193228776728896)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_344 :
Polynomial.coeff recurrence5Scalar1Second 344 = (((112496589297190994962785861627477343694750686674 * 10 ^ 70 + 5238708696782363671227562021879262045874748399572293621573906714726303) * 10 ^ 70 + 3922522198903615137810788059914840250739196334755968350530623769907711) * 10 ^ 70 + 175838328289109669983550140999905923175139344452978663485048385034283) * 10 ^ 70 + 7333376587529453950453175172380634859489962188024889335321810639714810
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_345 :
Polynomial.coeff recurrence5Scalar1Second 345 = -((((39008653564691029276429678370698865240436553617 * 10 ^ 70 + 6223900746113779783381273188162747296794197750966147853459368708471569) * 10 ^ 70 + 8595643902147333736686589526892528783653283922121569549886401581630794) * 10 ^ 70 + 7045141658896132306794767422446261738069576118385568873422058127282382) * 10 ^ 70 + 3779817843155136021603114684303740094010599235369027396470814579766339)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_346 :
Polynomial.coeff recurrence5Scalar1Second 346 = (((13128777835287869973950812965318570192428603548 * 10 ^ 70 + 6527852846643477452647841465684084300539183048936210594854726952093175) * 10 ^ 70 + 5392927111724688076737959554452585670967881377723639568724036879692736) * 10 ^ 70 + 8276918433205224354548398173333585406595628690102377130267827391768191) * 10 ^ 70 + 3701253667344892609607051084138061779356489349823803858642104665470442
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_347 :
Polynomial.coeff recurrence5Scalar1Second 347 = -((((4280304917557224883625245039847239376832133064 * 10 ^ 70 + 3242635127835624061196940237734579528490779716022662296080045060762437) * 10 ^ 70 + 9748808303884367642966724307368886154236369307271442825987592584928845) * 10 ^ 70 + 1545499532999525382393736812066053598094650282140083054180911225244896) * 10 ^ 70 + 3259545820586753039049293979449016891078651271336462410819498246011492)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_348 :
Polynomial.coeff recurrence5Scalar1Second 348 = (((1348322452596628755843421259012578543233511401 * 10 ^ 70 + 4164828275579021262131646675279477073039870867028640689038789783172033) * 10 ^ 70 + 3518591278203242467729012678102634340494715546789647655205892101978135) * 10 ^ 70 + 3802558940180836950305107322272176845048890639456722491694106410568677) * 10 ^ 70 + 2923720653554723214382426112965170670857580825135411294461686172701288
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_349 :
Polynomial.coeff recurrence5Scalar1Second 349 = -((((408786387118651441798083911124788925835947724 * 10 ^ 70 + 258356952154950338127116775017560432219153042853184284445690493905951) * 10 ^ 70 + 8064953251975894647948639549069943693441643114290437911039110851021687) * 10 ^ 70 + 2122262385529372837757046562164461539798618886711666003098073193113533) * 10 ^ 70 + 9442101305797844029874849948176197220721214594739710478217391144970574)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_350 :
Polynomial.coeff recurrence5Scalar1Second 350 = (((118515391371276174528484356851923215860145813 * 10 ^ 70 + 7588289332250952422300665778348389583084210353572275619232775740009473) * 10 ^ 70 + 6670374484038202055034656007715366201488020802504191404729926369888330) * 10 ^ 70 + 2111043859253232174847481954819174700851665262260820883293419588083680) * 10 ^ 70 + 7425458248620476302808025101691911982395208267478008004980669202709758
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_351 :
Polynomial.coeff recurrence5Scalar1Second 351 = -((((32474488626337064840603043663624737289442078 * 10 ^ 70 + 9905672466321288244302215572199835677658595595028821230668364470288260) * 10 ^ 70 + 7613054872555283823123774993845657983138183672130624271355501242726500) * 10 ^ 70 + 6125817005482812258955418543483367041663098481501759670710660687931093) * 10 ^ 70 + 7809760072845087962163297721431167987925665562684285993362915474109467)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_352 :
Polynomial.coeff recurrence5Scalar1Second 352 = (((8214856301973562641133081194341484599043814 * 10 ^ 70 + 5018740841487850281529327888666879801024765912871616331377828024137334) * 10 ^ 70 + 782869478581655218018154543153309839115807296413123164782628071738666) * 10 ^ 70 + 4355733526535108516357542526798239143552735543218232251956017791883249) * 10 ^ 70 + 6904027767988467876853859148389859890485603092641135862978772426861844
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_353 :
Polynomial.coeff recurrence5Scalar1Second 353 = -((((1814415954992877196230134710294454887056422 * 10 ^ 70 + 5843983828126537247411676938695118834289432179546764831719694537666344) * 10 ^ 70 + 3054174069581730022310142067632724826673904570381597094992037997861692) * 10 ^ 70 + 513983335055887612178005715215748420381770710980523033646590705848707) * 10 ^ 70 + 1851084785067237724052507021675291123484578103197281498471135115958716)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_354 :
Polynomial.coeff recurrence5Scalar1Second 354 = (((289518783375197744798711489600493494339348 * 10 ^ 70 + 5799460065630929869577079238837185413059350762738568104419479272251043) * 10 ^ 70 + 1133049581935441782719329804003160689803544175555651950083185310249486) * 10 ^ 70 + 9319429118229118847270860351374560680885745964816725794250864854204814) * 10 ^ 70 + 3884863427566483169401116119601279980363575764208437153531994144818578
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_355 :
Polynomial.coeff recurrence5Scalar1Second 355 = (((8040382213582646232664492285334762491957 * 10 ^ 70 + 8509592775026325224482995592101454321587249497894343136362252330249554) * 10 ^ 70 + 8676710283494543297976606455435850706698866940150942533144724648720872) * 10 ^ 70 + 3642736792333372688169705892053755170045078071209316458581694156838381) * 10 ^ 70 + 9495130458602455893482647650297043372866772461092606026012448993577583
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_356 :
Polynomial.coeff recurrence5Scalar1Second 356 = -((((36573005340503056405355762423486460800205 * 10 ^ 70 + 6007523207334026424005957829854204994994773799319160905603646813055826) * 10 ^ 70 + 9023486149503533383768904525538629117053282699530734403020886288577757) * 10 ^ 70 + 2194824897690699954612122527383894780258646578516259869238509436304945) * 10 ^ 70 + 2815046643319021775714281000375037187322002229639063311373700260829420)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_357 :
Polynomial.coeff recurrence5Scalar1Second 357 = (((22992984451012360920566862582528372816640 * 10 ^ 70 + 304325849944314250742214484037400500282689947189756840315535802650481) * 10 ^ 70 + 3203877253966780493080428692512505793587463507170145535568737384896523) * 10 ^ 70 + 9836378727203913815916216671915590231469214686728779523494360443525118) * 10 ^ 70 + 7415019278334048831473647487067053713485928403959380376280947243562076
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_358 :
Polynomial.coeff recurrence5Scalar1Second 358 = -((((11067390736272118585116897122399683735437 * 10 ^ 70 + 8039198124405148051660271936440514438650690100866996731133841139619477) * 10 ^ 70 + 7190623453618874546194288652975196626842420523914553778991265360773471) * 10 ^ 70 + 9052256664182849252705665237993210658195935830801005573456370287589222) * 10 ^ 70 + 6870996416525542624496189314030992913990985891924843304297924420383131)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_359 :
Polynomial.coeff recurrence5Scalar1Second 359 = (((4754677196634719580117076541896676463972 * 10 ^ 70 + 9615997843017971092457495554298890174766883819434126293876837640828311) * 10 ^ 70 + 9463450789229764779951529954045623216182691474436523156177244469257462) * 10 ^ 70 + 4328471841082515586210748843910950070745549522650423370392893769117384) * 10 ^ 70 + 3096622329913450659846378727407640881302774325671837414990311064830799
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_360 :
Polynomial.coeff recurrence5Scalar1Second 360 = -((((1918034418750913008559714735448148902747 * 10 ^ 70 + 2430312383117438339448791253865641949809912525011141307736240204884238) * 10 ^ 70 + 7968593756145547658691487638807021286114435429405401769767011940038194) * 10 ^ 70 + 8045416884116725442127123131513950427357496836055643856399612762241331) * 10 ^ 70 + 9605962006582523353323545315617469383152630115251191838309618876490884)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_361 :
Polynomial.coeff recurrence5Scalar1Second 361 = (((743571214065932957879963002972892914823 * 10 ^ 70 + 1123127084017139660210525555503231812704107353498510093789113125804790) * 10 ^ 70 + 934327388946352068175257788187457937775258376434498379224458764295908) * 10 ^ 70 + 1379308955277900017781312478272942794107281442917957722919227702071820) * 10 ^ 70 + 2417259033626471007357220287838821410274360303213500455811004819466595
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_362 :
Polynomial.coeff recurrence5Scalar1Second 362 = -((((280404857859510269664607428316209502767 * 10 ^ 70 + 4137777957654490186917115926540252821700286480302686282252969703511124) * 10 ^ 70 + 8190569605806353999732623730415307360238410297625772725816029449441994) * 10 ^ 70 + 5641007298847477855997699048951316965063013659219201732635419014205139) * 10 ^ 70 + 2427408118282059769372560707374573187390356313323975835797673439383422)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_363 :
Polynomial.coeff recurrence5Scalar1Second 363 = (((103521311683637949159095389345320710835 * 10 ^ 70 + 8621840190883803575659477223297840025068112626398924411348498622583971) * 10 ^ 70 + 3461628019145284174092437875080617354596670117197609014746985696327013) * 10 ^ 70 + 3783831104005256737806215224924229612815844006769317094694184943511131) * 10 ^ 70 + 6689909288927976498322982429603451784271451160281250321368531429199951