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_383 : Polynomial.coeff recurrence4Scalar1Second 383 = ((19847997079458137112362613145985584889284831870503300597215123010 * 10 ^ 70 + 7674578479234647359227502717837451423666787343556397049578065087694363) * 10 ^ 70 + 66288857811920380220155517271526727977995967272436684733761948767450) * 10 ^ 70 + 8094895066372721998862952165983669282442868677005860022739552866690364

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_384 : Polynomial.coeff recurrence4Scalar1Second 384 = -(((3995962610092808463593283990204952855038021438405395167368859483 * 10 ^ 70 + 7390922739538212015480952181197792568819595198292194168803383929988029) * 10 ^ 70 + 1114882740194285190445165249510199711890426846904686205693077381357873) * 10 ^ 70 + 3516870902581926097137132488906103347414156751264850805072102869167366)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_385 : Polynomial.coeff recurrence4Scalar1Second 385 = ((333829206123139461201096003841788257860012104317897148778527324 * 10 ^ 70 + 4995906998932151905625597520827042232992741133964137551151916479417454) * 10 ^ 70 + 6205658039780137013059243942485211984279953958408601571912687321419967) * 10 ^ 70 + 1574765057680446253668418001156349435231972627849495171573266700052539

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_386 : Polynomial.coeff recurrence4Scalar1Second 386 = ((233909018715489684760131896712724524951302363352269704726076340 * 10 ^ 70 + 3357723895335855265765809054314522605308140398305514795488519088921224) * 10 ^ 70 + 8694921010235015486130778740463558355806158385756145521180438143915607) * 10 ^ 70 + 7799882282111894207584360509753623040567635171640498800043409183641304

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_387 : Polynomial.coeff recurrence4Scalar1Second 387 = -(((187028619234973139838185764947160406522932888656823793141069490 * 10 ^ 70 + 1894920622734325440817577383248724122328960122512494606623069088069604) * 10 ^ 70 + 8110942326595524203204536022221749214768680517621716131215159000801724) * 10 ^ 70 + 1546030348857198949893860858532409341758413963347189430337384947700770)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_388 : Polynomial.coeff recurrence4Scalar1Second 388 = ((93722143314824885170182361647393151412561957329110184204954459 * 10 ^ 70 + 3896578782821699714360862867650614343374138661179486415624570762681453) * 10 ^ 70 + 9955863807051857464227221142302665979545761078748434238359967207927325) * 10 ^ 70 + 6039612112764754117343555445145348198998916212703526074145194034739770

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_389 : Polynomial.coeff recurrence4Scalar1Second 389 = -(((39383129011316837984666641895454088528014395544412061247407422 * 10 ^ 70 + 8289223231687153984762684789181987452373575127951537416995387841877570) * 10 ^ 70 + 1146101859547705009206464834271187735354869041088531864081703670732006) * 10 ^ 70 + 250129574363868869735816156393780135138875226757487854811108358129386)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_390 : Polynomial.coeff recurrence4Scalar1Second 390 = ((15013587977511855660358581024317062085188540090699288649716241 * 10 ^ 70 + 4307494244732673222996947139030919472877536572981615951801150899349757) * 10 ^ 70 + 5936557672265096222604309567783559412103054653141493826677807905572102) * 10 ^ 70 + 9242246451194382849410798834335202190361611376409957445909030944343628

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_391 : Polynomial.coeff recurrence4Scalar1Second 391 = -(((5402357480711864504651883900657947338150336275077249556222445 * 10 ^ 70 + 4143267448331046533884237888873514745236460179023021372875232142467328) * 10 ^ 70 + 2403320247667944644369840996346545410144618689427674460736546526991891) * 10 ^ 70 + 8885551955184298435393006267757100780763189270047941119251490231249965)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_392 : Polynomial.coeff recurrence4Scalar1Second 392 = ((1891651637659851438716257804754180410197223798682921418141791 * 10 ^ 70 + 3699422384189865986540860797992799173988750206198087063954828343649045) * 10 ^ 70 + 540060132409750285108353654708663713485509774227294643817627112347496) * 10 ^ 70 + 9465921118728531367968215110589161073188091028587962883541153809585037

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_393 : Polynomial.coeff recurrence4Scalar1Second 393 = -(((663297251957973702932772352739313832132185253339629281040659 * 10 ^ 70 + 4941268602195796118395828622263669659187581995857311690803651283163010) * 10 ^ 70 + 5835503304043313638479974888596127064453944189495646351198956717646921) * 10 ^ 70 + 7203747559576417580761925402824121138329373297856099456638108396436137)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_394 : Polynomial.coeff recurrence4Scalar1Second 394 = ((238659125830610029363095063355251430380752849233066809644793 * 10 ^ 70 + 540712630000596074600562165185758783547131902825850831535799267626423) * 10 ^ 70 + 2613099666223404278755190664703043170279606458098135761685355397755161) * 10 ^ 70 + 8387242388097987309156914696345651254291773375941827060807700394763594

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_395 : Polynomial.coeff recurrence4Scalar1Second 395 = -(((89196962189962138040931118598776936517249145910852128843627 * 10 ^ 70 + 730371469183039669613397774347330631907799684469811475832991419183114) * 10 ^ 70 + 5788660887051930535219372284781421149703437450590619554822224243728329) * 10 ^ 70 + 7143138832982847337156314134752965920568017769812429193854920009816392)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_396 : Polynomial.coeff recurrence4Scalar1Second 396 = ((34457022429602231653663491236279577884947884248939305520199 * 10 ^ 70 + 9056490584289134172522367565173568776645024818846764943431388060231294) * 10 ^ 70 + 7739238966826980687699760060454129360281856692849598895565536484682355) * 10 ^ 70 + 5574340749931068017851957726422154038636358396244415716630149252632555

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_397 : Polynomial.coeff recurrence4Scalar1Second 397 = -(((13517589228619894490584205179254736474411555059863210072850 * 10 ^ 70 + 7568448391532263086646992909079451628481409457073917207406829705116796) * 10 ^ 70 + 1245975236485444337763942359405274578631497054163713618260090393967092) * 10 ^ 70 + 1297347743026727175449021819656025875300425582915790743804802801945593)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_398 : Polynomial.coeff recurrence4Scalar1Second 398 = ((5274990483650750710165039858427450314321190446463257452798 * 10 ^ 70 + 4979038888406270225633787686022367921432137715645594451180072405237903) * 10 ^ 70 + 9336627054749460639366258145961366066252174828809215087931519248231482) * 10 ^ 70 + 7730967900735182553925431682623054760660221888003071566036987680391587

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_399 : Polynomial.coeff recurrence4Scalar1Second 399 = -(((2013199783726136128000695364221340189716973684690305450615 * 10 ^ 70 + 7764240306379745183536920857929661216452079683732113456399844060553622) * 10 ^ 70 + 5248847560026454262595873601960531554869386178584007210940676041794947) * 10 ^ 70 + 6898109459454006841586948325931692868916811682436643829236269858914560)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_400 : Polynomial.coeff recurrence4Scalar1Second 400 = ((742978178941748170886827367088712333875419381218692335940 * 10 ^ 70 + 9024107151929752965627821015965800895180962957097799277757925846935004) * 10 ^ 70 + 7325165022709702302764767064611781423924463998767082630224978689789219) * 10 ^ 70 + 6452384537835865004416457501658561385403806311338970460429177087404617

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_401 : Polynomial.coeff recurrence4Scalar1Second 401 = -(((263398897623226579979896224658357513026430615901688924190 * 10 ^ 70 + 5190837913363070424686539317151805019937167471101760692149274709657560) * 10 ^ 70 + 9660239634447850519499033996877818485436740808084169966004224053240884) * 10 ^ 70 + 1176158835718869397718012370309820905148336699197347580273575770118484)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_402 : Polynomial.coeff recurrence4Scalar1Second 402 = ((89392919438089763252981769749797085538482241558609571685 * 10 ^ 70 + 6916784713915625162760871468693601387915449147009088544200307056270390) * 10 ^ 70 + 448399171233567944076928769892692755616049580381364688180617891214243) * 10 ^ 70 + 6138610837419771181609162787702036626261352416706494271576721861335409

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_403 : Polynomial.coeff recurrence4Scalar1Second 403 = -(((28997119952656436041085930824992259969949754476495090429 * 10 ^ 70 + 7132192206260266026183243056385271373427740878895995133004561918756294) * 10 ^ 70 + 9830465896952407962195103450770626894435655063529350427934006336799734) * 10 ^ 70 + 3212709467167668482246280936875627669900523911565603976719118114642782)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_404 : Polynomial.coeff recurrence4Scalar1Second 404 = ((8983144373445242728139653131654805412887565304147445391 * 10 ^ 70 + 4496809768591379969418478115625986763440640959630021259080816476007334) * 10 ^ 70 + 9137624640028622169623763065847999574118631207536639956019140293426452) * 10 ^ 70 + 5607343174924581573689399221770765285532929551900313586620620747391741

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_405 : Polynomial.coeff recurrence4Scalar1Second 405 = -(((2654787663030337393970448933558078904442875816733174517 * 10 ^ 70 + 5468912202284989367766881914484002181329363826580728678105918531265323) * 10 ^ 70 + 9110966640779328971418580556735350962924259145979678913477179834092921) * 10 ^ 70 + 1025761132369282620712343656285896920389617368655032046167515130470869)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_406 : Polynomial.coeff recurrence4Scalar1Second 406 = ((745914191357733490484398350905975543433457816028463456 * 10 ^ 70 + 5334222777088829554427719957514775412388555740673448026488109950681275) * 10 ^ 70 + 1062058925473400307011627792775949725431901495994351997041661646915054) * 10 ^ 70 + 6098999935893646637640645977286400967533676140972149638706126167902312