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_329 :
Polynomial.coeff recurrence4Scalar1Second 329 = (((1564948852488946 * 10 ^ 70 + 5002284416799171889326670652693554830635590668414042253546631750757042) * 10 ^ 70 + 4929955032225618770305671271169460752491280172048703408377601261092780) * 10 ^ 70 + 7967214195604257592775016640143154641871942029017213637278812431154430) * 10 ^ 70 + 679219101078906535356640684667498332104539683559143429977680659293015
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_330 :
Polynomial.coeff recurrence4Scalar1Second 330 = -((((284068805941796 * 10 ^ 70 + 5264892449291446989172676329973938740822210208469070259180880968683296) * 10 ^ 70 + 3223790562027551388433424041604945852112490821978342789480749048434540) * 10 ^ 70 + 3388246223839525152374786901326012053669748622252412334623636603962307) * 10 ^ 70 + 5547168344594555341385629612501415512629613656392991181432224337752416)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_331 :
Polynomial.coeff recurrence4Scalar1Second 331 = -((((91388241949117 * 10 ^ 70 + 1554450940794323706727639428659157305204806950936929272851125812504173) * 10 ^ 70 + 4862896977283963510185170256357825374787037123769366912281883161330487) * 10 ^ 70 + 625965027391067559461608574579976542273283980080852980293000773705036) * 10 ^ 70 + 2689547730648856894973362819140434907188494675781797064851380446493607)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_332 :
Polynomial.coeff recurrence4Scalar1Second 332 = (((149732367351428 * 10 ^ 70 + 2168421658703280369210554731067995932435179601461437300551057861307918) * 10 ^ 70 + 7171034710791322574325701494661381026879674144923662281554834711545112) * 10 ^ 70 + 5293047365929670664909288310505508953206803478970954163282418953483757) * 10 ^ 70 + 74681153205448371053757214856029640160486870422953287504632068338550
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_333 :
Polynomial.coeff recurrence4Scalar1Second 333 = -((((118635511584991 * 10 ^ 70 + 7143010144914365499900245153323778978547803346418695089108603930149673) * 10 ^ 70 + 8229767145572184102777866356995989829964337753977779862669393346141814) * 10 ^ 70 + 5381115853106473066586746850564346791916982945814163108495567947997927) * 10 ^ 70 + 907146541216938367505894333704296531735880659252922803501546187619863)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_334 :
Polynomial.coeff recurrence4Scalar1Second 334 = (((76418359381077 * 10 ^ 70 + 2282771969627363840133985009884878474476887224410394020506571416362641) * 10 ^ 70 + 291873935874210028149615602663831832053166375299113070414059056317527) * 10 ^ 70 + 3839887939828364442590321836617876728145130041214347182647442980143497) * 10 ^ 70 + 2063319446440599405444952832625827556950817484609868181834362190553812
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_335 :
Polynomial.coeff recurrence4Scalar1Second 335 = -((((44202133655079 * 10 ^ 70 + 9648680232423649243850517703340018513786235627750020102733009427038929) * 10 ^ 70 + 4864225327235392352503077942507974150369202429503396786371127343499641) * 10 ^ 70 + 4861540444216792939981748375819848153233087719624160331888199881292293) * 10 ^ 70 + 3703661387291229858366103315478622793100937148257487174835786107283366)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_336 :
Polynomial.coeff recurrence4Scalar1Second 336 = (((23818808112348 * 10 ^ 70 + 8585577665061556522541652633966761623619903240265354471986863390345173) * 10 ^ 70 + 9796649201550444054213708151277141499948603143898098966373171995650769) * 10 ^ 70 + 2876305057943377828449649656261432823317103806788440380621036942430399) * 10 ^ 70 + 7886213732983233764028363066911601813724757381000347602849611228917118
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_337 :
Polynomial.coeff recurrence4Scalar1Second 337 = -((((12166923266844 * 10 ^ 70 + 2544804605165292462975354668601558273808465672646603850418795398289463) * 10 ^ 70 + 6211541271948088220166951700592921280690365337060279805325916795322763) * 10 ^ 70 + 7869237625160612983162549206807266275561576903860356852460408150517709) * 10 ^ 70 + 229297291386389358826426263449146274203575267761502628072482902414907)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_338 :
Polynomial.coeff recurrence4Scalar1Second 338 = (((5946477239518 * 10 ^ 70 + 2911699997068631514394767841056197395254464270615242368527331242916170) * 10 ^ 70 + 3397965647259513161861102410067512335609055125511501889875697875740309) * 10 ^ 70 + 2152753065736358235821389355148862261611547353253110863770450728846069) * 10 ^ 70 + 4877641758063788288918101971963400355780826691940464522125919603278011
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_339 :
Polynomial.coeff recurrence4Scalar1Second 339 = -((((2795219396364 * 10 ^ 70 + 881278632624474403704246151554384227696406869253103324131707460018754) * 10 ^ 70 + 3395845613556906334465691439834480501401634635183649907979738791360381) * 10 ^ 70 + 7451836783419799060243521888963129829416665844791895614122676046234070) * 10 ^ 70 + 4654440512102835813675645662599037613787707700639157295618644536437433)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_340 :
Polynomial.coeff recurrence4Scalar1Second 340 = (((1267264266607 * 10 ^ 70 + 9478991304638747974534497562825725419986135833466057495808976217872886) * 10 ^ 70 + 4417275313480466014976938987827229052766457626790574302098903693422247) * 10 ^ 70 + 3151976808293958210998338367818987922950178863900341089302182089874890) * 10 ^ 70 + 6278199877545200053074968714517544983043636407975560528714125434514912
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_341 :
Polynomial.coeff recurrence4Scalar1Second 341 = -((((554783167830 * 10 ^ 70 + 2090554907070674988204784863980498029547475228944248309966005458860261) * 10 ^ 70 + 4931312398374771892486233194852841186697421079293046500153594031931141) * 10 ^ 70 + 3026662175464122749331668900186410067524711465303214065560670576307711) * 10 ^ 70 + 8888546009952782254964282115016506251593386268525778242709402934934771)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_342 :
Polynomial.coeff recurrence4Scalar1Second 342 = (((234489189767 * 10 ^ 70 + 3568477183806866642659625589729870284423400283812997118692709139394204) * 10 ^ 70 + 7509244081877590975208574286943831908127465695727082597888223089525443) * 10 ^ 70 + 7820236651279140133754060929620216209683567436321000990855759218949628) * 10 ^ 70 + 788097248935923727642847800525241374070581440685693405659664796665852
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_343 :
Polynomial.coeff recurrence4Scalar1Second 343 = -((((95553772268 * 10 ^ 70 + 5263849980298275536506988762816260760061322775648605076555191008836153) * 10 ^ 70 + 6491109183393198895236431843168725765315324027126896764548552934217175) * 10 ^ 70 + 5790363556435226806310010194525090607672764285093205476605499719573578) * 10 ^ 70 + 7138110435121276370515908974583335572895054722283003812673364295409233)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_344 :
Polynomial.coeff recurrence4Scalar1Second 344 = (((37430392709 * 10 ^ 70 + 2274880251187195290919574908926633354274191816284732199442480411442158) * 10 ^ 70 + 8457003292626280360465826401353039557194952033916779279025539408666855) * 10 ^ 70 + 1485888478893403426992500185423533642069640898420728986536026554620795) * 10 ^ 70 + 9040936578825493032621110998486428814207856084117613024709426305286508
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_345 :
Polynomial.coeff recurrence4Scalar1Second 345 = -((((14023791235 * 10 ^ 70 + 4565468965022275676633410937556441709073706765841502340401041602135504) * 10 ^ 70 + 6967283154012481475374882933763281374698887446528239307939810822956949) * 10 ^ 70 + 5431950015836006566380832050840751785309028549728684140135858546962000) * 10 ^ 70 + 2188190665064307752623451033500774344500716408589544134360602146028137)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_346 :
Polynomial.coeff recurrence4Scalar1Second 346 = (((4983303542 * 10 ^ 70 + 3697350076132061901097435397729013616198744071316082560387651466473525) * 10 ^ 70 + 3748924767067185967391631390848913191001568708525978780331128441448708) * 10 ^ 70 + 7026785074227459100430813666395266119753991744045127000255373397053261) * 10 ^ 70 + 4687883873665776966778576962547977749705452439795674118993807072404070
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_347 :
Polynomial.coeff recurrence4Scalar1Second 347 = -((((1655091068 * 10 ^ 70 + 9856990734010452171795339540954628931716011290713724887256837873706627) * 10 ^ 70 + 9314851066276395230476531499407034844062536005909063821792789207992264) * 10 ^ 70 + 4034396907566737093988036521536066968736789504669329350105272096669518) * 10 ^ 70 + 4320381102672448524350899259853941027429730650624244001990961353814207)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_348 :
Polynomial.coeff recurrence4Scalar1Second 348 = (((499513176 * 10 ^ 70 + 2012053249728911176476588436935987093894155844192126555029306183058560) * 10 ^ 70 + 2988263044682779874727081396864011027799626193339033836316005313283786) * 10 ^ 70 + 6461974610004071636454062798325892156976104172396401590795464236329433) * 10 ^ 70 + 6585876352924479854519049620866142494132218621599762683015261247728491
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_349 :
Polynomial.coeff recurrence4Scalar1Second 349 = -((((128299472 * 10 ^ 70 + 2700587375529324322248026993449919968273772122054976075226680388148525) * 10 ^ 70 + 4434958396946960596083321020849497489336902645542172334385709001779783) * 10 ^ 70 + 2685129443437834213955371390285585132841195502539858444576451374772846) * 10 ^ 70 + 9505230102923452327804292633384776885318157391036302383898591448315762)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_350 :
Polynomial.coeff recurrence4Scalar1Second 350 = (((22265248 * 10 ^ 70 + 6509560275657764650187438565274459792087406552224759338383614072181406) * 10 ^ 70 + 7215669302051831154297684216788534629621529056655130048944413922370453) * 10 ^ 70 + 9793215818983655665853392143430441123383993117919444446819571218900668) * 10 ^ 70 + 6443278337489699153451276808050919293916624922909197654443089435703880
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_351 :
Polynomial.coeff recurrence4Scalar1Second 351 = (((1947680 * 10 ^ 70 + 6844471034796808775993083411324599079771458363160516584711378400477860) * 10 ^ 70 + 3091667224223912786028375860204082853636799872715135532300774586046771) * 10 ^ 70 + 6965744813661161035345261308569812967244502988154377844076071871154724) * 10 ^ 70 + 7841256995403067391721051773782433512269257421765657814435926795610872
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_352 :
Polynomial.coeff recurrence4Scalar1Second 352 = -((((4429647 * 10 ^ 70 + 5995810997740324804685867986760306712771405357998200845658600227420134) * 10 ^ 70 + 8073051016227687061970725515388163868705679558389023524598079191691469) * 10 ^ 70 + 5762076652170489464387577896272632839998125579339361751899731947026859) * 10 ^ 70 + 8849088582958839191595866897069143503908701196702320660747278929533858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_353 :
Polynomial.coeff recurrence4Scalar1Second 353 = (((2814664 * 10 ^ 70 + 9351169493818072339389760232301118164783988498590482328205101103283407) * 10 ^ 70 + 9581862274113247872404466259320900457608420283964129104505872756340062) * 10 ^ 70 + 5026600931171189700045787673289931800218481697745925312455009898286750) * 10 ^ 70 + 1660521555572832830625397159946509606436591852790496782877817317306318
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_354 :
Polynomial.coeff recurrence4Scalar1Second 354 = -((((1330199 * 10 ^ 70 + 125073169391910126565367055095551849819376614754319164410442957320281) * 10 ^ 70 + 1120015074651738933624778340546228750209323323813544636480936721218505) * 10 ^ 70 + 3802312274103764514391487654145015863040634449691806492350583662911362) * 10 ^ 70 + 9607361002619707384313721313644889522752968568778721957073912090283265)