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_407 : Polynomial.coeff recurrence4Scalar1Second 407 = -(((197342839341418878219543182672673524861221309490617512 * 10 ^ 70 + 6036263242084132743732641261260255418980905092164227908179947624067574) * 10 ^ 70 + 1269573849598008756798580331674321662020737955562280392122518227650948) * 10 ^ 70 + 6022730830277963705584126926026992755485927946656389946536872655668999)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_408 : Polynomial.coeff recurrence4Scalar1Second 408 = ((47902661510314414373161104658148306899162354191328915 * 10 ^ 70 + 1691071244616130893359239447831646068976578924419856784093677171334848) * 10 ^ 70 + 6629506460813541603284075074929838364894904695578478851419347717592729) * 10 ^ 70 + 4264280381618772696937813316437392979104031491472158377688973899495414

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_409 : Polynomial.coeff recurrence4Scalar1Second 409 = -(((9888178047154955098936672731725328940299791233878747 * 10 ^ 70 + 3999524106434544538808496445311943465541052001163502215232975928377601) * 10 ^ 70 + 8277396069389645658879835336079872543478968662632279560186707593551899) * 10 ^ 70 + 1838027704033591142725925084768929552827508183429492985214569175913783)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_410 : Polynomial.coeff recurrence4Scalar1Second 410 = ((1233732051721120079181612641539979474224460381414854 * 10 ^ 70 + 6274287230530843290460299046354790596310221512537424602579805372096023) * 10 ^ 70 + 5165784033065261779439585085486806844363003342629953732130938828054477) * 10 ^ 70 + 5522053189021253890413656253037026072987377601914028443165172275477357

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_411 : Polynomial.coeff recurrence4Scalar1Second 411 = ((294108853948480222233184489565782743275439494589416 * 10 ^ 70 + 8717313900302285659073011820490500048405902146327198828225327036021883) * 10 ^ 70 + 157417949461032369727898948064515807230217436203464829016093521464109) * 10 ^ 70 + 3605653711401100289758448365808318038160161727760973299331616622022076

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_412 : Polynomial.coeff recurrence4Scalar1Second 412 = -(((341077610711211461005612782330880983742121270508324 * 10 ^ 70 + 1705097736233375397450142309638556368845658699859409089385133791770717) * 10 ^ 70 + 7102503539297635480349691365596846369083277840240546508858082320480984) * 10 ^ 70 + 2375657528119136677374238911083049116918237314728505834939106041437493)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_413 : Polynomial.coeff recurrence4Scalar1Second 413 = ((197477222157082698374849120849098991125193899213722 * 10 ^ 70 + 9948305409927756407585236840959004967096214626211390144333808417970638) * 10 ^ 70 + 4734755489185461885395371537426848304155296334402744937622481193398773) * 10 ^ 70 + 9605084200524773525423458947477408209753177809015252489561329048148259

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_414 : Polynomial.coeff recurrence4Scalar1Second 414 = -(((94535290540730888657245240031525848465812096611607 * 10 ^ 70 + 5389408587264609688722747866030007857716902468379061490198889668708797) * 10 ^ 70 + 6908021595094153194990102059651895215009686954258950366088295409613855) * 10 ^ 70 + 2088794875480082463930753574374612538615399923982630024661399964596285)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_415 : Polynomial.coeff recurrence4Scalar1Second 415 = ((41268957385494173543071587671950933589508329080501 * 10 ^ 70 + 3834051136327395010366074149123265468972488847501687820101646386253751) * 10 ^ 70 + 8699729570491338269549873102031372645796225821455863251777007690251333) * 10 ^ 70 + 7094221566661472068782727742751581921119464943460130765452420246320781

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_416 : Polynomial.coeff recurrence4Scalar1Second 416 = -(((17051840138319194478383567872885347751180022896427 * 10 ^ 70 + 933337421692339075797431568107584331734728707987734120845344035500200) * 10 ^ 70 + 2946247031089326189265029983426504663129805577486828128449048651660195) * 10 ^ 70 + 8414595976496944241586262645464639232111260695818640543415545946581704)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_417 : Polynomial.coeff recurrence4Scalar1Second 417 = ((6792824170961851250989868128091885557430290243776 * 10 ^ 70 + 2592969955504189703290541344721703593436275592951413945484541826703186) * 10 ^ 70 + 181347929104868434086199949829275691791427863258256083422340054132420) * 10 ^ 70 + 484235682106909039229744307198637894006223045882025332175906983784959

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_418 : Polynomial.coeff recurrence4Scalar1Second 418 = -(((2635084378187742843847808356491551305592611648476 * 10 ^ 70 + 704101632420489504764706282868664756313340921559085039897014858254303) * 10 ^ 70 + 7752954432994996363385380723560256918314728606735228542168280309312820) * 10 ^ 70 + 4663334939891022916291384833132310982702721135919612293536040772661870)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_419 : Polynomial.coeff recurrence4Scalar1Second 419 = ((1000173412986725711208023835696053343998185436732 * 10 ^ 70 + 6010313038373899803907547079800599626613580590231780655025329714987598) * 10 ^ 70 + 3683313063508270122181915758316268313894440524169103319254187046550115) * 10 ^ 70 + 8872957509216936008890802716359829686407551785551172188892864776065654

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_420 : Polynomial.coeff recurrence4Scalar1Second 420 = -(((371807829502799115737428518600650730125893555126 * 10 ^ 70 + 3402912972602730029291739440809867361840307521720354815349895454668564) * 10 ^ 70 + 6439364709746062384220037588182295405840226515553789021303587184947934) * 10 ^ 70 + 4955977102069595720397397899356242098432805326393474230191489891709849)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_421 : Polynomial.coeff recurrence4Scalar1Second 421 = ((135133022265201231139049451105247412198414432588 * 10 ^ 70 + 1031497525840819225874081035631880979906067683464615188597501137794612) * 10 ^ 70 + 9312683302483185944427913052297406296440166642341263488709646422870318) * 10 ^ 70 + 7469604602865738430569179306477843692460424281442697507211050241215953

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_422 : Polynomial.coeff recurrence4Scalar1Second 422 = -(((47850735820392956004737170549187487486113020728 * 10 ^ 70 + 3371704252523713532473502788727761821665643153957568088402714289608321) * 10 ^ 70 + 3832527109040747624400330064346220074178535687778482635399479537725372) * 10 ^ 70 + 939289201914682967579761552888905091679512785924917162666178273059471)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_423 : Polynomial.coeff recurrence4Scalar1Second 423 = ((16436319519639913897030926971795301807640125765 * 10 ^ 70 + 1793472922111998073867373991467653897266415034915732510307951725267786) * 10 ^ 70 + 252675012410749541844636497354945410681563431122071123946117000527773) * 10 ^ 70 + 8184430346104323046616169028637572913406429857558199811966426390059326

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_424 : Polynomial.coeff recurrence4Scalar1Second 424 = -(((5451070772146209660234931260089090343272142834 * 10 ^ 70 + 4659980405412243157190456280644538591261979490376134277891482763311154) * 10 ^ 70 + 7980665778299842959810313167599282263643531510912603188077545050842231) * 10 ^ 70 + 4787273927024854043327365934964246683958420673106979599420242392822999)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_425 : Polynomial.coeff recurrence4Scalar1Second 425 = ((1737234751157640820060612544982955198813623533 * 10 ^ 70 + 7917624430182788857106933175064232949929599333479932457902189438387938) * 10 ^ 70 + 9181140969364269309071017455706383106691383228830404579608532245641643) * 10 ^ 70 + 1524381437024518209370380518074263054097912201251965862098422800799647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_426 : Polynomial.coeff recurrence4Scalar1Second 426 = -(((529412457316632246534172512706837625248289062 * 10 ^ 70 + 742459749091351718402176664617351895095142180115308806162553462833862) * 10 ^ 70 + 4892369226667352647065444943542960999190661113644520747076979244206759) * 10 ^ 70 + 4125055939854240974697856377796908198882755180272826950258736857538911)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_427 : Polynomial.coeff recurrence4Scalar1Second 427 = ((153422298173867828091172049431776081478930736 * 10 ^ 70 + 8281037521817512420142235823923894987486977323848290614885378049379147) * 10 ^ 70 + 8537007069037064378033212781461957070625019849028827309135995535165208) * 10 ^ 70 + 866614013086360220722089730221564332111022750922892956699740352537649

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_428 : Polynomial.coeff recurrence4Scalar1Second 428 = -(((41988082481289730584289189769388474022453313 * 10 ^ 70 + 7693837742436422345347659892730968419964341485732348358142779348386517) * 10 ^ 70 + 9551709100800946740494894944483611636708421909451492442404912591227398) * 10 ^ 70 + 2381973663089424221702830214254881679917135771268176037468473719082024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_429 : Polynomial.coeff recurrence4Scalar1Second 429 = ((10744851418692215432967219419970507566610085 * 10 ^ 70 + 1464579179578927576982061696326823557064110427129607698485329602139093) * 10 ^ 70 + 1435654820100714437214071532818508545278987550591709621809351310628345) * 10 ^ 70 + 9449767094519232586761278650041147192486387837755741174194521277187377

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_430 : Polynomial.coeff recurrence4Scalar1Second 430 = -(((2529720105399123953160921069860764773701933 * 10 ^ 70 + 7194580093163464077450055440937785557896598321655622999804878889330783) * 10 ^ 70 + 8471147473703412304147707626966439105348583641966161378474656785737207) * 10 ^ 70 + 3280975815047262828579134045373624053975746372669736570774043736324093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_431 : Polynomial.coeff recurrence4Scalar1Second 431 = ((531205487321655085151948105019997209066015 * 10 ^ 70 + 2910732010946592519287718880227315462831915131489936710363460724704983) * 10 ^ 70 + 5666851882753688458967609464449544909852651901888158086733122990860469) * 10 ^ 70 + 2475003918938601869347856436588992305497232110753093557660419386333184