Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_0 : Polynomial.coeff recurrence4Scalar2Second 0 = -58110081283624854118480555109909753495552

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_1 : Polynomial.coeff recurrence4Scalar2Second 1 = 322812217990679240913213129991663909694439424

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_2 : Polynomial.coeff recurrence4Scalar2Second 2 = 1744299746800717689180199903581668219332980366336

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_3 : Polynomial.coeff recurrence4Scalar2Second 3 = -17374360191690494783445856547786413522640011498574784

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_4 : Polynomial.coeff recurrence4Scalar2Second 4 = 52178580157867919626240581380201344059181692940181277376

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_5 : Polynomial.coeff recurrence4Scalar2Second 5 = -83738689134426836974607595293969777354170836455258915672464

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_6 : Polynomial.coeff recurrence4Scalar2Second 6 = 85531441245667780327896067645199331323499574423433253766275728

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_7 : Polynomial.coeff recurrence4Scalar2Second 7 = -59785513990014649150910081830506369331041577651477707239010887400

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_8 : Polynomial.coeff recurrence4Scalar2Second 8 = 29786620574334966548729391704706900025665120792010880085483191126696

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_9 : Polynomial.coeff recurrence4Scalar2Second 9 = -(1 * 10 ^ 70 + 1465926794302609485530099327306422737142384212072487807961333056860304)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_10 : Polynomial.coeff recurrence4Scalar2Second 10 = 296 * 10 ^ 70 + 1967065066289048725336183827425650594159195288841752045305853669757440

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_11 : Polynomial.coeff recurrence4Scalar2Second 11 = 66945 * 10 ^ 70 + 6548869620735684225315886562132320473802880635246440248050723942954300

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_12 : Polynomial.coeff recurrence4Scalar2Second 12 = -(163132437 * 10 ^ 70 + 5438278684743379203425310164165932166331253774898497709909354014431500)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_13 : Polynomial.coeff recurrence4Scalar2Second 13 = 118106557165 * 10 ^ 70 + 7982074781740472446167304536169282886932261025395541313821423461099004

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_14 : Polynomial.coeff recurrence4Scalar2Second 14 = -(40653694539513 * 10 ^ 70 + 6296581964710344524403304010902157123424754399583001634157088903292742)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_15 : Polynomial.coeff recurrence4Scalar2Second 15 = -(5634178564552503 * 10 ^ 70 + 2923035861169164925730792325070333104931567458207803741984234811733140)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_16 : Polynomial.coeff recurrence4Scalar2Second 16 = 14742902646052147040 * 10 ^ 70 + 6536839008583880667653322464879683733824403902198321092678583886466582

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_17 : Polynomial.coeff recurrence4Scalar2Second 17 = -(8178315865343037741791 * 10 ^ 70 + 3574890898037461409037289083634047427752099869898076570337398261221032)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_18 : Polynomial.coeff recurrence4Scalar2Second 18 = 2041308000088218431082991 * 10 ^ 70 + 7753396697125284729755221958077130842405232683975953617673811151697799

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_19 : Polynomial.coeff recurrence4Scalar2Second 19 = 209473467970624586763096292 * 10 ^ 70 + 7017011419269597886539713730071876371812550116433780882712567571826999

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_20 : Polynomial.coeff recurrence4Scalar2Second 20 = -(416697232225868745498349043206 * 10 ^ 70 + 6116625386197567957227861641632450676759675445615300421124755903965313)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_21 : Polynomial.coeff recurrence4Scalar2Second 21 = 200707038879728289929038555945540 * 10 ^ 70 + 3864326200207873915745006584286152230169761696371878712885057042046009

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_22 : Polynomial.coeff recurrence4Scalar2Second 22 = -(61870918686052040709694697135466964 * 10 ^ 70 + 9954947956573672485446651928425711728201643371425336494750977166150480)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_23 : Polynomial.coeff recurrence4Scalar2Second 23 = 13797184590713267590558558226602008209 * 10 ^ 70 + 111979706931211880478437182686695688658687660954769259895425215228207

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_24 : Polynomial.coeff recurrence4Scalar2Second 24 = -(2246792635775128049086282640905841188106 * 10 ^ 70 + 5276768594252947911638151276233743336050998870241254596102275889562429)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_25 : Polynomial.coeff recurrence4Scalar2Second 25 = 234106577809044693179831977664926362070213 * 10 ^ 70 + 4183705674347292050897814274387026281466847025033546014307562703490138

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_26 : Polynomial.coeff recurrence4Scalar2Second 26 = 2297688587075095261217634267528780839043326 * 10 ^ 70 + 2840770986893161670552802674253267717325608166192366817148677788822636

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_27 : Polynomial.coeff recurrence4Scalar2Second 27 = -(9608849082258186187299392037919233599849554450 * 10 ^ 70 + 1300672514440780053841070758790922464797428008292350499425093821577716)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_28 : Polynomial.coeff recurrence4Scalar2Second 28 = 3623309886217847225531144247618443873083220775800 * 10 ^ 70 + 643656982218829065771627993466420895119159691053894631817752936909054

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_29 : Polynomial.coeff recurrence4Scalar2Second 29 = -(1049058571894203013780701084546510801432199259939378 * 10 ^ 70 + 1412829735553291118925046817013623744879921663314297915899518546122277)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_30 : Polynomial.coeff recurrence4Scalar2Second 30 = 263293698774647645008102704590785198214285380526337078 * 10 ^ 70 + 9968603347478972272750850931615048772111061523742923971848001187507123

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_31 : Polynomial.coeff recurrence4Scalar2Second 31 = -(57974351029749906451370508840296715056126453675294036883 * 10 ^ 70 + 4559088836902347437928101879764804933118510890174124975511428360679867)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_32 : Polynomial.coeff recurrence4Scalar2Second 32 = 11162782926567630335283935122721697404594872789408113882132 * 10 ^ 70 + 8626380208732933446290264704298985011566742893013308827307629476974284

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_33 : Polynomial.coeff recurrence4Scalar2Second 33 = -(1872677245970218887153055433049304594861778287362935666769128 * 10 ^ 70 + 3221080005454578951487781109248772305372141387575502830186156311104415)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_34 : Polynomial.coeff recurrence4Scalar2Second 34 = 272166003061016492058578045399058143969463215437440890167525140 * 10 ^ 70 + 2573443317594211364934293155242020415108738759940795240211082483785397

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_35 : Polynomial.coeff recurrence4Scalar2Second 35 = -(33800256025267097036184407171182394940520138202051666105747721754 * 10 ^ 70 + 6581367861611269597145326327671384225791445526051580246995084271284530)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_36 : Polynomial.coeff recurrence4Scalar2Second 36 = 3462760483111482112363307098976330443980552635491030825731998742696 * 10 ^ 70 + 6356828983086794649730609242107884099580942379949915930548328522393015

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_37 : Polynomial.coeff recurrence4Scalar2Second 37 = -(263067937310920808008677370361747142505381994142172325081514004637251 * 10 ^ 70 + 3418618862198455715425682533201140324199391632583320533679732293625513)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_38 : Polynomial.coeff recurrence4Scalar2Second 38 = 7786462935484278121468903632654145437110156444072975875113119786561924 * 10 ^ 70 + 3522571943657399792953006703326746490792550181394827402312654048518357

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_39 : Polynomial.coeff recurrence4Scalar2Second 39 = (183 * 10 ^ 70 + 7651028363591259202415061937130307419842467763460198656518341420904833) * 10 ^ 70 + 5859386990009521107766450389904485762637979924406111645767599065390071

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_40 : Polynomial.coeff recurrence4Scalar2Second 40 = -((46283 * 10 ^ 70 + 8470703364903556246910357040702608781614245803879793344064462534350110) * 10 ^ 70 + 42759330092533749088500621124109797772055728394282463296839044126020)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_41 : Polynomial.coeff recurrence4Scalar2Second 41 = (6864620 * 10 ^ 70 + 4531740835167869378158706358102232867116945403792762786178559951674041) * 10 ^ 70 + 9702135795693943851264951991465165938674087346050511594120656527611449

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_42 : Polynomial.coeff recurrence4Scalar2Second 42 = -((795700635 * 10 ^ 70 + 558909949384080654993935017502141925363412599481960376242009795023392) * 10 ^ 70 + 6639523825102475167948826626999319401171432835608650058249946561395927)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_43 : Polynomial.coeff recurrence4Scalar2Second 43 = (76795329633 * 10 ^ 70 + 124454066156492090898153136089000105505630534672742860551234184306959) * 10 ^ 70 + 3077059100859378183716254067467224685378497668706851340506013465482557

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_44 : Polynomial.coeff recurrence4Scalar2Second 44 = -((6230125998010 * 10 ^ 70 + 1564339904572061841284635281651007322904833773712746030949828233120853) * 10 ^ 70 + 7580146608579568281565718690091259796335827877309889903365893937585266)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_45 : Polynomial.coeff recurrence4Scalar2Second 45 = (411275613914392 * 10 ^ 70 + 5679454200146021015846358045365276628955211803124043910987128436138889) * 10 ^ 70 + 5464899533185953641747142994081165186346302195946026940827795986920040

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_46 : Polynomial.coeff recurrence4Scalar2Second 46 = -((19180861380290733 * 10 ^ 70 + 892746095250145326300398859524891507864072441948610727560166987083264) * 10 ^ 70 + 895238969212421067972628364163428475967903377407651927053593884784887)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_47 : Polynomial.coeff recurrence4Scalar2Second 47 = (116069586896972661 * 10 ^ 70 + 378879890064548395606649802913228473638007563496670572082390662518020) * 10 ^ 70 + 7320122415817647773089970276792822332033689940467193210392162333345281

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_48 : Polynomial.coeff recurrence4Scalar2Second 48 = (105629127162875427312 * 10 ^ 70 + 2151004638790522474184567691125002427049294487323368768870028405151539) * 10 ^ 70 + 5732583726959272619903222781707197483521501431473228163376868758186068

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_49 : Polynomial.coeff recurrence4Scalar2Second 49 = -((15934731581219058753990 * 10 ^ 70 + 2975129473626052320890929679310875323419942224846442449161996614249524) * 10 ^ 70 + 996904045568147531676657331769212496659139015613369369484716416195062)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_50 : Polynomial.coeff recurrence4Scalar2Second 50 = (1642756492153570191719066 * 10 ^ 70 + 3482997870646649529902829322304974248493130481962924830810763999663767) * 10 ^ 70 + 648919870281801315090167463877105058742902817205449320779796229015549

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_51 : Polynomial.coeff recurrence4Scalar2Second 51 = -((140488523310061313423472183 * 10 ^ 70 + 8051894764767617325451257022237823088543533588428947213845960221719193) * 10 ^ 70 + 9191849672598385160684476337614085396167931668801622050063516563009315)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_52 : Polynomial.coeff recurrence4Scalar2Second 52 = (10578124192149063684498628665 * 10 ^ 70 + 662247927695406911375397113500248255913918992907616799545991780238298) * 10 ^ 70 + 5798359294758098336807362789370062998867462317284014639582935385829630

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_53 : Polynomial.coeff recurrence4Scalar2Second 53 = -((720404388915757985405594132284 * 10 ^ 70 + 4072883811172550946961804116802876217358624873135053701509206147617537) * 10 ^ 70 + 6736104255829316351269421943937963624522499698710307077157915305913922)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_54 : Polynomial.coeff recurrence4Scalar2Second 54 = (45039472980699910044233668918163 * 10 ^ 70 + 2168355746312590918077559674017304908750870725617179951115446172127843) * 10 ^ 70 + 9809060615324957993125671968167855968033945875600089408454662023579201

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_55 : Polynomial.coeff recurrence4Scalar2Second 55 = -((2609046875676393092198456022790615 * 10 ^ 70 + 2961525743330438916771160581216703759487892012388116445542466588438494) * 10 ^ 70 + 1016859632734986053301132709000549347152792545090542778844195843667685)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_56 : Polynomial.coeff recurrence4Scalar2Second 56 = (140919746159617449607241113015498811 * 10 ^ 70 + 3512276859051199533830188032276275124809274516066056150431088678769208) * 10 ^ 70 + 1967970347125101163824467669104333163414717604470737509878900818264794

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_57 : Polynomial.coeff recurrence4Scalar2Second 57 = -((7129037392768937231479830873703432812 * 10 ^ 70 + 7024438433046305828713110172802655794512865247361048515105128980939868) * 10 ^ 70 + 8322613725826643930271772791547103143173388217136672052341397898406376)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_58 : Polynomial.coeff recurrence4Scalar2Second 58 = (338953750557183489936739635131581282169 * 10 ^ 70 + 4164998340878906921839724603306392112786085642879081122476418059457952) * 10 ^ 70 + 3385376902919782236004854007291052357075511664670254308796593376225796

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_59 : Polynomial.coeff recurrence4Scalar2Second 59 = -((15186248970864459161722463751859127990158 * 10 ^ 70 + 9566349692723231281034285822015477248312814361068282295345695570265456) * 10 ^ 70 + 1243988373456954039792668194060175696422811598233607902276079263947098)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_60 : Polynomial.coeff recurrence4Scalar2Second 60 = (642497456180382636590977347226527838186575 * 10 ^ 70 + 732434821268421985264710792419181172011454865932634970132929114072770) * 10 ^ 70 + 6870227234923393407206872305785284831298217709415681759881966200994976

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_61 : Polynomial.coeff recurrence4Scalar2Second 61 = -((25711646644659568902060571591110822669546436 * 10 ^ 70 + 6408971375935208927611973358542283850231092570796776168570588172924478) * 10 ^ 70 + 3527155024965091851100953730077126807457830798794342316502315747874808)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_62 : Polynomial.coeff recurrence4Scalar2Second 62 = (974549072495923776581635931944647533772085558 * 10 ^ 70 + 578686238519575445763590151103781192213870654507433006943434614351008) * 10 ^ 70 + 8786081545657127381388348331328625373882223798116093633587863997307572

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_63 : Polynomial.coeff recurrence4Scalar2Second 63 = -((35022080206047026405583471441596878487837130547 * 10 ^ 70 + 2239279753731126488637737122797329499888945798297501540638008116226788) * 10 ^ 70 + 354757161630703712152285974869407877134044760147572003170256775428494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_64 : Polynomial.coeff recurrence4Scalar2Second 64 = (1194193673043088320626407355329632972092608633589 * 10 ^ 70 + 7215011523876635806302992984931197374294989602833037999140217033601712) * 10 ^ 70 + 9634570747824321808919117555690257009803665221982258521706127137943919

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_65 : Polynomial.coeff recurrence4Scalar2Second 65 = -((38655789419423240769932163550024160678907624902733 * 10 ^ 70 + 7554150324224186637623238749522746299589773336430189393463531676634623) * 10 ^ 70 + 702991254058991071851388261754255368407000461203018588700498300232747)