Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_79 :
Polynomial.coeff recurrence4Scalar1Second 79 = (40511619728178186806259156432602553583538324928427367238128996645808 * 10 ^ 70 + 4643041706403831414623558927508089781238112997424978963189235783407864) * 10 ^ 70 + 5458334452697521845115928230532295786867461104738411139838428703065999
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_80 :
Polynomial.coeff recurrence4Scalar1Second 80 = -((1702320258667531653972431386404351649836019840512336530591199380665791 * 10 ^ 70 + 4807636682015874947485067833246742336037867873993044042587333629974574) * 10 ^ 70 + 3622609843090970790192051940434654724891932864779683285445680909033119)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_81 :
Polynomial.coeff recurrence4Scalar1Second 81 = ((4 * 10 ^ 70 + 7835795447179386162068895787646819030882266684259662790727643619074570) * 10 ^ 70 + 7913590102178984608988888584083283421741289512574786440617240237515806) * 10 ^ 70 + 6407842773199468479643797556891928811151705605933192708467760133861753
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_82 :
Polynomial.coeff recurrence4Scalar1Second 82 = -(((112 * 10 ^ 70 + 2787328736844764108631288899323909669798610274652359953284167059763524) * 10 ^ 70 + 8782208602040108958551076034461244578655472259241957966894234856398249) * 10 ^ 70 + 4386030019567203512281268759630029609186238286250056239006441629420069)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_83 :
Polynomial.coeff recurrence4Scalar1Second 83 = ((2337 * 10 ^ 70 + 7863506251543522808082719085815179718152599042247623362295963585760416) * 10 ^ 70 + 4198852259371273432742859256685973666304613711150498661103687479016375) * 10 ^ 70 + 4517285244253702782624809173543531376468956798839173892856389230117593
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_84 :
Polynomial.coeff recurrence4Scalar1Second 84 = -(((44142 * 10 ^ 70 + 2885534397524988014548721614239435780437907894202094327583731402437810) * 10 ^ 70 + 1641970488902685848099976380387085343997912962921126088079398693981923) * 10 ^ 70 + 3868902302137519097384142143104752702760382419433557529761000897935060)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_85 :
Polynomial.coeff recurrence4Scalar1Second 85 = ((760416 * 10 ^ 70 + 1491343566069396573580791995124646545344169598545954608654305751059092) * 10 ^ 70 + 7215400744899009342479019608963368235366813110159279224110120080966390) * 10 ^ 70 + 668116063317492707201218141952115532078758546618003646074818525831172
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_86 :
Polynomial.coeff recurrence4Scalar1Second 86 = -(((11880710 * 10 ^ 70 + 7644162184318430387488543606541824690037553897946263503194361224756898) * 10 ^ 70 + 244560406086800777556150301548241022178068481001402983602845295021214) * 10 ^ 70 + 5760888532792677220572461684161824523654320450264716002206546408595642)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_87 :
Polynomial.coeff recurrence4Scalar1Second 87 = ((164595676 * 10 ^ 70 + 561327912938184365032642030995423411005983118020852659811738853562483) * 10 ^ 70 + 1278720661316082532540564569417630624702079021504182620984338141005200) * 10 ^ 70 + 8835961335418672038290547191237603501594250888574565273706807181708287
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_88 :
Polynomial.coeff recurrence4Scalar1Second 88 = -(((1897487156 * 10 ^ 70 + 7918857421890883520230209612564900033723113407293800178358377083697238) * 10 ^ 70 + 9222522713313810194454067878129047711591604208464748103301129051179547) * 10 ^ 70 + 8735469688842999947055391306621761406604336982320851429877766326108004)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_89 :
Polynomial.coeff recurrence4Scalar1Second 89 = ((14216237134 * 10 ^ 70 + 4564272758664543532953348610208880755272915143036469926050660879946420) * 10 ^ 70 + 3409088873253747721504799642040795328002599621887996766702892909710431) * 10 ^ 70 + 1531216846413863347650538601127287079216209147376335133377453036255998
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_90 :
Polynomial.coeff recurrence4Scalar1Second 90 = ((76072247001 * 10 ^ 70 + 6529373284483495968073964227620715307380919430715818016623105313620428) * 10 ^ 70 + 5726506545020885183898197815994429572813088203914977907470742406067058) * 10 ^ 70 + 3612992013263697661519738725567661002667054927431758979984593369784107
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_91 :
Polynomial.coeff recurrence4Scalar1Second 91 = -(((6299245603606 * 10 ^ 70 + 7639728977516624114141267041471180688166533758944024143443040523262400) * 10 ^ 70 + 3187487351907472462286916403304779660716655324973869319070995446963874) * 10 ^ 70 + 5117864583402264508528136227977521851880278518316733762754273291602035)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_92 :
Polynomial.coeff recurrence4Scalar1Second 92 = ((177398408470698 * 10 ^ 70 + 2369774277003872940952235822799527369737660946616997090713467418665096) * 10 ^ 70 + 6709027101959793295882003974142940892974137264658713047911867460496003) * 10 ^ 70 + 8424043645052424774242547486221240382475384720865526037506994128780623
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_93 :
Polynomial.coeff recurrence4Scalar1Second 93 = -(((3871622063605650 * 10 ^ 70 + 5683729452292173721279678166409427423653699848574225226070340491843954) * 10 ^ 70 + 9965899627252275177532641309869582987329939060585936037503457646189750) * 10 ^ 70 + 9384653924816338672730440954773088020779939828247303599007279882412329)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_94 :
Polynomial.coeff recurrence4Scalar1Second 94 = ((74040892164298664 * 10 ^ 70 + 8382648156904913237440992745922444143598605945246905516548796271420454) * 10 ^ 70 + 2883271271028417067456687168761049106915181957952017960681072210768570) * 10 ^ 70 + 3882243793893270583992720915820609412797997230570356335593435117273936
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_95 :
Polynomial.coeff recurrence4Scalar1Second 95 = -(((1296179283119867702 * 10 ^ 70 + 332853120593000070986621680290849568872788963797569720121562039681796) * 10 ^ 70 + 1222301021125128426729327535460568955154132596094607773444527233410098) * 10 ^ 70 + 8247623863600209136737737957046598981732979029589251492666613182247575)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_96 :
Polynomial.coeff recurrence4Scalar1Second 96 = ((21210572116093729214 * 10 ^ 70 + 9920040792130723163596115903005477670164814443077523189341828496782181) * 10 ^ 70 + 1698895064513000342779506508553733334867631117366124839129170074927726) * 10 ^ 70 + 1055644990890652259398728830375995152762185334504669034125335844528683
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_97 :
Polynomial.coeff recurrence4Scalar1Second 97 = -(((328286288918901576503 * 10 ^ 70 + 9201607462267648146147593301127808591236222392767571779867276397722308) * 10 ^ 70 + 9014559717350262081684427755311915792961664201787398933576053392461571) * 10 ^ 70 + 5244382636385344821140124678368390038598306501115875208055175266951335)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_98 :
Polynomial.coeff recurrence4Scalar1Second 98 = ((4841496915538642849253 * 10 ^ 70 + 3315988055841678782345611746868645924456441089048994053194551546773386) * 10 ^ 70 + 5427223795059958867172413293449403293755570279045286927093841954166050) * 10 ^ 70 + 6257975463202238913865732087919914183822351728111304210145756522451553
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_99 :
Polynomial.coeff recurrence4Scalar1Second 99 = -(((68377141619858681346852 * 10 ^ 70 + 3634839470802604180101169719412327074309827194349505463220497683576077) * 10 ^ 70 + 4228828271384341770143954938804297395390098082639084363354789982573667) * 10 ^ 70 + 9131065399487803059879394158146574644710697639250548373947647910184990)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_100 :
Polynomial.coeff recurrence4Scalar1Second 100 = ((928133314536126146210359 * 10 ^ 70 + 985619325104072902914416738585393091407367372620407368267472713377985) * 10 ^ 70 + 6709445686492279480940541077857300516864129885809079516398322846346440) * 10 ^ 70 + 7425689518457250047268237021165407964044767386715110716907846323783613
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_101 :
Polynomial.coeff recurrence4Scalar1Second 101 = -(((12140955885862257880671757 * 10 ^ 70 + 5857753288188636190196654574526536376341963021797240264030939597855096) * 10 ^ 70 + 969663397164393622294729489414491902335163603263964591301744135869675) * 10 ^ 70 + 4189591492858287895733218704468343095843011991503768187157320339646581)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_102 :
Polynomial.coeff recurrence4Scalar1Second 102 = ((153374874601805698632263933 * 10 ^ 70 + 4673779273104952837465251040116914726373111335112214584853600223839868) * 10 ^ 70 + 6378268306419969687897508141459592423788061474172378379351127288835626) * 10 ^ 70 + 6411621592952411693844474819416720824607223145258411107176585554041832
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_103 :
Polynomial.coeff recurrence4Scalar1Second 103 = -(((1874346454184736215579882574 * 10 ^ 70 + 9231191536175759483046586829873220831357966844878301859421293365626630) * 10 ^ 70 + 4907659300818294046925681853168161351037879682956598337280629910861074) * 10 ^ 70 + 9403676108778891052322117900453794862929617421950741059370934655918412)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_104 :
Polynomial.coeff recurrence4Scalar1Second 104 = ((22189402214568714762833258214 * 10 ^ 70 + 735373659499371906539249124439266590864133264735712428279900487911505) * 10 ^ 70 + 6770476753355856080148904781817167221914234811338892541993992460353631) * 10 ^ 70 + 3491303945967365630200356976913701595727381215560857121475331984825964
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_105 :
Polynomial.coeff recurrence4Scalar1Second 105 = -(((254771637661068648669697303203 * 10 ^ 70 + 375157157967061449378092993570250257607676187921349203399486854948360) * 10 ^ 70 + 555017315553816843375786998468374962383712271869478775490116453962237) * 10 ^ 70 + 6198422794766931947779216884111580534627048896520102798890381647800507)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_106 :
Polynomial.coeff recurrence4Scalar1Second 106 = ((2839899203498641273268502856365 * 10 ^ 70 + 5887197371087665400166642192422690405144374242124921424736780149160450) * 10 ^ 70 + 708261251587634368202148400654248603745133022659770659896824033948575) * 10 ^ 70 + 1884861127336086267414691692812443598338487293945496273395781836282246
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_107 :
Polynomial.coeff recurrence4Scalar1Second 107 = -(((30759627169648309360526610030823 * 10 ^ 70 + 8172157099996843007499007537529290080476610839752618540612637446796656) * 10 ^ 70 + 4637766535961882434573167396196284755727003299189734310993064497885483) * 10 ^ 70 + 727877066221767078372679615457726503266957943193344465355277679225983)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_108 :
Polynomial.coeff recurrence4Scalar1Second 108 = ((323981750858884384998736307093178 * 10 ^ 70 + 5797111033896282529992611107585557639911579640640866062303413400931237) * 10 ^ 70 + 2613233171755729004152937424916246675504064386449947576245346940692761) * 10 ^ 70 + 2193033388402788286228049599221454887977643616034889354746889978480089
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_109 :
Polynomial.coeff recurrence4Scalar1Second 109 = -(((3320628500362314448700453657291850 * 10 ^ 70 + 1387566410969661047686464330696173634839154130932808135126559696270099) * 10 ^ 70 + 6152027737242711025950991184025687153237326136987122158653216792595345) * 10 ^ 70 + 561629419707489416898304654299359188462208179320871941129134136145368)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_110 :
Polynomial.coeff recurrence4Scalar1Second 110 = ((33139785907859160065908972672443078 * 10 ^ 70 + 4956537578223738594905406531594718908768114109917118685699826261894910) * 10 ^ 70 + 448444536169309680009590018446377411881766561787545137514404654150359) * 10 ^ 70 + 1028529482302024229882168791085136353082563300541756538779227014344311
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_111 :
Polynomial.coeff recurrence4Scalar1Second 111 = -(((322220908185192319298113062845035519 * 10 ^ 70 + 5060603436085947457810304401894736081779861746806807153729237809490245) * 10 ^ 70 + 3880434923764594032392190416439022458826025078468261238263743707033595) * 10 ^ 70 + 4252841379759770488982606994303849452685602524492124545500360164350300)