Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0LeftPart1.Coefficients253To281

Recurrence 5 lookup certificate: Scalar0Left 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.recurrence5Scalar0Left_coeff_253 :
Polynomial.coeff recurrence5Scalar0Left 253 = ((((370139 * 10 ^ 70 + 1652471856852693798443044894641595221215140481539720962435727780292616) * 10 ^ 70 + 7854589237333883406134482460084177311352580266639290981327306303120528) * 10 ^ 70 + 4090464975253056513722237092241509510128610052589471858333072539381833) * 10 ^ 70 + 2630052601685324786176339150696744835521491455446834704230703906107950) * 10 ^ 70 + 2642518951803222346505775935654533882283829905194210191676597598891907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_254 :
Polynomial.coeff recurrence5Scalar0Left 254 = -(((((262164 * 10 ^ 70 + 5663379398730640561745697809108594245349249170128857214117478317836871) * 10 ^ 70 + 9966485416324373618699742881527608877839216162457127194608313150532831) * 10 ^ 70 + 5497730311486022784272837643472193413125842096162147229816615089783774) * 10 ^ 70 + 9017426932021646485895625124429702578993246862530208014147897128138507) * 10 ^ 70 + 146801589226070866117236073844318600474630308379279418220754626030098)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_255 :
Polynomial.coeff recurrence5Scalar0Left 255 = ((((179290 * 10 ^ 70 + 6285234186319212331644183599113287009874694891091777800004350471475587) * 10 ^ 70 + 6986463356548760936412541148335617119424745201945953317231317172943565) * 10 ^ 70 + 7163436585532951019791238583327611010705605309525701208761905660522820) * 10 ^ 70 + 1159830562383222487362840540052283208978519728828189122503566285678529) * 10 ^ 70 + 9123141222397493867961292750716218954581595196641644398238211512006862
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_256 :
Polynomial.coeff recurrence5Scalar0Left 256 = -(((((118227 * 10 ^ 70 + 9293887218114822403782199290070432546057099632676418803259740840634104) * 10 ^ 70 + 422249002733123886803596259266087870915723757577272303200762272541661) * 10 ^ 70 + 2567012412343000906984301266863796773577522024737709533383897939073243) * 10 ^ 70 + 3097819611118484804381553740473030964019330061100216894869890414361292) * 10 ^ 70 + 3767950078011048332816297344023578352807408453443972841990740029465125)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_257 :
Polynomial.coeff recurrence5Scalar0Left 257 = ((((75055 * 10 ^ 70 + 4670251455684450705201734089853549759292994996224799138542699388142396) * 10 ^ 70 + 9168937962233987211914529861728330820664712228868080334413304347833789) * 10 ^ 70 + 601726166804794596095012676532440456183886888221272448932695651234143) * 10 ^ 70 + 1700585648601807060624759874547156840957951203236264076561606025190417) * 10 ^ 70 + 7883809803464001561183844705564336187601240541229979634835939341531916
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_258 :
Polynomial.coeff recurrence5Scalar0Left 258 = -(((((45773 * 10 ^ 70 + 5097607399588154437074548326237502216871151622520278697267646842430821) * 10 ^ 70 + 2477958480016035970037482502092255145334824685388186109510525583523402) * 10 ^ 70 + 7389614375973316014318032405686306324335262387990079474633594534160237) * 10 ^ 70 + 2896236881897079640644412221376530749115756334585750858182678917372643) * 10 ^ 70 + 1969806645254036241936200476298171361546089694566346403872632649689290)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_259 :
Polynomial.coeff recurrence5Scalar0Left 259 = ((((26735 * 10 ^ 70 + 2856471317148893747129576739656469273298420124504984895302627832211497) * 10 ^ 70 + 485301161966138345825428568212816559957589331424287679280318969489262) * 10 ^ 70 + 6662239392100577817227928297284286268780694191987372333121669052671866) * 10 ^ 70 + 4497073950777837156008653951781578620236076217084545119060238514055653) * 10 ^ 70 + 6681682165233486761291289666986849228906226606003186827140182825184560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_260 :
Polynomial.coeff recurrence5Scalar0Left 260 = -(((((14889 * 10 ^ 70 + 8873615235625595271295347711492663021383335219792109509775532306632102) * 10 ^ 70 + 4232777172169011621518711448097639830401431320258460495540907148969112) * 10 ^ 70 + 3565057791365112023381150776108338438855777663996195860544182687384323) * 10 ^ 70 + 6682755685871316708318454216568775295661467203016883356162581643590727) * 10 ^ 70 + 8883790687029973502699496023651966855135826075798429177987337718012243)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_261 :
Polynomial.coeff recurrence5Scalar0Left 261 = ((((7858 * 10 ^ 70 + 4638282048411422251864727433867045905124939932700599584435705718895217) * 10 ^ 70 + 2883800964824103792746789716673676150722001724176568435428898998442346) * 10 ^ 70 + 9033947259048068557180512197347411525401564477538217934599627318298825) * 10 ^ 70 + 976631623168895182407194698246251864942549243980252436990466418217140) * 10 ^ 70 + 8763380264031984580695153069499770661001312169770714842265752644548361
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_262 :
Polynomial.coeff recurrence5Scalar0Left 262 = -(((((3896 * 10 ^ 70 + 3339380885774535414514763968484930623850080363314153648112720677442664) * 10 ^ 70 + 2253626987704346338959949528178478082898161817962984661255570917900831) * 10 ^ 70 + 2547917289784654072033116266762430723754667677746951527809946070321213) * 10 ^ 70 + 798204268608670101937854015055232896837084445715740045145520854393535) * 10 ^ 70 + 5322784636840540615449070805839398628007450788517978646401309643022677)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_263 :
Polynomial.coeff recurrence5Scalar0Left 263 = ((((1793 * 10 ^ 70 + 8858746911195616368650491140219125494083609969768899881814482329610151) * 10 ^ 70 + 3467833938204563726209227352021903079802815529567748281921321927189046) * 10 ^ 70 + 8438883492110764224442362882217006010651800270980444883998965323710629) * 10 ^ 70 + 8897012482916242261609288036555123702730686347650378401162080133450645) * 10 ^ 70 + 4100323907815145108075186865298864322956029603620347938716291107674017
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_264 :
Polynomial.coeff recurrence5Scalar0Left 264 = -(((((756 * 10 ^ 70 + 8668629510095466036488199192114545684961015214722465806734098334197471) * 10 ^ 70 + 3249079058163512397845527861940289346867391786348113672476052265610565) * 10 ^ 70 + 5147290505681449477834693694375988614644963778214561243768061536917013) * 10 ^ 70 + 9778597939790484355909069727341071708784436725001922258734058114274489) * 10 ^ 70 + 1524130361449037389829206914606271633204979600542870594225335060483315)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_265 :
Polynomial.coeff recurrence5Scalar0Left 265 = ((((291 * 10 ^ 70 + 8615501478875420293850483209510668795141566545834059591450628239149009) * 10 ^ 70 + 5778164390042333641080204643861942992847103099498068343252168050796314) * 10 ^ 70 + 1147235001132968600059209918023065151778493049390841649929335405473413) * 10 ^ 70 + 2347384519576978347027361039597466019812430566848708197465210064570191) * 10 ^ 70 + 2543921784311852044430914969698075919348971895573270517855858476227861
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_266 :
Polynomial.coeff recurrence5Scalar0Left 266 = -(((((110 * 10 ^ 70 + 1014837619526433938294870616740683259383985635769899880495450490638472) * 10 ^ 70 + 6144806152381810807392711128387313129764857229643200127593533988412217) * 10 ^ 70 + 36795727289643997305432178191244653929093858574242978527851820047058) * 10 ^ 70 + 1372244419883581962840467131760620715701703712117935841902599394571076) * 10 ^ 70 + 7410185112257153918098228197987442591052200229530825443929814473628269)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_267 :
Polynomial.coeff recurrence5Scalar0Left 267 = ((((53 * 10 ^ 70 + 7953031545927640036490473293802326887722744628113290296799693716468269) * 10 ^ 70 + 3318840265305457807212227180260852250764539900483107563902608578546128) * 10 ^ 70 + 216212380467586531427214896075532642615104044721461721393632970379330) * 10 ^ 70 + 1493273413146994380951754885126230434226273167480614469326007579493791) * 10 ^ 70 + 2591435177317267137613936995237400470693803074999984547403834204014676
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_268 :
Polynomial.coeff recurrence5Scalar0Left 268 = -(((((43 * 10 ^ 70 + 8142060538813355395526930114579534842789098745231829296866850818073036) * 10 ^ 70 + 6667373405992428670028522107446147174106235887078220323217777292562104) * 10 ^ 70 + 1754769749487079841652792724862871099322307216593712688267079337734807) * 10 ^ 70 + 4015629981084706362991341475424837983446687855073953994440616183940144) * 10 ^ 70 + 8470392996950497902916136021366247450168977592079418999307791379036409)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_269 :
Polynomial.coeff recurrence5Scalar0Left 269 = ((((45 * 10 ^ 70 + 98485731183975186899638457934898332430337963498070894031549652324745) * 10 ^ 70 + 613856217836531182366063879236225163262488619894411631085153537716615) * 10 ^ 70 + 8516735630095703006342171186474561649744022318154445353308378370255124) * 10 ^ 70 + 413211451189453805345310345115559171611723076129476557959560483990648) * 10 ^ 70 + 1455137443484428577220100721278704570749161371408208629829542799586950
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_270 :
Polynomial.coeff recurrence5Scalar0Left 270 = -(((((44 * 10 ^ 70 + 7412638611866857863932512296621457825416814615127870668983634291717345) * 10 ^ 70 + 8419329621357011014374957770182657471971898742994267539498123515210087) * 10 ^ 70 + 5510866673919404602015354087376859354220556108955178958727835015267012) * 10 ^ 70 + 3341366306235124145836989963158246972999856510092434293774685519912562) * 10 ^ 70 + 5074435669206124145755261772881631490015436854649196928178567343471834)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_271 :
Polynomial.coeff recurrence5Scalar0Left 271 = ((((40 * 10 ^ 70 + 5326890015108088907752806271938125748063956452357006235940996306710847) * 10 ^ 70 + 9680647878918209602468025027876702271991157970572367606875046029308894) * 10 ^ 70 + 8424991257345854466857446772672074270720977371269942527764564566200255) * 10 ^ 70 + 6099781156815163302311555621194471205265696719689791797657914577699279) * 10 ^ 70 + 7266627251356905065342543532816496850027368814361359007617612156630766
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_272 :
Polynomial.coeff recurrence5Scalar0Left 272 = -(((((33 * 10 ^ 70 + 5876267088634082811868529333776791142872715956619483340434510827761025) * 10 ^ 70 + 3530505580612168487965872812031139149334434624734850763871297638279196) * 10 ^ 70 + 4008651933371019623090284316058379965164737600787193850570245543167363) * 10 ^ 70 + 2974022486880836677811743821675903366881166045313376103799506963570635) * 10 ^ 70 + 3267825261392876206770534722268385888994715223028874450308125173815458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_273 :
Polynomial.coeff recurrence5Scalar0Left 273 = ((((25 * 10 ^ 70 + 7781545546553326232671046542938512942239458418233322111344365121413299) * 10 ^ 70 + 4853816452938490239728357685526954343778303135728650467881587060321118) * 10 ^ 70 + 3650103113398830245348613514466319252940782976228080541567514977599228) * 10 ^ 70 + 5180259629736942595909187307232602258469916614788583953509632487113604) * 10 ^ 70 + 3223129231286026254881590035761410592673937069492622880048715940016145
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_274 :
Polynomial.coeff recurrence5Scalar0Left 274 = -(((((18 * 10 ^ 70 + 5187772700063623124788544222053977180165653721783832421106166538929304) * 10 ^ 70 + 1398618688802516111766687330231195925969645797082743947824331092191865) * 10 ^ 70 + 1788383556842833211044041846344245438346380277658485929196991935055744) * 10 ^ 70 + 8615111474298734667454460524954777921260965295628009368485037548406354) * 10 ^ 70 + 3111569874340988606263796846958641947451417856501827502949219674469909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_275 :
Polynomial.coeff recurrence5Scalar0Left 275 = ((((12 * 10 ^ 70 + 5461385827676474967838382165226098135342447674805512870171854403037716) * 10 ^ 70 + 6320103667037007573288582384506262981125412267439708827564769029091725) * 10 ^ 70 + 5230901172627886204166581602685057025165453702677226337470585869396221) * 10 ^ 70 + 7752530484647723120829014435469249644981095135389519502232953501848723) * 10 ^ 70 + 7019516706065921531088402350116604503428632964121373259531730688026396
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_276 :
Polynomial.coeff recurrence5Scalar0Left 276 = -(((((8 * 10 ^ 70 + 548088975671711888922370558972268638368664193227756963033557957715281) * 10 ^ 70 + 8976802281487308550960808528749327310633722730546815346844410567353576) * 10 ^ 70 + 1890904535775879410282143688064461624138568042933762617853067209173441) * 10 ^ 70 + 7978812361875099421606190942661951415928701039279663033245840730588207) * 10 ^ 70 + 7496753411332417284930909475910516606128232282407936383074655817026193)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_277 :
Polynomial.coeff recurrence5Scalar0Left 277 = ((((4 * 10 ^ 70 + 9141830828064446533461634572789792748173758069059966641414460228269617) * 10 ^ 70 + 2312757105021259655159063721102742326063616259312623530408125375895896) * 10 ^ 70 + 6026053331669160554013753661309255795166500315683261273076644603112384) * 10 ^ 70 + 2834340215115392307835071210435009166826738028793186637112291331250957) * 10 ^ 70 + 1363002970356348372047990698457430900592523288496651608394867063510861
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_278 :
Polynomial.coeff recurrence5Scalar0Left 278 = -(((((2 * 10 ^ 70 + 8519870910224581485004311307882688405827771017803928195652903795339388) * 10 ^ 70 + 1294893389581933584071904684005489307207874952339717850950673709811354) * 10 ^ 70 + 1332282391335544450963503725625159480027777232038068140337684306630608) * 10 ^ 70 + 1448506016088218220337265593952411412043510204020547752933749024079508) * 10 ^ 70 + 2415533223549245470559281178702195034019636375836838967489183263471217)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_279 :
Polynomial.coeff recurrence5Scalar0Left 279 = ((((1 * 10 ^ 70 + 5736365264936419093146544828962276128676604254837350950145040250825887) * 10 ^ 70 + 6876945576069656505774709547289439509384179811840323111699786542083798) * 10 ^ 70 + 7552615293556951645416926341699386998363917332613874651536439496693941) * 10 ^ 70 + 6707397156967328248873848808142769939846239353476545285746321391207052) * 10 ^ 70 + 6938235943261258262261149812420486633865130600307077357803563989747628
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_280 :
Polynomial.coeff recurrence5Scalar0Left 280 = -((((8237187250203090421175627178674061963589779432811377864511839634296216 * 10 ^ 70 + 836865102283404828740631428196471918154879347507050141758064052961767) * 10 ^ 70 + 1840561059194014110168983592649010186605911081024336253408860060202673) * 10 ^ 70 + 560996473467546057527469807299068562116542675827127344840478161873155) * 10 ^ 70 + 3748583664746711511582346929890876704828571372508750776432236065818454)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_281 :
Polynomial.coeff recurrence5Scalar0Left 281 = (((4074093517570532202312926565328734947281105883755687017385371120170278 * 10 ^ 70 + 9806758945233282861227048429957098338409140229806981563673055158632745) * 10 ^ 70 + 2499420985075338305503469793113432513062925433975388607235356607515483) * 10 ^ 70 + 7290295649086439342699878806849239273132430797790814027255688802339826) * 10 ^ 70 + 6974648927069040497620601934956993419455842008156422340068514453945207