Recurrence 2 lookup certificate: Scalar0Exceptional 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.recurrence2Scalar0Exceptional_coeff_232 :
Polynomial.coeff recurrence2Scalar0Exceptional 232 = -((10611107688030479963139801436135872171043746437824727971357359 * 10 ^ 70 + 5876312946272180039138509895029480224356939192463084147229207500825133) * 10 ^ 70 + 7773803497462998305304309800359626580679334019037820787555178388124858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_233 :
Polynomial.coeff recurrence2Scalar0Exceptional 233 = (8146682714838781562863733858405887175879440239299984923358690 * 10 ^ 70 + 7280272271405914813280726973206338481792713904797256198613631132027316) * 10 ^ 70 + 9339454652435749092859464132883467916532438549557316145579380153284475
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_234 :
Polynomial.coeff recurrence2Scalar0Exceptional 234 = -((5787074263936029118978790795098670543128712508062183286046326 * 10 ^ 70 + 1377599017651320315925723975992295635239486999065254066950384167346872) * 10 ^ 70 + 4473995201619473158056289566564091739084593555808615501167666551678093)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_235 :
Polynomial.coeff recurrence2Scalar0Exceptional 235 = (3758737539467107177101919691339892477923004140193213258492918 * 10 ^ 70 + 8734337820682101415839034202958775896019850926499868183431795900898092) * 10 ^ 70 + 3250722026605909662975036565373333326312582263431995719735558608420447
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_236 :
Polynomial.coeff recurrence2Scalar0Exceptional 236 = -((2169704095319069684949862495463938043801212579053590497394884 * 10 ^ 70 + 7347721710069789607837293919953739993951918748186935432456731955835713) * 10 ^ 70 + 2363729549347521846589937447057952816822285821693203515971281533141793)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_237 :
Polynomial.coeff recurrence2Scalar0Exceptional 237 = (1033311659527180580881584819914438978867025204297265709239711 * 10 ^ 70 + 5354772786434748597382687538405031620540842735356088821239255771571694) * 10 ^ 70 + 1361792870338636934391919276566048373765621800907791169874087769508745
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_238 :
Polynomial.coeff recurrence2Scalar0Exceptional 238 = -((299467536720650589632200977395108640895558292269467556608611 * 10 ^ 70 + 5677697474094045976775895118843567636923255327725079947753357497651165) * 10 ^ 70 + 7566596761522401329371039449926055451331201289190081843465661233457553)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_239 :
Polynomial.coeff recurrence2Scalar0Exceptional 239 = -((114861844796825933899505468593722954965302297504464219815699 * 10 ^ 70 + 271111735829964111329117590496131984493561110361733977776962796539876) * 10 ^ 70 + 6317200107114135881117277094306116681001425751525295887918366529481862)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_240 :
Polynomial.coeff recurrence2Scalar0Exceptional 240 = (301073560163082302609357099958998866799262968899517504888135 * 10 ^ 70 + 6836776203053597754152591608796724892355419926380793818118027947223785) * 10 ^ 70 + 9651449550699269852622984229087444672614453858270555330261021916691640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_241 :
Polynomial.coeff recurrence2Scalar0Exceptional 241 = -((342352359033535005160961077816172694977543414564180158893963 * 10 ^ 70 + 1776254741258293986181065725284935414963274809102982657638804718035468) * 10 ^ 70 + 6925583884593078491619839701239487078265664256694941653089492893393427)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_242 :
Polynomial.coeff recurrence2Scalar0Exceptional 242 = (304891167666928746874665900931792690142480529500089136369936 * 10 ^ 70 + 8868634109090247166941745288634021154744609968806142815186361823725990) * 10 ^ 70 + 4295677516239618182459181416353049567121858041487124794858761569274636
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_243 :
Polynomial.coeff recurrence2Scalar0Exceptional 243 = -((235351516231034510140856015470786091111916619785951488414954 * 10 ^ 70 + 4994834724239241402801224761214179030124193918094295052473849040369646) * 10 ^ 70 + 8647245152327338219890637962976358136725707203881220075738439298692746)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_244 :
Polynomial.coeff recurrence2Scalar0Exceptional 244 = (162493364567518657221672193944771720057042692039124682223592 * 10 ^ 70 + 3017815015694830605903426638619896704403672989799105277396189835174629) * 10 ^ 70 + 9877758925628779060376692619288735172621061829209478838085885003109677
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_245 :
Polynomial.coeff recurrence2Scalar0Exceptional 245 = -((100985707053646097169218844792371888528350214214962926573251 * 10 ^ 70 + 1230943123724367214355950610614656673862530897430276874939402445700109) * 10 ^ 70 + 3801746606365933987974732069715765863468145671274355204798457497382979)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_246 :
Polynomial.coeff recurrence2Scalar0Exceptional 246 = (55828040656070415956308588402363142078762682037945205652913 * 10 ^ 70 + 8293922489144489359812190534721706558032984791825059323627185773709696) * 10 ^ 70 + 8713428663369513558906208254540463174296498132265582635929463950145204
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_247 :
Polynomial.coeff recurrence2Scalar0Exceptional 247 = -((26352929830775959920695020756131992785572392840547816126471 * 10 ^ 70 + 2078969429790414294036256760316909493553989517385181070674016732040589) * 10 ^ 70 + 791737331663634864916201984382857541430796104756447639280466737022260)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_248 :
Polynomial.coeff recurrence2Scalar0Exceptional 248 = (9291552448229639009924629360200217571238811437615950963921 * 10 ^ 70 + 8052700793825369808135806092116118331340145313057188957666884101229708) * 10 ^ 70 + 6041900671856215234325096252602456679970465513123416365037789426681015
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_249 :
Polynomial.coeff recurrence2Scalar0Exceptional 249 = -((782020366484313540698460603750002840343070250353062268406 * 10 ^ 70 + 7239766750171183564809946663525951177868457579089213709444417110336101) * 10 ^ 70 + 5729169516268652661291491536014178499518134644284164533319965106845791)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_250 :
Polynomial.coeff recurrence2Scalar0Exceptional 250 = -((2546544597064898835252770016800250784301090428965034190993 * 10 ^ 70 + 3347095253229648244546523539936972435238498239069043381606743794827078) * 10 ^ 70 + 2578269999867677821829681424735405118599528399318727914836278658017562)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_251 :
Polynomial.coeff recurrence2Scalar0Exceptional 251 = (3163863644467997917129430213734086559663586645561907067381 * 10 ^ 70 + 4945068398889568218429328082381917864765014075141482584924516904658625) * 10 ^ 70 + 2000358875618102832155926137643647329371553378688823946051759793411403
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_252 :
Polynomial.coeff recurrence2Scalar0Exceptional 252 = -((2637673616106995762289640439391880416478983555211793364425 * 10 ^ 70 + 8071396562177527949533889206226452456415135154810970760628108187631455) * 10 ^ 70 + 1298465498433070495863630119491274614744127911197956199300527244803514)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_253 :
Polynomial.coeff recurrence2Scalar0Exceptional 253 = (1824904037112719108083398350337813317817461008055041690284 * 10 ^ 70 + 957181151968544441428535764802145637143290097205673158899797190936193) * 10 ^ 70 + 7310248866070447471921900802260697641906381920414801257809538235842537
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_254 :
Polynomial.coeff recurrence2Scalar0Exceptional 254 = -((1108572438053627620080915415178942442108283443807109322961 * 10 ^ 70 + 4586394167671364965085791805365996201242615590926355166903921976130170) * 10 ^ 70 + 9225482549849206759294174506370968385927140170133824291719674984267539)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_255 :
Polynomial.coeff recurrence2Scalar0Exceptional 255 = (601926745187544458032196577820832528744312100208793661621 * 10 ^ 70 + 3580809178158275340679611398107614539509708308508728958764827578231792) * 10 ^ 70 + 5466836140618778105382109903762243885974182745922038188756545039251703
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_256 :
Polynomial.coeff recurrence2Scalar0Exceptional 256 = -((291907693511582334020788491318077038467742812193376975762 * 10 ^ 70 + 2384189554745213184063198240766674508971671549739689145074620120895307) * 10 ^ 70 + 6067542120506892528765061258826545951696067554534190643114999535225165)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_257 :
Polynomial.coeff recurrence2Scalar0Exceptional 257 = (124014835873077465425377983941990791463857337606411541566 * 10 ^ 70 + 2516930209546099524538839560039102994404332688405461914074637381044838) * 10 ^ 70 + 1965486066821013475547200174776210084068873617515012261613246317260773