Recurrence 5 lookup certificate: Scalar1Second coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_251 : Polynomial.coeff recurrence5Scalar1Second 251 = -(((((168167 * 10 ^ 70 + 7753203704125704647118816429363676039343149576077697213883344915481936) * 10 ^ 70 + 1539852545518842695121543799831495608481631836340521302710684675166012) * 10 ^ 70 + 5970021018431746402825555864836934319848281961298219435829822075709147) * 10 ^ 70 + 2152051694784507552233366519696191095057059356663926746127406816146735) * 10 ^ 70 + 5016082391107088139086554684116889209798785834776344352605511329479718)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_252 : Polynomial.coeff recurrence5Scalar1Second 252 = ((((127448 * 10 ^ 70 + 2101747699837810150649622792086179620078961799596432081757626696936846) * 10 ^ 70 + 1242444132460229573843149289270242324928213822284495042700853202532182) * 10 ^ 70 + 7235581065645885158233948118799631792050822913175907037826565365902931) * 10 ^ 70 + 7174947543766738541133610283616627183836662830020140589433782944602846) * 10 ^ 70 + 1050314583192539006149341747504071018912926416487675688924466092581428

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_253 : Polynomial.coeff recurrence5Scalar1Second 253 = -(((((93249 * 10 ^ 70 + 2465333837700435325173111011249234014895504610619275654448149244690769) * 10 ^ 70 + 1158957848424374804425013577812849671962060958058213631454648036936521) * 10 ^ 70 + 2709628398746617186967696750105222357029742049048870224196717533974750) * 10 ^ 70 + 7349688501289124335934673569582702027486014496844250179814489011579986) * 10 ^ 70 + 3353869287162440612380112454352412252872978471703238808425144070463636)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_254 : Polynomial.coeff recurrence5Scalar1Second 254 = ((((65941 * 10 ^ 70 + 452879929095953068662320403245152666176076766504300927970664380993351) * 10 ^ 70 + 5205143399020700551128405788032037558501903675564011752713573498260250) * 10 ^ 70 + 1448288142256186961458062762716014721920546891268891422716775503663808) * 10 ^ 70 + 2147683830874603794465613034138090521384052076336630984524524403336320) * 10 ^ 70 + 8090084546230445555448713059390045707964768056751862007431437354175042

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_255 : Polynomial.coeff recurrence5Scalar1Second 255 = -(((((45070 * 10 ^ 70 + 7520423631996774869891960218071209872079149074802820285115773980936703) * 10 ^ 70 + 1856744910318515633213701088937895292024335045226416922917393406134412) * 10 ^ 70 + 9742739984826683330421537826355371684262694477122056828962274058235148) * 10 ^ 70 + 3295576739712489851904606150651835594091224742576186597782485740650616) * 10 ^ 70 + 4023336374027437960223808022251565841582924593825672950116251707074055)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_256 : Polynomial.coeff recurrence5Scalar1Second 256 = ((((29750 * 10 ^ 70 + 8295210814976233042524248003873871503581989618475277572579034256133536) * 10 ^ 70 + 6510526570048151562458704864388095453285763502615654874852606624971004) * 10 ^ 70 + 6688352146737806759276725117571201736163883783279813834421032816801759) * 10 ^ 70 + 3583096602217804192831368944802474667421797099325756881072527201483557) * 10 ^ 70 + 6592096445776464836168964216198183920034536593963551283480815148858632

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_257 : Polynomial.coeff recurrence5Scalar1Second 257 = -(((((18931 * 10 ^ 70 + 6262197952279786431803775746597995870190025556471840620085949559893758) * 10 ^ 70 + 71622366514698085684123159649895219246117424483140294766565528234810) * 10 ^ 70 + 5468806257419560149501682516223500929833571198055973123892563854020392) * 10 ^ 70 + 8060846869836199699239162751892934854718291841948279768788990004483423) * 10 ^ 70 + 1160398281672330596990570263358026079814977588890792743660358876243283)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_258 : Polynomial.coeff recurrence5Scalar1Second 258 = ((((11578 * 10 ^ 70 + 6184407113968021230483955051896591551976510584998344681440814166202220) * 10 ^ 70 + 1190203804647758272196864148306206131752967189393097435945598846932062) * 10 ^ 70 + 2232455867994724175252080305785039802799418177720807241870452001503618) * 10 ^ 70 + 5499531241859919303726506187390674416699786497443863003948529137250048) * 10 ^ 70 + 1346139513463420270704355145753169587799639992861932214066294265016133

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_259 : Polynomial.coeff recurrence5Scalar1Second 259 = -(((((6774 * 10 ^ 70 + 1075203246988008933018821556212117031727518708859640018819594585325671) * 10 ^ 70 + 4083051147941404006260003448651440652135119629001831220628554742164941) * 10 ^ 70 + 2717368762533887657060934865802602144423414046188492877644792570779805) * 10 ^ 70 + 337459544703453172794505786187026803280152462964440862752948428025983) * 10 ^ 70 + 8202664678027568567086252557694450398527046487301509911990758095126381)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_260 : Polynomial.coeff recurrence5Scalar1Second 260 = ((((3762 * 10 ^ 70 + 9176921142197125234591334994409221071956472907904693379831291814355684) * 10 ^ 70 + 1958786902637795513752094572114468993006759052160792484707435432202907) * 10 ^ 70 + 3032557905132732788524752779764659863785742460763951720582271293089308) * 10 ^ 70 + 4830595984374647792517643381883859460829020973332582714106676661907701) * 10 ^ 70 + 6374105134266098905808291073489710212214386256084296560613153853357821

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_261 : Polynomial.coeff recurrence5Scalar1Second 261 = -(((((1960 * 10 ^ 70 + 1491511209769705145153768185195399697976288211427339913076363409033080) * 10 ^ 70 + 4983774894020754519763129096639236420353115947977839542479110381144836) * 10 ^ 70 + 6115880840821310314446896590589536403740357329095066570573003717256217) * 10 ^ 70 + 8395393471562033617374067979609035552317739333062782228314099753012849) * 10 ^ 70 + 1893342813388460190351971384702956332357578070343140696515128485363772)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_262 : Polynomial.coeff recurrence5Scalar1Second 262 = ((((936 * 10 ^ 70 + 2228911095030412635117882855422197942287044691218017785787681825319505) * 10 ^ 70 + 3794960543416801035779929983336431563936692897394723033041703231909410) * 10 ^ 70 + 6490359319923487419891231002176423527576295411664633934964225218762891) * 10 ^ 70 + 572268129783509027787556422653816559312934289500421498400095136338217) * 10 ^ 70 + 2868451202306656643069793856563816497818285203894003690631555759524987

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_263 : Polynomial.coeff recurrence5Scalar1Second 263 = -(((((390 * 10 ^ 70 + 8963835487216530439063707731100887392469889047636867279150916991625277) * 10 ^ 70 + 2541113497477502511954700763419959269866818306070421196799215528678467) * 10 ^ 70 + 6054072187770801937059488435442872292025180007248992591032895272546952) * 10 ^ 70 + 9689175773154088436493159360370226135404709644396526676412411690026674) * 10 ^ 70 + 7691811763007997709978795915163235431141119293305435803112766364886374)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_264 : Polynomial.coeff recurrence5Scalar1Second 264 = ((((124 * 10 ^ 70 + 3137834179435465635819306168815703549222403193032184471810124198948797) * 10 ^ 70 + 8697225250570747143771788523718508980018227462387055436956362772154511) * 10 ^ 70 + 1235158792870515931140580637893206729227273366786770177387819879420264) * 10 ^ 70 + 3843449777792899126899314108481766769620700918298799084602210463791176) * 10 ^ 70 + 6815814083324220360678548849968672726943327605086347509338433330738060

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_265 : Polynomial.coeff recurrence5Scalar1Second 265 = -(((((9 * 10 ^ 70 + 9882128069152051868500558173103428544970096424551992635502655475716396) * 10 ^ 70 + 6615435581188092806954415113210458625483882086773824646882333038669594) * 10 ^ 70 + 5891054922689108969073353495893159042901683086189379950177536665567009) * 10 ^ 70 + 3740770901196125165279204735434218324799305511867394842614585990437958) * 10 ^ 70 + 5316316218570270050963380736137598067702093230372793805188924818411368)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_266 : Polynomial.coeff recurrence5Scalar1Second 266 = -(((((27 * 10 ^ 70 + 8420853517245567823096933331791337059136386769106828489447100286280010) * 10 ^ 70 + 707901090337071372102368628763072579117478869232886511954442039229500) * 10 ^ 70 + 8900529516151168571963491935863200132177288934355255253493774357965622) * 10 ^ 70 + 6549181677238995632479234668442409704602633663216958136775362786362773) * 10 ^ 70 + 2404841496485842367028793137124661892545481824187261614160141950495532)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_267 : Polynomial.coeff recurrence5Scalar1Second 267 = ((((31 * 10 ^ 70 + 7379548441622396406417329900484254571998190859602678154797477108636995) * 10 ^ 70 + 3634406642334705054475001746301104818515813762024764356309440339714536) * 10 ^ 70 + 5265550341617533741121373839558551676670734561521046215478975329932624) * 10 ^ 70 + 591931501285534474322278517608638941259512479632221061451657007186015) * 10 ^ 70 + 9307555924650681547700059433926323701796434748963852976533116629991762

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_268 : Polynomial.coeff recurrence5Scalar1Second 268 = -(((((23 * 10 ^ 70 + 7433240317734554181541623206096638141856114961295653339296176966904215) * 10 ^ 70 + 2465919575057743819970595590214290939880973098255705531435588724835801) * 10 ^ 70 + 6684115961786910298447059662198660040650814466438003028484031000278730) * 10 ^ 70 + 8664193119681310505169386929102151473513783744327861015986167984249368) * 10 ^ 70 + 4483355542284783772420532088766404645854004465055508284420299017400493)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_269 : Polynomial.coeff recurrence5Scalar1Second 269 = ((((14 * 10 ^ 70 + 169335201935102580790607925778752064028403006886378313740091449344966) * 10 ^ 70 + 6830282203313193707493587988971204374398683957739616511610887856730239) * 10 ^ 70 + 4086905727156078366317908104558717391689940467326392831925876154269622) * 10 ^ 70 + 9871005060860246062732549422547327243390140859122740323790256809939296) * 10 ^ 70 + 7429179788283169035955679734593989032233242500365486610463563370034659

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_270 : Polynomial.coeff recurrence5Scalar1Second 270 = -(((((6 * 10 ^ 70 + 3563734331981422976607406501391692486399129374914753559938334299206581) * 10 ^ 70 + 4678461687452000226518830937813978374951095768316907439054000560635168) * 10 ^ 70 + 552776765887611510382867607023573996278637452579348035269415004825857) * 10 ^ 70 + 4374384511612345296798794355575239434532392402135746120187002608615671) * 10 ^ 70 + 3447458777863346597212426439030465819423278972171862095282225039977533)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_271 : Polynomial.coeff recurrence5Scalar1Second 271 = ((((1 * 10 ^ 70 + 5070023986997796845079968449824336071468131823521108285736676365351739) * 10 ^ 70 + 7690608855495635672247848815877266047272688589275717693816840864218395) * 10 ^ 70 + 5091728679925916178620281270318029689901942935548293502314773338799222) * 10 ^ 70 + 8209884438891966414503547498741460280452588798851847294318768618206175) * 10 ^ 70 + 6174948089617174036433910208554376300520330657885029091511835973114242

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_272 : Polynomial.coeff recurrence5Scalar1Second 272 = ((((1 * 10 ^ 70 + 43029066427330112615620704866310623873033142690865791431558326275871) * 10 ^ 70 + 9578881632124900441483270361438906028202097055691961106997791318882452) * 10 ^ 70 + 7208129997774139338456645944848869389662937693886129393128775411531831) * 10 ^ 70 + 9457327616207971583399883549751291773669892379583211404192270890950393) * 10 ^ 70 + 2096844970812714781196158191214614428770328775597128466456637540114690

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_273 : Polynomial.coeff recurrence5Scalar1Second 273 = -(((((1 * 10 ^ 70 + 9520463730657930762456122546288080490618241245811170566523527305724504) * 10 ^ 70 + 9834781944436622143272465517231307745530930689022281515210543756229418) * 10 ^ 70 + 8751955582809251858449945273451911104287884471745871244633660411577165) * 10 ^ 70 + 4247237334565780081334171565658390484390208332957631969609868513334356) * 10 ^ 70 + 945026132984319859838214754949667308293030851174894472792588076708826)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_274 : Polynomial.coeff recurrence5Scalar1Second 274 = ((((2 * 10 ^ 70 + 220569120837512984592649695201588078365637410174032311772363383820985) * 10 ^ 70 + 5423362354408243290247326801725204850063950836819447077497050417475733) * 10 ^ 70 + 984338249655064870736248120250256039101755097087007308640327949329084) * 10 ^ 70 + 1685644528394290440403862514726713226631430643487332589706553977989775) * 10 ^ 70 + 7809964400194681954603815600167482282037471278476728417532092603336901

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_275 : Polynomial.coeff recurrence5Scalar1Second 275 = -(((((1 * 10 ^ 70 + 6963152370226966366804169653349210650669414392097474088363076722453571) * 10 ^ 70 + 4962556171734433233696305528547701895017392793529429505825336661710311) * 10 ^ 70 + 9225506000163043599589822885001272982188722853253735206637808664878634) * 10 ^ 70 + 4392834282072553548249469956916667127145541000581722004985564145688392) * 10 ^ 70 + 5126396932338229448828889062150150405623029914139444374724271609436024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_276 : Polynomial.coeff recurrence5Scalar1Second 276 = ((((1 * 10 ^ 70 + 2618873042191992062882209943510245550467434698386923758682293203503177) * 10 ^ 70 + 9822933489840009483475380973505250887147715527228837948344744366595327) * 10 ^ 70 + 1815024816643383129762242505257392641832954774068700194331611715702927) * 10 ^ 70 + 64385822768671622490758649441830005204626723060184076551332127639075) * 10 ^ 70 + 6334968242346723067369986813702016331706947165007273104987213167604323

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_277 : Polynomial.coeff recurrence5Scalar1Second 277 = -((((8619190732514507127175396356182875829301721457273326136044114511887189 * 10 ^ 70 + 7530935184328786195806163714773524939442325242575590351256321098765787) * 10 ^ 70 + 6655582173245515607955336715112555158843788821854943668101643829838752) * 10 ^ 70 + 5470639878440767964913187789813537500400698356503150920762000268957216) * 10 ^ 70 + 2290937928403379227620780930483841997742011579013467977269118831657868)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_278 : Polynomial.coeff recurrence5Scalar1Second 278 = (((5495140391643861964627227576021049800833796576176898526489401896543218 * 10 ^ 70 + 6083648196949802315122438035216876593594690276805058766366265968119600) * 10 ^ 70 + 3456380963071807745547500720624223243538119901347697080783817483725968) * 10 ^ 70 + 5248746393137183556659366478680874048835043356463543929718521012726146) * 10 ^ 70 + 1075671979762416106410835859921654787653263331767289944950179191564415

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_279 : Polynomial.coeff recurrence5Scalar1Second 279 = -((((3296716238857651820400102601493249812748109138026173255052259885680887 * 10 ^ 70 + 3080084816354494520996431532938513190445112216133126154831439227608211) * 10 ^ 70 + 9897524800184882877081916546684033628316523955225306811227057521830095) * 10 ^ 70 + 6516841985223613543888879848603836251867331136082105005108734348781305) * 10 ^ 70 + 6270747033404420820781531416770260926818399302278835613898859081591117)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_280 : Polynomial.coeff recurrence5Scalar1Second 280 = (((1867278365094381065033698219477865291632863475820881279113372036413107 * 10 ^ 70 + 9619460590062445251894064750342811537538302136158558108348264719822493) * 10 ^ 70 + 5586337602169755599803468920294229595516963852409378172746604094557722) * 10 ^ 70 + 7733553470495098367622060908580598190130110143653175398045972089995574) * 10 ^ 70 + 7193719873732539303823155196706436678771020857368457231220851637837930

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_281 : Polynomial.coeff recurrence5Scalar1Second 281 = -((((998174391349510477504148680029187386143116053835859446007611324490592 * 10 ^ 70 + 1672177641460687083506498870627015936090524936041435106991978424706880) * 10 ^ 70 + 3739994431722171577939716982917408701097077403598908319653539730691427) * 10 ^ 70 + 7063923964786394871824463301257063396560339384017020130352561050070614) * 10 ^ 70 + 5248304761925546429368073552701142079450834672432539978168522867513901)