Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0MainPart0.Coefficients156To196

Recurrence 2 lookup certificate: Scalar0Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_156 :
Polynomial.coeff recurrence2Scalar0Main 156 = (39197138570117565323848036944882767882671532 * 10 ^ 70 + 7552057296698648401090094975882700382620079493699596907266519533614196) * 10 ^ 70 + 3253215702681637850040692837120788248507672518028837295418159343076337
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_157 :
Polynomial.coeff recurrence2Scalar0Main 157 = -((37805421813751138082677481914555069479577610 * 10 ^ 70 + 3516487852657959092868053533891970900524109797732402628669228623019376) * 10 ^ 70 + 6807689166758577424531534409556657350303616118922438801183867428173853)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_158 :
Polynomial.coeff recurrence2Scalar0Main 158 = -((334191990342574529351672446349447855277155506 * 10 ^ 70 + 8184174720959962652331138240412812586264505513998577966230187738213776) * 10 ^ 70 + 1568509333816093324316273225331906744684322085582248879349509279761219)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_159 :
Polynomial.coeff recurrence2Scalar0Main 159 = (1692414095037027696147777090904205591065652269 * 10 ^ 70 + 8101397403079117835292192667896336909251753880736970634039275825174414) * 10 ^ 70 + 6981356780059748480993332140183928077709776166643877224400505875784958
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_160 :
Polynomial.coeff recurrence2Scalar0Main 160 = -((2338424402035940931145277779767586034559389504 * 10 ^ 70 + 2959591680923880139348625656268426249925877855089690488251044549341572) * 10 ^ 70 + 8322614450188856907358444182860349406253456174629139882421553237298256)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_161 :
Polynomial.coeff recurrence2Scalar0Main 161 = -((10959483461202649376950684197556612719146955358 * 10 ^ 70 + 7477927664823048327270749154028440140182992990240209511774927271201990) * 10 ^ 70 + 4036047762898392222125355301894920354746216632339077413874293362214234)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_162 :
Polynomial.coeff recurrence2Scalar0Main 162 = (67073363271447596063042935402102845643066331753 * 10 ^ 70 + 2720264619180036567038891118678831166551900269330957000869991568668015) * 10 ^ 70 + 7838633717544357694671759044747621746394725924207932101618436534967452
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_163 :
Polynomial.coeff recurrence2Scalar0Main 163 = -((123092222785154814071731459378141257604229197750 * 10 ^ 70 + 7722719056738823125236286413235888547582978717364743637485394580318380) * 10 ^ 70 + 1917951983145523937414642528977708832761881913901938439629347623766549)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_164 :
Polynomial.coeff recurrence2Scalar0Main 164 = -((297347492933049515868767861574850746391211058674 * 10 ^ 70 + 5883641913562796113345500455238223201210306825716112968141274672777428) * 10 ^ 70 + 3454134713742411419629727231984064416392212898378526885584620701657997)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_165 :
Polynomial.coeff recurrence2Scalar0Main 165 = (2474985576145966320892800214919965428367192727845 * 10 ^ 70 + 4510939968143109923071211509443585760862393794214843936174218110396099) * 10 ^ 70 + 2762762163516778023894044673302496059902363515717726516745516622763855
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_166 :
Polynomial.coeff recurrence2Scalar0Main 166 = -((5996848089597615248344340503548537060776847376666 * 10 ^ 70 + 5208850893535485044382690929373928040705764455341144900735878929968546) * 10 ^ 70 + 7138587171087656744598901876269698793566346292301985162284135397382184)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_167 :
Polynomial.coeff recurrence2Scalar0Main 167 = -((4302354516744625145600216012570234490720820426014 * 10 ^ 70 + 6245034189686168346918233092849155860603106233416615067646878008262850) * 10 ^ 70 + 8533314633175097091517412591135453673062919428555740345329697435148874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_168 :
Polynomial.coeff recurrence2Scalar0Main 168 = (80641698921825460412574517508610335063071964953941 * 10 ^ 70 + 98905577641039457594113874471644937404023600279948522172721114746786) * 10 ^ 70 + 3456105073327536201207550481805684099691369911800843281168986982918225
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_169 :
Polynomial.coeff recurrence2Scalar0Main 169 = -((262119636564694449919105053319183461793507790919410 * 10 ^ 70 + 3873567123580988730724764126163730846340612716051090860752651290946076) * 10 ^ 70 + 3692897699335704497907094398942527636224286487829150471212903229749093)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_170 :
Polynomial.coeff recurrence2Scalar0Main 170 = (166327185542396279077546870536183783924359182985734 * 10 ^ 70 + 1743556792873227543954508882989767713153740384122283948743341739606723) * 10 ^ 70 + 4935503841965829814530016810064105726922116484152230532321629264736314
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_171 :
Polynomial.coeff recurrence2Scalar0Main 171 = (2035637842175068793200489428813650978438211093495375 * 10 ^ 70 + 4854734782045805019216959993146134236483089997802286828656966441599483) * 10 ^ 70 + 1540238757596498871114789733833958019802790480745372787351310009960864
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_172 :
Polynomial.coeff recurrence2Scalar0Main 172 = -((9505350815303114524356427404095592218656563921471295 * 10 ^ 70 + 658315292202738638305995783616213915275237205392193168672576308495734) * 10 ^ 70 + 7889826059041103216540485203741563165832689934439430707655399381737638)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_173 :
Polynomial.coeff recurrence2Scalar0Main 173 = (16649361649219824736172836606134145131482112747926864 * 10 ^ 70 + 5776946898815623340141165474235646984604623456295049487375027988877399) * 10 ^ 70 + 1046569311421143975693043038782218211046152762165789188517701289280011
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_174 :
Polynomial.coeff recurrence2Scalar0Main 174 = (27376178452013420151568963686118878994991134843190835 * 10 ^ 70 + 7494584327039127147990916119505629371144508213050515820034002869369878) * 10 ^ 70 + 643933025951533891375487870279715014905408051332051416822602644145602
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_175 :
Polynomial.coeff recurrence2Scalar0Main 175 = -((262960639522632646064182993228324560072139515144528049 * 10 ^ 70 + 6594343979137061376405840523825703568902392780467699532091567291846985) * 10 ^ 70 + 5337252031958063982997952760716004477936121546569934227812496826467449)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_176 :
Polynomial.coeff recurrence2Scalar0Main 176 = (759817087602437887095844298798138273640028418113298930 * 10 ^ 70 + 2862998712143574640572476870538565476061873478652353450956149333635861) * 10 ^ 70 + 8026132656380324103116441526863732791662853463463093560621281078191839
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_177 :
Polynomial.coeff recurrence2Scalar0Main 177 = -((533112987945108319488141230587210041923187710232575675 * 10 ^ 70 + 7235983200647992657989101169583388402232592526730432962829272448013929) * 10 ^ 70 + 6064820538644076400400857769141872191053879860359726395330344995324186)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_178 :
Polynomial.coeff recurrence2Scalar0Main 178 = -((4743712558315898378476974815138076580285080484977591548 * 10 ^ 70 + 5529857080688125337995463847119373451270480233901586467074400580342998) * 10 ^ 70 + 1077699923836994327723986039232547844116388584583880789281091927790559)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_179 :
Polynomial.coeff recurrence2Scalar0Main 179 = (22957629966697309131896505671166623872759920954193202484 * 10 ^ 70 + 49068067076291936536779634923609794931626535315152554698573566043225) * 10 ^ 70 + 2902134818697249909185168202340848083230306389779759115087379592249405
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_180 :
Polynomial.coeff recurrence2Scalar0Main 180 = -((47418429562099132364740337146993945721949998209322085117 * 10 ^ 70 + 380660001645753643977486197615348294785386480667382926095340642563487) * 10 ^ 70 + 8475489564979586281643353991145723033851533866119811245044238551846475)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_181 :
Polynomial.coeff recurrence2Scalar0Main 181 = -((12530532955639367192851096163283833930215969203608890713 * 10 ^ 70 + 2906754836117778558039774408678000810621962734651508350780691854705000) * 10 ^ 70 + 448378560572029496812785319549106602932020204652952544222429895387827)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_182 :
Polynomial.coeff recurrence2Scalar0Main 182 = (445274086917182776301435001771415815938782119142796620408 * 10 ^ 70 + 9979808463727908959128157674870307256623117303850326604673293420747139) * 10 ^ 70 + 5967621258867479049045866239647105770980203934069208431851437747907517
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_183 :
Polynomial.coeff recurrence2Scalar0Main 183 = -((1616430093132563654934547069932333170194316750066542104867 * 10 ^ 70 + 2825613165480009655038045535531503859937310214625025710030441769003283) * 10 ^ 70 + 6627798945795720422234857243300388793113364709799321765759268567418651)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_184 :
Polynomial.coeff recurrence2Scalar0Main 184 = (2641193233714419178067940111667302341148905990352091552396 * 10 ^ 70 + 5747815016711727812988460423759953652738057299943259305450973132637579) * 10 ^ 70 + 3152124554896352290552973763427823489947567701137042858732949713748414
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_185 :
Polynomial.coeff recurrence2Scalar0Main 185 = (2663859017451319997522953938453363818914473544430614108876 * 10 ^ 70 + 8792829567019254598403684741317566589425185135233750753174380697495685) * 10 ^ 70 + 2128063679149984456723586188501930735224914494616572013832386666261505
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_186 :
Polynomial.coeff recurrence2Scalar0Main 186 = -((31041132306282617925750941813994889269848742173492734586202 * 10 ^ 70 + 6853828326381268050078968952276494123459326517364936606277746133822051) * 10 ^ 70 + 1257935217868528113535611515230396557959182309944944888732174026584115)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_187 :
Polynomial.coeff recurrence2Scalar0Main 187 = (99917177950028534143660442325423378536441738793802589652516 * 10 ^ 70 + 9621077905624137899620137026066913927147826550293067555980625273091365) * 10 ^ 70 + 3401711865105219668394078075633191295635908010656710037556953323921092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_188 :
Polynomial.coeff recurrence2Scalar0Main 188 = -((152794160252542267032571646025116035549135145926004393055175 * 10 ^ 70 + 7594253722389174734420994146908140464695112592075353464004109933501532) * 10 ^ 70 + 9392429736690147763280640897516524222732393640699142173637926326685696)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_189 :
Polynomial.coeff recurrence2Scalar0Main 189 = -((150448495943284316295839387464264791369112993534740301155754 * 10 ^ 70 + 7985741001702792382601802101766365310986423979646727692649767022569783) * 10 ^ 70 + 9714297736305842450905921230270533127581786786594460124397731428316190)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_190 :
Polynomial.coeff recurrence2Scalar0Main 190 = (1703743167712887811501546758086080559353795282957180788159182 * 10 ^ 70 + 160233911715642624583379919836749633375235594958314304651484263722169) * 10 ^ 70 + 3609376075695987589822731430214429259019912660984752492789451109498718
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_191 :
Polynomial.coeff recurrence2Scalar0Main 191 = -((5548085880316504179897276305730069119956546768853737738241036 * 10 ^ 70 + 977395126384376693387948176721297819273617211535954464003759291418536) * 10 ^ 70 + 1522246390353240727346891250663017967418528750468372295217308439221748)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_192 :
Polynomial.coeff recurrence2Scalar0Main 192 = (9560459870034323285242604932275561095830414893657628456656102 * 10 ^ 70 + 4761581246193050360533354652082524013332169164730996610361063051032235) * 10 ^ 70 + 974509136883626576879000518737012247530674044666189809978607740660313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_193 :
Polynomial.coeff recurrence2Scalar0Main 193 = (1278709975547349164516181566116822000310088627049690011115619 * 10 ^ 70 + 762179600855055802394580215542101448117842861431592030808561842736533) * 10 ^ 70 + 6509183558074379361618555303088775464926836965687265586028771395897000
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_194 :
Polynomial.coeff recurrence2Scalar0Main 194 = -((70163603456582543928929191167213511672628098400537786134253402 * 10 ^ 70 + 9828169056818477860378417864751272070268117065426375886585681758772237) * 10 ^ 70 + 1674301120775667733103162986255562568567428311380013821978597816506231)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_195 :
Polynomial.coeff recurrence2Scalar0Main 195 = (264795419559115171876443780699862189338149976486147313284495972 * 10 ^ 70 + 4178241022389147289154233627710254134906931459149350838592441239535607) * 10 ^ 70 + 6521470963498048547472404899123177776844374658041124810535199131161659
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_196 :
Polynomial.coeff recurrence2Scalar0Main 196 = -((570358541660891143736765378833160056791470122646103939413633491 * 10 ^ 70 + 1646209704806772239920199443885877143099250514155195381648686019391266) * 10 ^ 70 + 1709067140744600760609333099166620456438606110200683764282982759774679)