Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2SecondPart2.Coefficients399To423

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_399 :

Polynomial.coeff recurrence4Scalar2Second 399 = ((170700718270930801310297655826129814466328054265418198078 * 10 ^ 70 + 8478194116694847764279454116068001758738471405937378009577761809865048) * 10 ^ 70 + 9853918344482398274138348667674733507018442114867038906188508045919486) * 10 ^ 70 + 9408151298233333132081674964966986386119559313366320030928164269411031

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_400 :

Polynomial.coeff recurrence4Scalar2Second 400 = -(((48888765859135761166528292151799161309904492994406055573 * 10 ^ 70 + 6038785012898554123163005161300756983990059252287021111881669174324483) * 10 ^ 70 + 2517255624885915478321348860994224451903204266234284782982677254182203) * 10 ^ 70 + 4287895578256740317186135204767820429826254546125428549410094252431474)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_401 :

Polynomial.coeff recurrence4Scalar2Second 401 = ((13163032862390767396915065099277408140049435396674650847 * 10 ^ 70 + 7871397936426544689660273854471917895351976123942526349001414730385793) * 10 ^ 70 + 1785953569357239970204423176828919771606990227588750062811612889113509) * 10 ^ 70 + 6602426839046426757764890841811797987424233185622630944599275715597489

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_402 :

Polynomial.coeff recurrence4Scalar2Second 402 = -(((3268909180199370309448447736278209201053722401089312978 * 10 ^ 70 + 8153169838007512737265651676564625430651335325088434498102691163769448) * 10 ^ 70 + 8090144957293415209359864804999100730374670863962576427674039755066344) * 10 ^ 70 + 7445435588603163790565440522900314334103264350178103609805015449324147)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_403 :

Polynomial.coeff recurrence4Scalar2Second 403 = ((719055465704182842339535705182634799371746315347711248 * 10 ^ 70 + 5207919243463583672807232658257506817790769997266195778239108185701133) * 10 ^ 70 + 1591448497811589258447906284384754487778302642929735100022727164143486) * 10 ^ 70 + 5136012427345539003491309070743139656272116985740375891692279312625427

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_404 :

Polynomial.coeff recurrence4Scalar2Second 404 = -(((124856346818661645365782757548679405579187998543553925 * 10 ^ 70 + 661234857650624070936995475429463658617702899530775298249960595238977) * 10 ^ 70 + 7445327542376982989565772448264249158981377811696740790941625791310592) * 10 ^ 70 + 221026794162329924099801853854692474262673112446306219641339283958519)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_405 :

Polynomial.coeff recurrence4Scalar2Second 405 = ((8129778258307879150095104720380887702641273600186563 * 10 ^ 70 + 8748793610636847434647677790046755384864112094902948866478879220645987) * 10 ^ 70 + 6112418209960702804307449966603262128686372178498807334167029200411806) * 10 ^ 70 + 9887141778466612161947334146771702714650261970372000434679013945837525

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_406 :

Polynomial.coeff recurrence4Scalar2Second 406 = ((6561259004932580782875698199898909209660093249025644 * 10 ^ 70 + 9129049956221149632294684580149361379795683852269660228211438205980048) * 10 ^ 70 + 1060170465455114145654263313789716025326266812359634903445954560720) * 10 ^ 70 + 9615667114951695441391380380547029364293068831086401536333064844328976

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_407 :

Polynomial.coeff recurrence4Scalar2Second 407 = -(((4666868121591491902847962306381001276908945705581348 * 10 ^ 70 + 1610249783615775625007629753340521390209428477985912520648876200382712) * 10 ^ 70 + 5469481243930969682095790961692849348732251655292599947426692920359315) * 10 ^ 70 + 2375589680749173513592938668987693606836110260920708537473446903141492)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_408 :

Polynomial.coeff recurrence4Scalar2Second 408 = ((2220174126608253740336951233112361622268948740022593 * 10 ^ 70 + 147810760974591543486675247010902611273491117343910995379573419864475) * 10 ^ 70 + 2202169286459303905509919756402074400206537908856839968235970417094729) * 10 ^ 70 + 9514518720686663453867870654367692327075371813163280046905816401422188

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_409 :

Polynomial.coeff recurrence4Scalar2Second 409 = -(((929332780992938557503505302941930032352205747950721 * 10 ^ 70 + 3218345553986088459950372655824070392780542518127017580004712569130827) * 10 ^ 70 + 7715758572055304268735935984547165696507227095919938829212807545862421) * 10 ^ 70 + 1626955555836882612247028411521948889452253268815761450386119718389140)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_410 :

Polynomial.coeff recurrence4Scalar2Second 410 = ((370365876769692548981651463164310968908972005911160 * 10 ^ 70 + 6354928367993281769337725035894489501339760178184578289502870413525852) * 10 ^ 70 + 1551583102736564564470770272745768593282737275379532482485057471320739) * 10 ^ 70 + 9660260368606630487725899724288126640933318328305894029964113764201438

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_411 :

