Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0MainPart0.Coefficients191To221

Recurrence 5 lookup certificate: Scalar0Main coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_191 :
Polynomial.coeff recurrence5Scalar0Main 191 = ((((2781691961 * 10 ^ 70 + 8476318666373975889911501561310926444937336724686726483242285568777224) * 10 ^ 70 + 6170676200072209776555981618260977545383482064923057751381230987058868) * 10 ^ 70 + 4265628018916886211071795099341686168476364397782542838158261029352060) * 10 ^ 70 + 3479248851035750472837871565821960440605621627621418231809683956957388) * 10 ^ 70 + 5198897073357225582340857812092330131235093780912684230462666991268009
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_192 :
Polynomial.coeff recurrence5Scalar0Main 192 = -(((((3835997864 * 10 ^ 70 + 2500292694691390518265412756493096329074842811757088852109575955933367) * 10 ^ 70 + 6342059946844157963686553662599207837085859314740712405531236122331948) * 10 ^ 70 + 7875755790761096799668593852833307968488044736422469047955045460057225) * 10 ^ 70 + 9618464913029593962147920743271268277597366474456434480192700014971641) * 10 ^ 70 + 3385021309752150262896661587790154012131676317031982567761917236470428)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_193 :
Polynomial.coeff recurrence5Scalar0Main 193 = ((((5203052425 * 10 ^ 70 + 7468339977807102743772349701678237464406758163821339025949751507421419) * 10 ^ 70 + 9572731257059892284469010551741034148601014137682165782947076318523269) * 10 ^ 70 + 5968778676335996116161786808470508637731328589168947209211281215163084) * 10 ^ 70 + 5137649056633937624492068493310426080969563398964196954436648573267741) * 10 ^ 70 + 820922514650706566362587203643714415925476761519616827376753545724103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_194 :
Polynomial.coeff recurrence5Scalar0Main 194 = -(((((6941694943 * 10 ^ 70 + 5432303003255080682736858801653305088169965958716036244720192447594738) * 10 ^ 70 + 2905479777340016826906349955305548153506437483555726674914425938227708) * 10 ^ 70 + 5218307657617456359236710946009654354120595471649826382471151690906488) * 10 ^ 70 + 7141562669390102276460317577575650667763360897871481464512534137765677) * 10 ^ 70 + 718471813023150540190794988752375902912623893675583002650347675551453)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_195 :
Polynomial.coeff recurrence5Scalar0Main 195 = ((((9109972715 * 10 ^ 70 + 9377280967767063637412835641654395105808259205394657433326554389051111) * 10 ^ 70 + 8377101912881880973385440842158280491806373286113140123365930920020382) * 10 ^ 70 + 9794776155341013851235246695883101399513234335265843555082724047585464) * 10 ^ 70 + 5747797593625070921168587865167891020724460170034068214093654513812473) * 10 ^ 70 + 7688059506908251647694031259002399643653462734216906139806354743429167
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_196 :
Polynomial.coeff recurrence5Scalar0Main 196 = -(((((11760597973 * 10 ^ 70 + 1629869569889769715859142440617397193755353014843987194923671346964611) * 10 ^ 70 + 8876646949975140328254704253229267551247503167477094429281495059617312) * 10 ^ 70 + 5337434694452397263068045449837410787831232576086282681667435580765641) * 10 ^ 70 + 4991677290137865627303989472289896711656108395296392158252265806103432) * 10 ^ 70 + 3938451645444624660276629795641786081391996331971549124758224900263477)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_197 :
Polynomial.coeff recurrence5Scalar0Main 197 = ((((14935468200 * 10 ^ 70 + 182658516762616783791609061359414802959919133947120788442937918781369) * 10 ^ 70 + 5848581092066010904782313874189177111733511338703442188680641193832752) * 10 ^ 70 + 3566117631443562401075157206336410686963296761037410549584162302777524) * 10 ^ 70 + 5651126881114783716499899453817986176584531078765438111096941582686354) * 10 ^ 70 + 7517262748706263109154501166037179767132076558875648613782942439534607
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_198 :
Polynomial.coeff recurrence5Scalar0Main 198 = -(((((18659564028 * 10 ^ 70 + 1779975941769657416753955689529234047228205617988542615869612001090043) * 10 ^ 70 + 7765508018205373791292432982489391505599925614016996213943628608839250) * 10 ^ 70 + 3698705037296129497106301813285096703936131015850249651503772121487590) * 10 ^ 70 + 5695696810868387196451754654556630762305919496943782196868142524110131) * 10 ^ 70 + 1818641211382356824265936927213044722488103316471536753066897212265685)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_199 :
Polynomial.coeff recurrence5Scalar0Main 199 = ((((22934707688 * 10 ^ 70 + 5349196073109731510667989756361660632399500571528203498344808142238759) * 10 ^ 70 + 6797628494985458888307701992165990210990845892453895760917052612491325) * 10 ^ 70 + 9455507592992760499580722298831417551274127898608382314071494558025439) * 10 ^ 70 + 485235572986968643679178488276947696709348714438905484722360032830998) * 10 ^ 70 + 6309456587934561933277971999252466637167791700437760112940936913214577
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_200 :
Polynomial.coeff recurrence5Scalar0Main 200 = -(((((27733811527 * 10 ^ 70 + 5018790559010070670062984359833082688908915625641808260597678850329821) * 10 ^ 70 + 983858636439097687129728581505869314620535275032263109239471360331231) * 10 ^ 70 + 5487775346580469647463767194262517729977069536197560582841487209050243) * 10 ^ 70 + 4177233092892616073430581083072811289419590710427472819638185162659968) * 10 ^ 70 + 9413594395223804315495963319493570658331978670831538602753704512700446)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_201 :
Polynomial.coeff recurrence5Scalar0Main 201 = ((((32996341141 * 10 ^ 70 + 2339543527427671384174524840915363193018997067018082089799566359800557) * 10 ^ 70 + 4206730578340095199483330796849159387653109283346385552519803233288490) * 10 ^ 70 + 7796746299629967401477737611554840194062824488842619604558838732954248) * 10 ^ 70 + 337781746757087677764966161074503269342458546036052458493204460105121) * 10 ^ 70 + 6556159327503088788694429809767296806035397172567734573560167498969717
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_202 :
Polynomial.coeff recurrence5Scalar0Main 202 = -(((((38625733799 * 10 ^ 70 + 8599372590483812506670487190637036847602778940522406080061187631121506) * 10 ^ 70 + 9733024985456762805318867706498186136797432872595301530443923642154151) * 10 ^ 70 + 5816104242129127878782483038382591293035326380566779961534177894190516) * 10 ^ 70 + 1744218991956416321586441876993247884377232296361047043259456163927558) * 10 ^ 70 + 9349777682371140861198686382375707769484694183024908360724787226215326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_203 :
Polynomial.coeff recurrence5Scalar0Main 203 = ((((44489429905 * 10 ^ 70 + 4661359166256716011374628224679980928371476349564878918868538431541417) * 10 ^ 70 + 7623877783565746137260864731759442694921499450283227561625965413937992) * 10 ^ 70 + 8620733813422633002281841676019852167860196828615407203616227739280122) * 10 ^ 70 + 9430125522867448507743005970015926660126531950999213042586455914713476) * 10 ^ 70 + 6814618284990831549947269880898009334984416586444406189222664314082326
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_204 :
Polynomial.coeff recurrence5Scalar0Main 204 = -(((((50421985911 * 10 ^ 70 + 7572810599417175791840339228577855971719627714857713527551705297526701) * 10 ^ 70 + 6965397200456302823512832765067268721835703092060446121361706837959834) * 10 ^ 70 + 8258322835978910006776567121156506831029533382306469379056329119233610) * 10 ^ 70 + 6159956815446854372283177715395207061742877073290405124572692935972680) * 10 ^ 70 + 846031033367232845622296605827478540123346616428357308406026747846386)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_205 :
Polynomial.coeff recurrence5Scalar0Main 205 = ((((56231450787 * 10 ^ 70 + 1735292859671313619604316859386540331194182695114248302944785843723401) * 10 ^ 70 + 1448911758567682762687728404223699470174757262535615069812290641196539) * 10 ^ 70 + 9375441178006603869273933676121132542199108350694983723770909564841162) * 10 ^ 70 + 8799188395719172012159153790453933218026012115983463960322352652069382) * 10 ^ 70 + 8336283265147137622058533439363539968005511089685270903134147859376874
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_206 :
Polynomial.coeff recurrence5Scalar0Main 206 = -(((((61708832053 * 10 ^ 70 + 7869171621819384597618546644400455924110648297565665206361845673886070) * 10 ^ 70 + 1061589876209430229544794447108064762291191843651317485873234059339604) * 10 ^ 70 + 1338583822364021210749230922816962836780147173240966304542137781592789) * 10 ^ 70 + 7557730798358580307719848943791246495739006142574567928932152699138449) * 10 ^ 70 + 4603176660597239618741209946980545122689766775809630820135899687337239)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_207 :
Polynomial.coeff recurrence5Scalar0Main 207 = ((((66640094851 * 10 ^ 70 + 4317390173859526577016798903028724278463164483421938166421164237021942) * 10 ^ 70 + 6238616969505851665264225366616683004747892549841583671321273395669136) * 10 ^ 70 + 6481796867104640345332571473753772978328643661258511848638245889972277) * 10 ^ 70 + 268497241884009227827692874245653869892528705984989041469752432587040) * 10 ^ 70 + 7226078285848133810071119462321908172140634528348408121238242630133026
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_208 :
Polynomial.coeff recurrence5Scalar0Main 208 = -(((((70819781771 * 10 ^ 70 + 4999814306525591224694905249429449710838509791815814292380798628175526) * 10 ^ 70 + 6395103377430846677544570174744528131398937725172185177229648110820953) * 10 ^ 70 + 9370984269995871860666894073761177511663222579312647178633433517580627) * 10 ^ 70 + 9122513132744042599318653873683048120445639409528953321208410379287696) * 10 ^ 70 + 5199054851073369307512281237417490784516041943087393318892905203352347)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_209 :
Polynomial.coeff recurrence5Scalar0Main 209 = ((((74065067670 * 10 ^ 70 + 6878023021084255362704059207117144545730671567569699510904607811013974) * 10 ^ 70 + 686795175913282406377451482463638476701991504996072328112550507640916) * 10 ^ 70 + 3891420074698151240834079501882267952869224214209330935156006052290468) * 10 ^ 70 + 8031313419113190314453619834551774948912752004287187084193495626765388) * 10 ^ 70 + 2042261910334551650722964022397988485174330212987999790205896636728169
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_210 :
Polynomial.coeff recurrence5Scalar0Main 210 = -(((((76228919808 * 10 ^ 70 + 7906569514193379872022043450289347185505419984027964944479267239581878) * 10 ^ 70 + 9165486435479827594701172638192122704866481532267987640561592156588502) * 10 ^ 70 + 8965147150497122480262583221674163715639726935662012007146443736755251) * 10 ^ 70 + 1474591675918449857301072819349565044831054470114974840994916153410320) * 10 ^ 70 + 8524766249755612254966128744575184747500216901785086343677294283182868)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_211 :
Polynomial.coeff recurrence5Scalar0Main 211 = ((((77211050059 * 10 ^ 70 + 1320354060135732266999534079555366350324614686877133973849700373770434) * 10 ^ 70 + 4914009571384168512412242693819234931879241884332353398883226987971824) * 10 ^ 70 + 1545719478339306060892493019716983163607147413545135916875474575792624) * 10 ^ 70 + 9627499990141348219213297122467358318343551142217240587599538224167475) * 10 ^ 70 + 6301046596309525584701184219964081951334218173751373090174728137272670
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_212 :
Polynomial.coeff recurrence5Scalar0Main 212 = -(((((76965529747 * 10 ^ 70 + 1049384401742903682059225742961076403913406116805610821201651764447223) * 10 ^ 70 + 3205058022879275735102912554797151412125118664817850785769124052059037) * 10 ^ 70 + 6546747481946962589554499844683837594634334383266291441653397094134617) * 10 ^ 70 + 9201194101383739170300501598479239505852407216514578387599560820977446) * 10 ^ 70 + 8503236965247033827880817000895666072393340240978289569537371481024244)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_213 :
Polynomial.coeff recurrence5Scalar0Main 213 = ((((75504270014 * 10 ^ 70 + 1319488950564791784808537312247557738494916257824167577447865098084894) * 10 ^ 70 + 3726521962816198263971075425232007823175151287192873102890723546742359) * 10 ^ 70 + 933970698380669344100881729047116362846534678726391950526746419162911) * 10 ^ 70 + 2142302214024016519048342765775313044685259595013873677110572277491155) * 10 ^ 70 + 5723409238802633455183465745571862000545299607203338710544947988959023
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_214 :
Polynomial.coeff recurrence5Scalar0Main 214 = -(((((72896008857 * 10 ^ 70 + 102292880488131881226550056566304247297310055190470463173044317416561) * 10 ^ 70 + 5140426499324477767799785288143168791788937358000210593679612386842763) * 10 ^ 70 + 1920327412243112511254769863955124496979784422773756354738445280399640) * 10 ^ 70 + 6391188776921609014351477024748597926500413617207289408416757580661311) * 10 ^ 70 + 1100281542591381537095005656823207877064302652547926850719739548781244)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_215 :
Polynomial.coeff recurrence5Scalar0Main 215 = ((((69260930499 * 10 ^ 70 + 2698232306945177915857311651579591138833780955000825418324182518895312) * 10 ^ 70 + 9675356256706279517015590071113667596983000970895302385541341321089906) * 10 ^ 70 + 4326559434398271804273010740455870041449442570440115900993000516751201) * 10 ^ 70 + 8293040432427525701374221122832547962319133545735191062075603189289717) * 10 ^ 70 + 2427956581587957747259291860408531911503171348853268232877210214833856
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_216 :
Polynomial.coeff recurrence5Scalar0Main 216 = -(((((64761506762 * 10 ^ 70 + 3768725608156183577610256432198358979090767286733593629873901095012708) * 10 ^ 70 + 386195054186685735479950010259994917871225470463054592210971798137004) * 10 ^ 70 + 4875276691374950566019479902147922939748696270036940614463365714027738) * 10 ^ 70 + 3705485309971988208776756116925027635977139949181632600405214001271339) * 10 ^ 70 + 4997598694379988502122595386312108192083403432604809575118583471169442)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_217 :
Polynomial.coeff recurrence5Scalar0Main 217 = ((((59590530971 * 10 ^ 70 + 2563172895542756633154780149861204056081079323327563346699429287299149) * 10 ^ 70 + 9736473662787785805934112590899434394072565341305884502251148413132878) * 10 ^ 70 + 2290734613603647302254602133482779001374466168450077288242867332545102) * 10 ^ 70 + 4128277040716629907664768126823908061498611235988830952991703572252483) * 10 ^ 70 + 3471608569235133059139187193227700843373112955805673212312088107642447
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_218 :
Polynomial.coeff recurrence5Scalar0Main 218 = -(((((53957564335 * 10 ^ 70 + 2104043479646240767783526203653895283245040561895552119938920752224486) * 10 ^ 70 + 9685441352019577398783224469846776223682022455320472111377313502651236) * 10 ^ 70 + 7483071983296916847643611135078848475526826523962229305048236196516457) * 10 ^ 70 + 9260860532070975126430088276149939811153566040161081609747187363165830) * 10 ^ 70 + 5524883271267583312267546360180603608109193150478132282508431963819475)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_219 :
Polynomial.coeff recurrence5Scalar0Main 219 = ((((48075106025 * 10 ^ 70 + 5462679799130728439007005226515808841026514386150984457843044164680727) * 10 ^ 70 + 9402421347943522039167610734533469267264721991388645294220479523954145) * 10 ^ 70 + 6250990647211263216973704227181320554633745276587468754351302415753317) * 10 ^ 70 + 2467336769352425591128747643815461168060866242168547907533136035475679) * 10 ^ 70 + 8464394607151184690797539742966660692791593399298100967277459942810427
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_220 :
Polynomial.coeff recurrence5Scalar0Main 220 = -(((((42145729431 * 10 ^ 70 + 2819202515049645461421278816299566794505594560484025157572982854511388) * 10 ^ 70 + 551058846723654789433957991928780853933639273436809883580961360837385) * 10 ^ 70 + 7458322333006368453491285503369062359396656240964970022682571346019157) * 10 ^ 70 + 4184869245051246802817421732267368065286459240498578009298557353763324) * 10 ^ 70 + 5856150407665413515689411482789253326402733709710497385120107620951545)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_221 :
Polynomial.coeff recurrence5Scalar0Main 221 = ((((36351219781 * 10 ^ 70 + 3410869271258315287727493336962757635500039015111691085221046463250053) * 10 ^ 70 + 7429753640817540685089391439377752578877904598613147843414037563497935) * 10 ^ 70 + 4943438671048146814582911812429730274290683139602201131064442049517544) * 10 ^ 70 + 6325917985509709282038339522786458895432914056804081117183135039128333) * 10 ^ 70 + 6360735023874071860201486321011258264298148071337396540845527309469357