Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_338 :
Polynomial.coeff recurrence4Scalar1Exceptional 338 = (((2835571529763 * 10 ^ 70 + 9198512226937557623587943608345117297578290280935640061400166753764159) * 10 ^ 70 + 289389408391377695636159065758104121007101017327449121006717518291437) * 10 ^ 70 + 6683285040455057250846138014682284970876323120843441120604413377150368) * 10 ^ 70 + 6395960397259160929326010755172838269051430707153618006200422978645171
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_339 :
Polynomial.coeff recurrence4Scalar1Exceptional 339 = -((((1072894083893 * 10 ^ 70 + 5919517736551884360120994232796108584584874369129640239843257805046089) * 10 ^ 70 + 260560649797794947158644115196338749532179544678127177687189527799859) * 10 ^ 70 + 2061281271952352756740710157701688978678946953537327233591738498585208) * 10 ^ 70 + 8075672974520158041251686056418508303652116969098154321338291348479359)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_340 :
Polynomial.coeff recurrence4Scalar1Exceptional 340 = (((391263472552 * 10 ^ 70 + 6840309299550560765737759660573409457554796898367163948215843859496611) * 10 ^ 70 + 3404747403989551253199324693459933940959674373937477149571028058348477) * 10 ^ 70 + 8320684859251505632467224221122207586073973568818144313302159417950358) * 10 ^ 70 + 6669585102499578821378912344032494867456581866288779660733816519659891
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_341 :
Polynomial.coeff recurrence4Scalar1Exceptional 341 = -((((136016437443 * 10 ^ 70 + 8203163958389375828414498197869187927183444360917707401862944257634698) * 10 ^ 70 + 2982533738135391381352794825636145835338949217996920955244847429726174) * 10 ^ 70 + 963997746372827834992080909453749224002373186611401374016123288242351) * 10 ^ 70 + 1409554225011125316077064924880044061434088969894375953320562614506560)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_342 :
Polynomial.coeff recurrence4Scalar1Exceptional 342 = (((44137362233 * 10 ^ 70 + 7279560665855231247860414135313071915112177111133333816455333430389240) * 10 ^ 70 + 4966643421199851257425126896608744200212960492903887315004726647056882) * 10 ^ 70 + 3361948344290779375704253887587186956463137864157777555801987008617624) * 10 ^ 70 + 8888730414303717314913571571247234895903415219505970250132844024654030
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_343 :
Polynomial.coeff recurrence4Scalar1Exceptional 343 = -((((12758950627 * 10 ^ 70 + 6685099934271284211682793017366095524035682762615940217377516393924915) * 10 ^ 70 + 7540782584018651431382202643915201851769769667025581873699657343625977) * 10 ^ 70 + 2724555244340923839404527319812484262714013170600256511028244206604088) * 10 ^ 70 + 8865511195645936170865428501044410909978652393127807159721522844713085)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_344 :
Polynomial.coeff recurrence4Scalar1Exceptional 344 = (((2852130644 * 10 ^ 70 + 33897796251122078662744628955316119009158255994625555238261306499876) * 10 ^ 70 + 850435598013858875739622818464673455267996206541314657292745462828473) * 10 ^ 70 + 781637006829094959807151846645045697159691559127417126712440499914186) * 10 ^ 70 + 9614248691198343232686693662389088928094157354752655927566426373316769
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_345 :
Polynomial.coeff recurrence4Scalar1Exceptional 345 = -((((134129184 * 10 ^ 70 + 6938689381956545694589817559757072228444795704769774172600875134349138) * 10 ^ 70 + 320011454565257176405945262439477622104366484008507314435790396329478) * 10 ^ 70 + 2675028491498466767030796909339877021246567193570108942933921138157678) * 10 ^ 70 + 7392721566326391030650757623702323101924026524343560255692779673418545)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_346 :
Polynomial.coeff recurrence4Scalar1Exceptional 346 = -((((386074680 * 10 ^ 70 + 8326761229363364358410285664767195514123369825231465037351795060161204) * 10 ^ 70 + 5086880137083586512073191146809006083669141336964587826553914520454634) * 10 ^ 70 + 9209449705389881300345350403783948701852943588632909477562537723721373) * 10 ^ 70 + 4052136486195432295325348339927191651639863615067879704360934926424160)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_347 :
Polynomial.coeff recurrence4Scalar1Exceptional 347 = (((342446240 * 10 ^ 70 + 4364834462131661387133787953058672659390745999195575244078514731566649) * 10 ^ 70 + 2740562305216714024227306708323949908388093937818645966374527442160158) * 10 ^ 70 + 9334906979222403615108577431965674296799175295221016359711830660601563) * 10 ^ 70 + 9650540235323889444411232999952468236609135261987700714505412609365136
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_348 :
Polynomial.coeff recurrence4Scalar1Exceptional 348 = -((((215678303 * 10 ^ 70 + 9777473447671772314244034350036973666965961515641609017465245053698043) * 10 ^ 70 + 5799911238764854976664067706003991600738608394208134401657164973527628) * 10 ^ 70 + 3779264897175951488963779243018642080386946880936282272541432806240780) * 10 ^ 70 + 6149235103241501743068376372545823810419464466330719492951948708947419)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_349 :
Polynomial.coeff recurrence4Scalar1Exceptional 349 = (((118461367 * 10 ^ 70 + 4546875603904141994517477443148439747637453429812109727699110981100078) * 10 ^ 70 + 2458691520212435483273953156524443466527884073717184511355146573227192) * 10 ^ 70 + 5905558435295403376917989156720153624108928900779002887929255898689401) * 10 ^ 70 + 1019021294172732555083686268450547737393378487175875013186441925936098
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_350 :
Polynomial.coeff recurrence4Scalar1Exceptional 350 = -((((60202043 * 10 ^ 70 + 9095907681712282596043604944473942045342193916962099575137029055690208) * 10 ^ 70 + 3881097910912582038985518223275296317831946078830559261998943299658702) * 10 ^ 70 + 7672609086425176061764950726288092772853611640983481774953156029192651) * 10 ^ 70 + 3810487010144647357624678430769993856558573002594051221064125149794207)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_351 :
Polynomial.coeff recurrence4Scalar1Exceptional 351 = (((29019112 * 10 ^ 70 + 8236094584912702554054129083307885105726797965373527045365828031501260) * 10 ^ 70 + 2191168658319273844950867277564803116212166837400167871676040426481561) * 10 ^ 70 + 22309222476124904784338718242800587125922356181259455835243108888683) * 10 ^ 70 + 4845770787784585062581549644660399284648953619987943507260365822536353
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_352 :
Polynomial.coeff recurrence4Scalar1Exceptional 352 = -((((13431312 * 10 ^ 70 + 2169791362285262862684523847312120802085199379537256787244525205733680) * 10 ^ 70 + 3083619150777119834700121581815759186928855832728407971652578491822701) * 10 ^ 70 + 1672240765987657188467757653006559460505606483794690604073477122271450) * 10 ^ 70 + 9932374342750154151820939913717290773241751771004360006112608970598966)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_353 :
Polynomial.coeff recurrence4Scalar1Exceptional 353 = (((6008193 * 10 ^ 70 + 2156482070595203958347337044485188556609487538767851299171594244454728) * 10 ^ 70 + 847364188666241559419072028331455574400075224413406088925254852402281) * 10 ^ 70 + 9562289107816530706651236539482472646507582916737984147595877557861431) * 10 ^ 70 + 5986098306703867870585279749139157344076841982781236738493543182770934
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_354 :
Polynomial.coeff recurrence4Scalar1Exceptional 354 = -((((2606586 * 10 ^ 70 + 5181418858689932300749061379713570272405123403318797526933985685275438) * 10 ^ 70 + 6684023555714456459265970650910506218718954849730375008180450060584539) * 10 ^ 70 + 4899371014005477470385411710964983518599004562406747364932178536129771) * 10 ^ 70 + 8703479743191155246281942862019374597094053550743892628411122366497428)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_355 :
Polynomial.coeff recurrence4Scalar1Exceptional 355 = (((1098591 * 10 ^ 70 + 5460985922879995002400078972677436223283527945625605744053604621132196) * 10 ^ 70 + 9207715854873814302814953558989168654025912402782869228025652289207209) * 10 ^ 70 + 3796918401187225038903833114127612063398349033736512220106581761053503) * 10 ^ 70 + 6793182763702263062407135304930226872872193016595086643976117681497351
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_356 :
Polynomial.coeff recurrence4Scalar1Exceptional 356 = -((((450044 * 10 ^ 70 + 9136662716715035670981319248516553452052882658283906576646847202977817) * 10 ^ 70 + 9579891767048447719844715990632951613651459002596569809903597361053703) * 10 ^ 70 + 3774085894388052383529783952582849694505220326087337011744420462833392) * 10 ^ 70 + 2411409134248613128599410885907500905587995966339949617692690619146412)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_357 :
Polynomial.coeff recurrence4Scalar1Exceptional 357 = (((179126 * 10 ^ 70 + 9485946443165851390648229997421436072289862405455539847644462661518293) * 10 ^ 70 + 7477128531482701958669426401655493511008473996401361535868830692427418) * 10 ^ 70 + 9540858810634730331322720073320125916791045803782819365704377386678245) * 10 ^ 70 + 1634020142834145212518315201569929675789674844624419821598695030072253
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_358 :
Polynomial.coeff recurrence4Scalar1Exceptional 358 = -((((69186 * 10 ^ 70 + 7448872318072538143037376269954150372117081316514308950131781301697176) * 10 ^ 70 + 8891404747046768414733452310237355716857306672079086693135135364406034) * 10 ^ 70 + 5857663059164905060139614343887547104716329010415737867833602904567178) * 10 ^ 70 + 5565674995362664676291443299362378083074551509444403705012644591237900)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_359 :
Polynomial.coeff recurrence4Scalar1Exceptional 359 = (((25876 * 10 ^ 70 + 1893852918619440809798006844418791754863804000213191434080190532901778) * 10 ^ 70 + 7973151461714970706540538269895538223901286031957833350940301052875236) * 10 ^ 70 + 1152670530020932380161574400641438914226337762419718341794464335752056) * 10 ^ 70 + 3367287656243204398444148431752666825437554230611518789482218653616145