Polynomial.coeff recurrence4Scalar2Second 411 = -(((145311054170239149027891726908556541341005967400859 * 10 ^ 70 + 1352049747843169736594063462968998223450767973859754387316186219269120) * 10 ^ 70 + 8227888447745078768667002411231325115580682986406555767146465984024450) * 10 ^ 70 + 7903361431257199451176023776585341814919346214359534048017036327534836)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_412 :

Polynomial.coeff recurrence4Scalar2Second 412 = ((56856042375206860706679989139621601293906809712379 * 10 ^ 70 + 5229221945985715078284437865851275480159600663267944305680641288383567) * 10 ^ 70 + 6462949264911761812501150918457245807731506655341184524727771979689120) * 10 ^ 70 + 635108648961299329419378452604571209421228062824178194867302043383025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_413 :

Polynomial.coeff recurrence4Scalar2Second 413 = -(((22209618914376793208836019575375385413408346485333 * 10 ^ 70 + 8604487469357408421666765569496330598533933462824479184994171902606272) * 10 ^ 70 + 3211670420571946666424677508356410912302385489328432950198286704406351) * 10 ^ 70 + 3178581785441805062352701161918420525850264740027699833734326622474478)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_414 :

Polynomial.coeff recurrence4Scalar2Second 414 = ((8619446454678887775823500398157473542877776099591 * 10 ^ 70 + 7214438159500174292838751631027394390632152290209088329552750881102970) * 10 ^ 70 + 3705370236662208333124861633473707242684899922062205828363443972623225) * 10 ^ 70 + 5614377569306273109972075165854661620043972755976626757181840793425998

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_415 :

Polynomial.coeff recurrence4Scalar2Second 415 = -(((3301543434640573505675844522084103870286492356780 * 10 ^ 70 + 4459018483980971177245553445600578088846867901798096980222951216825457) * 10 ^ 70 + 2171126197793582741836040592415072699129357962301404242619262954328988) * 10 ^ 70 + 3945340517929156342048318178924694572274541644945140611451889306637177)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_416 :

Polynomial.coeff recurrence4Scalar2Second 416 = ((1240578126805437064424351326208451399821659936620 * 10 ^ 70 + 1033384288931727758022378088801959482340192801383528718542723839525458) * 10 ^ 70 + 3285887515881002474632212206506839585822706265422990129293807371460814) * 10 ^ 70 + 2302035747058403828512732265307481122388779246988220095863199605603987

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_417 :

Polynomial.coeff recurrence4Scalar2Second 417 = -(((455143814675140925933239538377787542705826583104 * 10 ^ 70 + 8038041600995563877495741806231492100711211895143790762017709901714195) * 10 ^ 70 + 3500680904116024683152530782065958019666662265138371271708556334607299) * 10 ^ 70 + 7247721678158179135664040833432621605779080486344695801946952005726632)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_418 :

Polynomial.coeff recurrence4Scalar2Second 418 = ((162471396545109746935142503547380459981379085151 * 10 ^ 70 + 5997715922622047523089994942788519728970039108175948255592851346848776) * 10 ^ 70 + 5992998731476777093629345387349726707986386443367901737647505648096972) * 10 ^ 70 + 6513175945576661735518983940714294892040530201786495330865987490454387

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_419 :

Polynomial.coeff recurrence4Scalar2Second 419 = -(((56280818170036187217858892016567261798756744460 * 10 ^ 70 + 7667744237110549124544061684517563202666830055205075889994495899172431) * 10 ^ 70 + 86859118470066155419956599569651924880140854564246859122383509274762) * 10 ^ 70 + 7239163850951677255242184319132808671362903908744129639766665918871812)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_420 :

Polynomial.coeff recurrence4Scalar2Second 420 = ((18876935497679310724731119770700880931365329124 * 10 ^ 70 + 7887430276439699380322411409322523902814487292565587103201905690583536) * 10 ^ 70 + 1927468541975286650285764530794957295936696940491245469837435400825607) * 10 ^ 70 + 7531473844249246261989811212282803641038586039289795509718502750615546

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_421 :

Polynomial.coeff recurrence4Scalar2Second 421 = -(((6117131589704635086033437765483973653372659745 * 10 ^ 70 + 7068224279228767423738402397312305150871726806891009520519582269154705) * 10 ^ 70 + 9069893750548638619065585865041848449147472965803348358282997032435810) * 10 ^ 70 + 2107539882345846653277762019458547476303840105346750893259981600320161)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_422 :

Polynomial.coeff recurrence4Scalar2Second 422 = ((1910569662052504964423833655250720841004374519 * 10 ^ 70 + 7868690615976452243096116413979395649990804780484308407746332228140361) * 10 ^ 70 + 505629164153602343692896413934505590717586164280859253763791435890994) * 10 ^ 70 + 8346539611397631428645876802738483071004675742627696435149320911110554

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_423 :

Polynomial.coeff recurrence4Scalar2Second 423 = -(((573457853122001555860307905871762517119711474 * 10 ^ 70 + 6750835447901986611150502030724415280367604874097706219799321635888916) * 10 ^ 70 + 3077656171321884072321322209264707146862243016350710548984754187101307) * 10 ^ 70 + 7243896650941138861251903125517178112448782087003131552927392233432221)