Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_199 :
Polynomial.coeff recurrence4Scalar1First 199 = -((((33334301687612012598 * 10 ^ 70 + 7153394288145621001811861761630609588609653815052690355934976521470271) * 10 ^ 70 + 9077198868342161173744342309482761886848307453643405632536457405532762) * 10 ^ 70 + 6665219391368310357522549035225556409023818390124540098626364548973682) * 10 ^ 70 + 5597718022458215720073556556255481086976118306638713716044482485252948)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_200 :
Polynomial.coeff recurrence4Scalar1First 200 = (((69162992013725486778 * 10 ^ 70 + 7756566933852577513412089742390106979180457166946265114085674063678364) * 10 ^ 70 + 2182981612602822056967852455816096354801958338370186557036259789478744) * 10 ^ 70 + 8117242593685909066199204581960812504812984209115036986394117976589920) * 10 ^ 70 + 2569110226730788933610985612430772090827253438110234275244760542728674
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_201 :
Polynomial.coeff recurrence4Scalar1First 201 = -((((141512393825663658579 * 10 ^ 70 + 4059900639919335065841784821339120637312414353455290149087232163648606) * 10 ^ 70 + 4373279447321892968254007253353689077408169964916495507114207778411929) * 10 ^ 70 + 5023389649983583419794705813168908671254394090135383640139744248884863) * 10 ^ 70 + 8177318517578168852083281128265783582613421786702720028330308915984648)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_202 :
Polynomial.coeff recurrence4Scalar1First 202 = (((285537085211416321276 * 10 ^ 70 + 4250663156103682285074148271592959076094808570621570019250314000753036) * 10 ^ 70 + 9984512621594407520702740623171821428448303692373476032500893161776298) * 10 ^ 70 + 3787090572514745961721323117325822950932898512777357213084451914996899) * 10 ^ 70 + 6058345130923412899311852941373531142574083511003210124014062542000738
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_203 :
Polynomial.coeff recurrence4Scalar1First 203 = -((((568180651248590433424 * 10 ^ 70 + 2169080884497708384941028582010690459461635149855557133914139343805791) * 10 ^ 70 + 1314114416032038382535620414888637229511334705838490384678112762353331) * 10 ^ 70 + 3550975483848603310434204076026410262844344578220234521931609013545836) * 10 ^ 70 + 509738787623754719090646376222656831153033053910234971871232197930007)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_204 :
Polynomial.coeff recurrence4Scalar1First 204 = (((1114998425139320226494 * 10 ^ 70 + 8337043065109263196374911590663675985264720548219682995644552050585927) * 10 ^ 70 + 4111124591959224235748530375161374327884443986801838273280283945138105) * 10 ^ 70 + 6581091687556004860744946817387858645426308849616523338262263249589659) * 10 ^ 70 + 5735703365025071481327924887771289143131602499555046872667754293992867
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_205 :
Polynomial.coeff recurrence4Scalar1First 205 = -((((2157910700345712403562 * 10 ^ 70 + 8329109498125884669191913650405048585086583230082081771451022694333105) * 10 ^ 70 + 6664264995501783522071238094164257144619026557860775576954134687070718) * 10 ^ 70 + 4264736567553358220840848081697566706673228606419944762762514514587603) * 10 ^ 70 + 1407086369696016266323280201282330190014070638634395375154042660649153)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_206 :
Polynomial.coeff recurrence4Scalar1First 206 = (((4118803466226056535843 * 10 ^ 70 + 3692195948456040283220253524865936912241726721866362136825412262339912) * 10 ^ 70 + 5290820642441706580653461585101276817951795831144295990625344437453951) * 10 ^ 70 + 2078347395051221401194396187963561029937110253685162839104476454722495) * 10 ^ 70 + 3274728423019557531654384838733680471653935356095803998789127965725640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_207 :
Polynomial.coeff recurrence4Scalar1First 207 = -((((7753423706953786209375 * 10 ^ 70 + 4447905297642123372333043171097145167930772301788916984953715867688006) * 10 ^ 70 + 2944408324347190167572832683473900660718577181666403110282047800279844) * 10 ^ 70 + 9933086756563556681931778796226051437329005245225239856624333528786242) * 10 ^ 70 + 1360311936430006002283408969881127527262602438831605609202164415694934)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_208 :
Polynomial.coeff recurrence4Scalar1First 208 = (((14394836724349028518315 * 10 ^ 70 + 5078142887257631002490189960731920957057170453817432644320122339962888) * 10 ^ 70 + 9422631237982095985226101382985925490050646008415982261434095898111882) * 10 ^ 70 + 8767029387512814207638862511601535260472210300356104390028248286231797) * 10 ^ 70 + 2821431408514861896436841404807996838600509031543837445260912277519619
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_209 :
Polynomial.coeff recurrence4Scalar1First 209 = -((((26358223551158121310795 * 10 ^ 70 + 5677147455065166854944402779264837935433909628885187965654957775463830) * 10 ^ 70 + 1379600728930662143872075649521005952153377156385362434274034891194666) * 10 ^ 70 + 5750869517898195837189321076841718124642613579705118386470937340592713) * 10 ^ 70 + 870967270134207401879408034922584285888370402382504726397148954168197)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_210 :
Polynomial.coeff recurrence4Scalar1First 210 = (((47602147238673567794890 * 10 ^ 70 + 1917322907208195451032503019419653341756829544734890765204944633657743) * 10 ^ 70 + 7558646007452475139548184462989062447809353631327843553575927545894958) * 10 ^ 70 + 7109265099024426912010325896549101085724155535589463958718763195991398) * 10 ^ 70 + 5399795912926250926466965976232126848934830415831435481226700988483682
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_211 :
Polynomial.coeff recurrence4Scalar1First 211 = -((((84789533949811727781215 * 10 ^ 70 + 3036235528233401546342328036451519396462276739458704363978119786989721) * 10 ^ 70 + 818832244228324222130314437716364587539664462882722097609503268450728) * 10 ^ 70 + 1448532652729514493102069414268928443399878340360592631366414362711095) * 10 ^ 70 + 5472145276336242426679485969676089341547830304672509925047415666638353)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_212 :
Polynomial.coeff recurrence4Scalar1First 212 = (((148959075222915528934275 * 10 ^ 70 + 4410881501877180725354112142126611506419551767742990648005575380454373) * 10 ^ 70 + 5415193526723876553745283571474983062541867889457080652290819511755373) * 10 ^ 70 + 4253750994136186876790784935598780057960073131056917806488763837624698) * 10 ^ 70 + 745730301035589178816699836391204993622836671067407265345232066909014
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_213 :
Polynomial.coeff recurrence4Scalar1First 213 = -((((258109406867856764386401 * 10 ^ 70 + 8419542223847257148016540875075190865985050716751840844550557483522336) * 10 ^ 70 + 6808232885269325125476937959903188567931967577112250811077316508543917) * 10 ^ 70 + 4533937349739316406919375039320482502131969406614825153628213165814374) * 10 ^ 70 + 1400299585052137665273333768582429102786474614604799673192292116308951)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_214 :
Polynomial.coeff recurrence4Scalar1First 214 = (((441118605010206421256039 * 10 ^ 70 + 9476497768043720733965181925133907422711641638424650580927576980913688) * 10 ^ 70 + 9031567334340886287214223287704914827216073473426153352847359273977940) * 10 ^ 70 + 2710548659634389419084194291144361318348590463812259075627201043680456) * 10 ^ 70 + 3075042515355827747322629101928720758195177740047450973183125372690592
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_215 :
Polynomial.coeff recurrence4Scalar1First 215 = -((((743572820632406725470654 * 10 ^ 70 + 9347688232133876312025395233434880858502418269381622725547419326139513) * 10 ^ 70 + 8571053292419865147629763134346079722124900453766896701667157429104730) * 10 ^ 70 + 5618964263627169042682797882327533074607936877498933765201785671999459) * 10 ^ 70 + 4988516215061708092547620300645084768195079591411403390276076365455591)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_216 :
Polynomial.coeff recurrence4Scalar1First 216 = (((1236259092293616667992201 * 10 ^ 70 + 8856047240483839263773531247019754097980998740208195113278048298252069) * 10 ^ 70 + 2325105735243752514055846294827643139216798452160178310749457772186698) * 10 ^ 70 + 7630310159147785572149741197907290119013214994546011076376968946205036) * 10 ^ 70 + 6429133691263442392254369015050658947603711335355512101823123702855946
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_217 :
Polynomial.coeff recurrence4Scalar1First 217 = -((((2027281033799867708117233 * 10 ^ 70 + 4517653953344951368427036983446655993634560530586621314918850220840373) * 10 ^ 70 + 370765166673595523057060010749160079061054635330351204130716441451318) * 10 ^ 70 + 6377752752965198500985620132457750129503656230097126068464282155860234) * 10 ^ 70 + 7470791157742357584129565248708285121657478103509922974579147990040252)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_218 :
Polynomial.coeff recurrence4Scalar1First 218 = (((3278965120535623222298113 * 10 ^ 70 + 624760066741848331722925969358026262573988774011544112574496360709298) * 10 ^ 70 + 2630835380497655124604608112781839603233443269766172630438036946130127) * 10 ^ 70 + 9983106603416729423521459264019984638053410087072775543819015390984469) * 10 ^ 70 + 7448099927087610518330462955069106047180983330973613327821819154010914
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_219 :
Polynomial.coeff recurrence4Scalar1First 219 = -((((5230909518449981966126054 * 10 ^ 70 + 5506344868682560512198757002831765339931014729734917962239657745302223) * 10 ^ 70 + 530493986927799897643667095989122704780095115937898271194734294175688) * 10 ^ 70 + 5604260250264995813447078648384060848799623373231071249477078944380358) * 10 ^ 70 + 843981271324311078394040193921590663432001661109376307608722563981889)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_220 :
Polynomial.coeff recurrence4Scalar1First 220 = (((8230640278539872528873172 * 10 ^ 70 + 6528998960052696224039407760368809716286586559555937854340834037447526) * 10 ^ 70 + 8447403750929803097131393508853099230036872207194169143202079776659464) * 10 ^ 70 + 1614468452846729616814974884821041607968051475529134691317789990845611) * 10 ^ 70 + 7301292119497364719172059179771076594808760698876441019032257523944085
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_221 :
Polynomial.coeff recurrence4Scalar1First 221 = -((((12773316344352990734577432 * 10 ^ 70 + 4758077973340417394384067339568269755576082091376230481749701383613599) * 10 ^ 70 + 8596139948728858378027561449881448054672165960195792301448299896846593) * 10 ^ 70 + 8907886366472433673329752853153755454652203295609535964411567671657575) * 10 ^ 70 + 9137825926429224584505474845702799516153184295287544502304383823405882)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_222 :
Polynomial.coeff recurrence4Scalar1First 222 = (((19551682401096539805108202 * 10 ^ 70 + 3020328077590498408786458048121708490044026311241068217616115392595486) * 10 ^ 70 + 2734252200135278105088762687151956131124582791865678607148072542162262) * 10 ^ 70 + 2113079938483212537816543778453901860440113705653224550990112793173134) * 10 ^ 70 + 921750210529800875517885968120697476927544348356037164992583873662820
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_223 :
Polynomial.coeff recurrence4Scalar1First 223 = -((((29516911021773660894004966 * 10 ^ 70 + 4213595571684149325216706461036520313658733355322176508627476912263164) * 10 ^ 70 + 6496887489100786076354623243522551748398242593338918363253911616812390) * 10 ^ 70 + 295892606678927358489044441415508210379010120331745398510065631756198) * 10 ^ 70 + 4220078484948160335016768397861695547140927997857466546558025590593201)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1First_coeff_224 :
Polynomial.coeff recurrence4Scalar1First 224 = (((43950003556407378874174338 * 10 ^ 70 + 1169039051941170832449939225651477394037465847425348471519391333286399) * 10 ^ 70 + 7881028558131970201669554763515493807832746132665455324918429902985868) * 10 ^ 70 + 4252146155590442433443481487181932022934024065819166380193301900613114) * 10 ^ 70 + 5433633950877201749630271146166216735239598385738150598900816042634987