Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_53 : Polynomial.coeff recurrence4Scalar2First 53 = -((1177939857635656934866474054765 * 10 ^ 70 + 1414657380198663634455256818053292384663427512946951235659908186404935) * 10 ^ 70 + 7843554119056088354346834304621719256404954081682997410319834224117601)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_54 : Polynomial.coeff recurrence4Scalar2First 54 = (68397774465674959877576645378900 * 10 ^ 70 + 2465098043747384116642334264764083246009355649425212270419741856819263) * 10 ^ 70 + 6550991011452562572677794243794115093510075896303674689598553771793065

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_55 : Polynomial.coeff recurrence4Scalar2First 55 = -((3726309046477413028410729533047701 * 10 ^ 70 + 2694422052273393463229454345988381293783250805011273159629182886526703) * 10 ^ 70 + 3829671735572336438004791473575998021256356428005045657895518084850932)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_56 : Polynomial.coeff recurrence4Scalar2First 56 = (190996950256374678704372733927969749 * 10 ^ 70 + 7263921998428729561170342944334031578157109395499495755352501763983441) * 10 ^ 70 + 2261321034703510362834152798845378771825515911315316749818651638200585

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_57 : Polynomial.coeff recurrence4Scalar2First 57 = -((9230993608755835650674336658040949375 * 10 ^ 70 + 1713916578545881502529162287911908032531658242734572844410229158353938) * 10 ^ 70 + 3444461823321299176354519517509599297680286254048745355324972289054909)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_58 : Polynomial.coeff recurrence4Scalar2First 58 = (421439089723292953597642159852761720382 * 10 ^ 70 + 6489223824172041904483359824884731049375821536563496583672066974027661) * 10 ^ 70 + 4901435098131351261239035152753494018509628864241777398853158843045071

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_59 : Polynomial.coeff recurrence4Scalar2First 59 = -((18202733858100599637431053158560692080509 * 10 ^ 70 + 150517672514375633274610038373077201329668059149661424774527655596253) * 10 ^ 70 + 6071413179465262246176193794645610318704668478497124837960813897989070)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_60 : Polynomial.coeff recurrence4Scalar2First 60 = (744712150087788399952458167204864528759463 * 10 ^ 70 + 3449771417287204963442455904949553180591219490026119126224079684497472) * 10 ^ 70 + 6405549365455737670241208482896632301748685487418931323891011827981402

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_61 : Polynomial.coeff recurrence4Scalar2First 61 = -((28888278974305752875770806428212773801827630 * 10 ^ 70 + 1473731837011187534389631194709181316150052731650965782223800318302971) * 10 ^ 70 + 1344878954403683041714344469125458617412542021734509260080529168142068)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_62 : Polynomial.coeff recurrence4Scalar2First 62 = (1063337051891257868116392246800276365600821276 * 10 ^ 70 + 9738604974485768964444636245886435683795072152874817899852707499927204) * 10 ^ 70 + 7682745001876329876934343412591277476260181678476209849235482258856480

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_63 : Polynomial.coeff recurrence4Scalar2First 63 = -((37159900058414243115683402258817848503739700667 * 10 ^ 70 + 1748280759911816855563298554616239160800123346296066668785121790607583) * 10 ^ 70 + 7705590042129868915673744038318478818910597971203840579897059145388591)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_64 : Polynomial.coeff recurrence4Scalar2First 64 = (1233299561814208629985835918077475091784555876092 * 10 ^ 70 + 9502933992782982675374362567787022395055478337754408678686924719764097) * 10 ^ 70 + 8730389143898297312998118519669335748022679235515510020329914728165631

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_65 : Polynomial.coeff recurrence4Scalar2First 65 = -((38875331571707598739104492646816845768231983632084 * 10 ^ 70 + 5850759771969309879401854482466226428334783598250379128866738822575159) * 10 ^ 70 + 411673443243375035772132805659259865781369735251411746550354627012894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_66 : Polynomial.coeff recurrence4Scalar2First 66 = (1163521701454956177351801806732299331163733049787933 * 10 ^ 70 + 3082195699248696007283902672502326955605423264220926803523061689995347) * 10 ^ 70 + 1668600485697298852233720371904477153993196548209249794837352911184263

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_67 : Polynomial.coeff recurrence4Scalar2First 67 = -((33042944778058708146155761787525516863081200795457833 * 10 ^ 70 + 8970398308784610428892954197464106866480141954275778366036854097757432) * 10 ^ 70 + 6412735881917907975230793202667409546951978901929480855837704641867736)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_68 : Polynomial.coeff recurrence4Scalar2First 68 = (889329294568563889236792537009958464164201537136531226 * 10 ^ 70 + 9545109920066391379190186956916211710969392822964133634395373692574234) * 10 ^ 70 + 4117281984010521222186392408295202241420795553619791870153332114557465

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_69 : Polynomial.coeff recurrence4Scalar2First 69 = -((22639758785593991448026292981625583845938433221983090581 * 10 ^ 70 + 8763821847683839968433606631738984663457186106283136313795499500893615) * 10 ^ 70 + 4014508886915818306418649696140266862916998321768470862136710824122991)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_70 : Polynomial.coeff recurrence4Scalar2First 70 = (543446948095094110205603721599711801828994263409928063539 * 10 ^ 70 + 4786933512742306851110524328609169296681535172561799039402853764351061) * 10 ^ 70 + 7613917212891633798814350042115554351090896597426247125405220200889884

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_71 : Polynomial.coeff recurrence4Scalar2First 71 = -((12239852688464006012804400376312207781079524840430017839900 * 10 ^ 70 + 2411412086908766789272020451125088417393710033471153782310968086356252) * 10 ^ 70 + 7789231248113783547614541648205935432023359684341282053275816673796644)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_72 : Polynomial.coeff recurrence4Scalar2First 72 = (256571441114951213068949222989713422664675858678164036899041 * 10 ^ 70 + 9998609530791965056051681765407401555060601670615773420031205629793605) * 10 ^ 70 + 5258728782036683908101305004496136928522188038030105531368733597845305

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_73 : Polynomial.coeff recurrence4Scalar2First 73 = -((4934853305384518853569652585757152724189970171146272780152222 * 10 ^ 70 + 1576127121255145376082949637873600446086426286826138671034891835795953) * 10 ^ 70 + 9290888588024949544106749845171361699606504027120703948261656339589606)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_74 : Polynomial.coeff recurrence4Scalar2First 74 = (84692222225171974084582088356542527563790887216565690938220853 * 10 ^ 70 + 9883020362525945381637669889000610677225996937111748900922825676560854) * 10 ^ 70 + 8507767454921109522833378642430224345305721656956497872899540939338934

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_75 : Polynomial.coeff recurrence4Scalar2First 75 = -((1213085990140362813340959637725861265420696114179814124039290645 * 10 ^ 70 + 6290977866412024675057029778796480749750962126091900791615092802659277) * 10 ^ 70 + 976675159620385682608441959315375822376571808853131475622856385320123)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_76 : Polynomial.coeff recurrence4Scalar2First 76 = (11341585506321966061087592217647844171388546103657452341777386014 * 10 ^ 70 + 6691005237488392830363371117182726091239814551441821205839402680106108) * 10 ^ 70 + 8508020373128430178831287943356556203168724472990349271112635096138896

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_77 : Polynomial.coeff recurrence4Scalar2First 77 = (70627686042813309296036128577478657702206047440083686902394498206 * 10 ^ 70 + 7586224520704712018529947770324281365013464900737464782898942883738142) * 10 ^ 70 + 7806801212672024725480330989047762261832808739041699880011404546684257

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_78 : Polynomial.coeff recurrence4Scalar2First 78 = -((7426965143966340271903605090385440064179773412163345804309319237199 * 10 ^ 70 + 1625629930037819598770890898476694161358242403495208844097835175890550) * 10 ^ 70 + 7206831287190769839771857745969139542382435438929445791450644700752214)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_79 : Polynomial.coeff recurrence4Scalar2First 79 = (254901613128399835313944612615168227357735641083678194506889531822399 * 10 ^ 70 + 6470776876151910510385079206178142467781903665374863137977541302102822) * 10 ^ 70 + 579381939060602958406833424433257486392955423632961487886435858434231

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_80 : Polynomial.coeff recurrence4Scalar2First 80 = -((6682032314807883436664827986298510924153638934731100837162745262958419 * 10 ^ 70 + 329046568340264936337623437565512794492751699938828232096478727463901) * 10 ^ 70 + 3150508068030863884041157534835786416539106293352712455635623061476706)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_81 : Polynomial.coeff recurrence4Scalar2First 81 = ((15 * 10 ^ 70 + 954763950007491031680715168792879708525236546679143000479731159112256) * 10 ^ 70 + 6756973046992019728628151746757781024192581332548325840747285649954786) * 10 ^ 70 + 7170559979736733333372512816995048041851207337663905219330839179880490

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_82 : Polynomial.coeff recurrence4Scalar2First 82 = -(((305 * 10 ^ 70 + 5579088689530356838864305616395977607777075826302993741295629666503400) * 10 ^ 70 + 7645875598616257678766893188492872686263439705973924622252733817876656) * 10 ^ 70 + 5461609595002573986012758905948499744050478460499286769581258989376956)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_83 : Polynomial.coeff recurrence4Scalar2First 83 = ((5616 * 10 ^ 70 + 4890548677659051507383925808185022343761638136895564574721988994767921) * 10 ^ 70 + 8387409873103077606547871487479562354440998269201014225180850836002089) * 10 ^ 70 + 2367535900222690799945267768723606970757003436473624858444084955497236

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_84 : Polynomial.coeff recurrence4Scalar2First 84 = -(((93691 * 10 ^ 70 + 139033089046993438814706021554573088928768475962380066812109484393032) * 10 ^ 70 + 2126214459435113116747101260857092244481969801325878368062427432590658) * 10 ^ 70 + 6545496666015221409895451370790470263045266909738378822764805445860805)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_85 : Polynomial.coeff recurrence4Scalar2First 85 = ((1396657 * 10 ^ 70 + 8908670127185420100726168026091576207244494644219714422235345777407242) * 10 ^ 70 + 4636649058094290830409738518843165043419450783391306875398573968400279) * 10 ^ 70 + 9780309824110470195347232311907425023669132884185336320452401789437470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_86 : Polynomial.coeff recurrence4Scalar2First 86 = -(((17782627 * 10 ^ 70 + 3382094662238924851480899405407165550283143324452478197730367683935470) * 10 ^ 70 + 3946442094362617326575896847010686849511711696310618212843534588015632) * 10 ^ 70 + 64317820769830138954666989972172015864715761731131399356988373476091)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_87 : Polynomial.coeff recurrence4Scalar2First 87 = ((166261003 * 10 ^ 70 + 3152771871936109046424736698903726149823117108298110447868465558848743) * 10 ^ 70 + 8891771506717936137739347476563152697486250038315584976024291673757060) * 10 ^ 70 + 9630767096820872611327817010873301542367082210160293121946818964199064

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_88 : Polynomial.coeff recurrence4Scalar2First 88 = -(((177984509 * 10 ^ 70 + 7316654714756783718923603943114240587347391012190317016424356352358965) * 10 ^ 70 + 9257349474857118596473836267893852700120287452238539232816853811239849) * 10 ^ 70 + 6328275619327931647013094435297395409322003961751629077249320464253096)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_89 : Polynomial.coeff recurrence4Scalar2First 89 = -(((42696901957 * 10 ^ 70 + 92561282586221850921808904056147629194992945004711943744862050165947) * 10 ^ 70 + 9807328656052640706214888674074531878984246032933279062246671613331748) * 10 ^ 70 + 3487082185622755002727776206404709221070293193225270534340124603196615)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_90 : Polynomial.coeff recurrence4Scalar2First 90 = ((1432883111751 * 10 ^ 70 + 7046499338513372139304312293312885106111474338699435428539203233121119) * 10 ^ 70 + 540793940155033981920596808785691026245708194286560459010921885744253) * 10 ^ 70 + 2936747631137457207365583088603080272953801208831038889587103726702865

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_91 : Polynomial.coeff recurrence4Scalar2First 91 = -(((34058263442227 * 10 ^ 70 + 2442319297421609201541791197855565198918072831192715199816688091968064) * 10 ^ 70 + 8925227247002350920956471176328875462366956845564729350109178150884702) * 10 ^ 70 + 8943854081572142770446548091457756540982241027198122316773374617133551)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_92 : Polynomial.coeff recurrence4Scalar2First 92 = ((692364215552344 * 10 ^ 70 + 4663439447120087172224153412346580008090331644897209408463187111130442) * 10 ^ 70 + 3480942685451550023157167726789252169666216595228219037580376867957656) * 10 ^ 70 + 1535361938428254010866393597427828027912677790748372573882736172794340

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_93 : Polynomial.coeff recurrence4Scalar2First 93 = -(((12752108709087567 * 10 ^ 70 + 29924144488550675263861940792389275024936593441107503306106513607870) * 10 ^ 70 + 9338989753505540146672497575637146216986153594012147928212209985870610) * 10 ^ 70 + 2554784607767811324895061678158025584860233152040809093076554604802707)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_94 : Polynomial.coeff recurrence4Scalar2First 94 = ((218337659877707388 * 10 ^ 70 + 2594379115995791963221084809791325332245709010152008593499451492149032) * 10 ^ 70 + 8628516169299768162361047805319740803088912117324795573066984429653680) * 10 ^ 70 + 2689071888863733293990509636688869737091475568149037153257175567776022

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_95 : Polynomial.coeff recurrence4Scalar2First 95 = -(((3523793462810947163 * 10 ^ 70 + 8515440373184650373154414294205662557867215125093142736635227141207696) * 10 ^ 70 + 1195186931590605532709628491476472345712562337257173258388200778609493) * 10 ^ 70 + 4066387653235773906876370235173226290010757170472122539176378150892955)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_96 : Polynomial.coeff recurrence4Scalar2First 96 = ((54064294951039715430 * 10 ^ 70 + 3858470490135770202746758026055153690669954443600433692493359697848531) * 10 ^ 70 + 89552157605084062577520552493786030613084257134016863794670266316742) * 10 ^ 70 + 7679874030129888630490127864926916073369932196310540180240003434941124