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_171 : Polynomial.coeff recurrence4Scalar1Second 171 = -((((379331340 * 10 ^ 70 + 2025519456421791050442361403180932549200610431124297876494272567796854) * 10 ^ 70 + 1669010838322683408253580561409906206451679956344938848570204021562357) * 10 ^ 70 + 4351742156269382736513391341109883248150482859686816421867923281186682) * 10 ^ 70 + 9663955970881482448801929099123676128677776974511684137450006817079245)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_172 : Polynomial.coeff recurrence4Scalar1Second 172 = (((1174667779 * 10 ^ 70 + 6045500313201050980514617689719967240497350605171971795863702906474501) * 10 ^ 70 + 3193590787583793335287131221179874839872063879249355212192740300188770) * 10 ^ 70 + 6381144274580847876344235790035592606824412842484236312834303302162137) * 10 ^ 70 + 675708267941046533893403023441627402892402678359927371566207314276430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_173 : Polynomial.coeff recurrence4Scalar1Second 173 = -((((3582752430 * 10 ^ 70 + 9260400994081662052051910489366107099144139061542410419427294253911987) * 10 ^ 70 + 4886572409242860749992232105846592130183287278444208277823823027692775) * 10 ^ 70 + 9943538069731813594401841438478653016305337088490399499352261397471431) * 10 ^ 70 + 8308667859504557448901013841272009432158265608154085173226315777494551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_174 : Polynomial.coeff recurrence4Scalar1Second 174 = (((10763347471 * 10 ^ 70 + 5765655602825958454805056482042911316509295493350990576715062019214611) * 10 ^ 70 + 8555953272969314884092184348885381704893327613222290382149489801695916) * 10 ^ 70 + 9930704826322530389279341946318557743935203795964302161761735249999213) * 10 ^ 70 + 4393829119992655695972129698478594947392861958905685825254936261859117

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_175 : Polynomial.coeff recurrence4Scalar1Second 175 = -((((31851458979 * 10 ^ 70 + 6466041617621558988358458821670357051478936824630066330692119584787079) * 10 ^ 70 + 7664598258385067892979669078665347604776549519876877435973444656179891) * 10 ^ 70 + 9193905781500177010928352939651012287708857691018792158069912102517565) * 10 ^ 70 + 6657636882290283379436159267615854571284127622489995701349770944182252)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_176 : Polynomial.coeff recurrence4Scalar1Second 176 = (((92850552179 * 10 ^ 70 + 362983368620642076727993887486240474490239291714674366356396446644672) * 10 ^ 70 + 3621209832922228552502400193261982997407996467976716526746416296229501) * 10 ^ 70 + 1171499050029813202921726752392326285291337364113256258346705192927052) * 10 ^ 70 + 9627314440404112667143365935327775133805691703263602557032951745531778

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_177 : Polynomial.coeff recurrence4Scalar1Second 177 = -((((266645235468 * 10 ^ 70 + 2663928539905993581389914872605663139677121598715616399975150823245565) * 10 ^ 70 + 8192302930664078084874497236167333578759521591595994291375882967324317) * 10 ^ 70 + 4001899142478251556844728515471906157982145527271446457170344360785286) * 10 ^ 70 + 3123327579975484768421571834551326457679358546268906895360299067860123)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_178 : Polynomial.coeff recurrence4Scalar1Second 178 = (((754392806335 * 10 ^ 70 + 1722478670385838825466443731962785203964540436700112329624909827515013) * 10 ^ 70 + 987737565360265267857916185280322175428582317290839363176150781762372) * 10 ^ 70 + 6102906134297343927137200364201056824235468622463099811912300350908873) * 10 ^ 70 + 3307005790017800032334005754707682577224393216404347610884904238613047

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_179 : Polynomial.coeff recurrence4Scalar1Second 179 = -((((2102785810000 * 10 ^ 70 + 7347328044101422810567723229063045870366668564111693929959431248946013) * 10 ^ 70 + 355040989261090970817874423898092343163275601223336625798902641020511) * 10 ^ 70 + 5501028485561669013374094692469079106881422398109273440535938028003743) * 10 ^ 70 + 7760475087452057996917470433474763562614432572131417104817578938642438)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_180 : Polynomial.coeff recurrence4Scalar1Second 180 = (((5774906611160 * 10 ^ 70 + 2903596263216448156557652070681638141836886604454795708270988623923992) * 10 ^ 70 + 7437405546995954872429414490859131249126495772920269339730685978526774) * 10 ^ 70 + 9519712776532907545119673906504457088561198983172622849024230491083146) * 10 ^ 70 + 1489351438060032664966259443864236121356805624524102184587859774098146

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_181 : Polynomial.coeff recurrence4Scalar1Second 181 = -((((15626625031903 * 10 ^ 70 + 974058772322289586704097429792469653630571007459620701651034745832807) * 10 ^ 70 + 3856913854930053479913778809252766975896458324552447991848677186824972) * 10 ^ 70 + 9543712156353026714162271092350235738705797340765079920847127609242838) * 10 ^ 70 + 8325986563068960344341848401723804369371249165102360634523057580982904)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_182 : Polynomial.coeff recurrence4Scalar1Second 182 = (((41665137315683 * 10 ^ 70 + 8970722784344337674015223979515473963127573043809937860221950924114715) * 10 ^ 70 + 1680408363660627555179241196188128138855816665657405231826109527397659) * 10 ^ 70 + 6215124902765075078463008961138291341206527248278817207349062979590963) * 10 ^ 70 + 821731680116217177961222802577510155786020097571202388385433246117706

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_183 : Polynomial.coeff recurrence4Scalar1Second 183 = -((((109467243529294 * 10 ^ 70 + 1079966462664216603459997011778365905432095330884012518934778494937516) * 10 ^ 70 + 2666487469934542233658264693624108437394595719457697981477498575334036) * 10 ^ 70 + 2368807397712093272152123020564615673375122215015427618671576642544643) * 10 ^ 70 + 3399428141027525470258060573542690394421946440523580555945927523834674)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_184 : Polynomial.coeff recurrence4Scalar1Second 184 = (((283409797828383 * 10 ^ 70 + 9792899914098023284908964259658522329295594229473304018537653652250553) * 10 ^ 70 + 7090889768262429216027463415296515827473269213394672398493996838954073) * 10 ^ 70 + 8953117397690903470374249484609006271835161802965896627335948032189106) * 10 ^ 70 + 2674048286524621543071773326370301141410178683440666689454612383975477

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_185 : Polynomial.coeff recurrence4Scalar1Second 185 = -((((723068865114584 * 10 ^ 70 + 2064816794054115495681274184444270411104187261340778998652126318534889) * 10 ^ 70 + 9939340802673472694051436287360401681507913052680749976977050807062730) * 10 ^ 70 + 451292034080660559056119632945655727090675131971669321244611216723496) * 10 ^ 70 + 6332480486379089858312397984554292956547045072000634439587238174874252)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_186 : Polynomial.coeff recurrence4Scalar1Second 186 = (((1817994771669666 * 10 ^ 70 + 2979674519524668033737642381883102266868432744098689245039559380389402) * 10 ^ 70 + 2392500199768059091069678752667751387262647745668482431618706975509220) * 10 ^ 70 + 2670744402208539858187272245833034633898845414220086855437508161574623) * 10 ^ 70 + 1057180581814110817727533624466387902466614908360826224884852840840419

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_187 : Polynomial.coeff recurrence4Scalar1Second 187 = -((((4504712090868252 * 10 ^ 70 + 2064640706180803333698628747418796952321535811784418146854632104547099) * 10 ^ 70 + 8946030747755242151636881782129139517661434452514282173247012855206663) * 10 ^ 70 + 249267387936074878651234750698472726357565284599291214860850707619611) * 10 ^ 70 + 5886747439252685271821942405124648748923381654578320604872631888149893)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_188 : Polynomial.coeff recurrence4Scalar1Second 188 = (((11000575019393155 * 10 ^ 70 + 3619247022841401780699622181932462490705451907960629429737571244594566) * 10 ^ 70 + 9135196409389413291744811233044159289344187738617545409354672816974807) * 10 ^ 70 + 5119668889516189936133358146018830053394241689159400145401449069953781) * 10 ^ 70 + 4024994682871581126867375600116450259815740656623936231174110153933310

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_189 : Polynomial.coeff recurrence4Scalar1Second 189 = -((((26475818049102666 * 10 ^ 70 + 1250262391288337662775116726538819882148335543749095366626298478422713) * 10 ^ 70 + 3541385814148952396065832691105098148394197301579420315855393775711885) * 10 ^ 70 + 3872609677290620983273246376711395165248655031884374963695935655819133) * 10 ^ 70 + 9390358502714950221814746169304347300912062869116295856584801323193556)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_190 : Polynomial.coeff recurrence4Scalar1Second 190 = (((62802938172764783 * 10 ^ 70 + 2693323810119720817824163753239628499184999887638999735945730319856325) * 10 ^ 70 + 4755503096861328428207075545937915807649009557969031253493298382253012) * 10 ^ 70 + 2552007277566528596199428751397084587000058103153785098805730609385715) * 10 ^ 70 + 4935767672483599580554678471323976143355942431672163686387286868409930

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_191 : Polynomial.coeff recurrence4Scalar1Second 191 = -((((146830820602003694 * 10 ^ 70 + 6063438165185514805852654489850894677898384341351382772320329036701449) * 10 ^ 70 + 8242650149428993802797720404612900921892671616353153637980246569990134) * 10 ^ 70 + 8166652636105912252455605731868386397544279312890011070636009956885161) * 10 ^ 70 + 7793919985299261848928664405887538888792945920896536892628207418861530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_192 : Polynomial.coeff recurrence4Scalar1Second 192 = (((338353345240546592 * 10 ^ 70 + 2080817492023757257373367679586169291134074479751636357790468836182999) * 10 ^ 70 + 6423687920521624862697861184272255854531867638567098819933824945252512) * 10 ^ 70 + 3377798361728039003190183519547192927049243591479851825987170137198482) * 10 ^ 70 + 9775028037370858546207158696081790258617808353467075432634620222149926

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_193 : Polynomial.coeff recurrence4Scalar1Second 193 = -((((768507600102419829 * 10 ^ 70 + 8281822655664984210997357959586611344242693420132654001185120804790555) * 10 ^ 70 + 5667124428727750481810344881534531700113552535392820562765628795835754) * 10 ^ 70 + 2151348443547091025745482871554044427041119961435005138810021081623939) * 10 ^ 70 + 5961113918393741395915107237191637880088903688877798209770586250251615)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_194 : Polynomial.coeff recurrence4Scalar1Second 194 = (((1720512782426828484 * 10 ^ 70 + 2036756300248512896118508991241999757669865025927749696797889639558214) * 10 ^ 70 + 354207396058004831327882713249776723907076789420325662229959709574797) * 10 ^ 70 + 9191748987483240333464553111222393964680669006531817928744473712479126) * 10 ^ 70 + 859573839631000830539038159553198042436923876440445255382540670054559

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_195 : Polynomial.coeff recurrence4Scalar1Second 195 = -((((3796701073098758401 * 10 ^ 70 + 5530489665608467793486913082848897077381713258725648771207347492766336) * 10 ^ 70 + 8570463160287785523097915566270443459284888299406635573596118197911227) * 10 ^ 70 + 2778201227281572801375757947653013314073961236030965894726098791831134) * 10 ^ 70 + 9384257340322516492004872472037043768488741690507646820758740073769510)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_196 : Polynomial.coeff recurrence4Scalar1Second 196 = (((8258467866741681784 * 10 ^ 70 + 5498300858414679169848258501422969102144773335905950472003036149469154) * 10 ^ 70 + 3373889866695213112800154739339516556562625388457036208074591664185250) * 10 ^ 70 + 6776703323225252491959838255867121984613768781959711279525048529110736) * 10 ^ 70 + 2107629024858118765431970716046412860475385107367209025632534589713010

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_197 : Polynomial.coeff recurrence4Scalar1Second 197 = -((((17706878648860989564 * 10 ^ 70 + 5026718431596830531292803008817457185564316104036607285416703633419753) * 10 ^ 70 + 3837779775547620748848616243179800602887960579459735758671568974932820) * 10 ^ 70 + 5906377309494960484605151801839665094616879040846167207992269484320337) * 10 ^ 70 + 8419965459545553781889105604040020778886482889260456005358247014466361)