def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3pCoeffs : List ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3pCoeffs = 0 :: 0 :: 1 :: 2 / 3 :: 2 / 3 :: 8 / 15 :: 23 / 45 :: 46 / 105 :: 44 / 105 :: 352 / 945 :: 563 / 1575 :: 1126 / 3465 :: have y := 1593269 / 6891885 :: 3186538 / 14549535 :: 15518938 / 72747675 :: 62075752 / 305540235 :: 31730711 / 160044885 :: 63461422 / 334639305 :: have y := have y := 17141894231615609 / 143758249516606725 :: 34283788463231218 / 294362129962575675 :: 371973541444416706 / 3237983429588332425 :: 1487894165777666824 / 13246295848315905375 :: 750488463554668427 / 6770328989139240525 :: 1500976927109336854 / 13835020108241056725 :: have y := have y := have y := [6071 / 4092525, 934 / 636615, 2 / 2115, 184 / 196695, 1 / 2209, 2 / 4465]; 18423734 / 5380579035 :: 515864552 / 152449739325 :: 5661043 / 2084368455 :: 11322086 / 4217210595 :: 7724 / 3728745 :: 679712 / 331858305 :: y; have y := 1005836107061 / 166964748035085 :: 2011672214122 / 338210643455685 :: 3498929752 / 690507642825 :: 55982876032 / 11186223813765 :: 2164231201 / 514742061015 :: 4328462402 / 1042038806445 :: y; 161305480768324 / 16760692014291225 :: 1290443846146592 / 135947835227028825 :: 114145991713067 / 13781013433972785 :: 228291983426134 / 27934486690485375 :: 880273539218 / 124153274179935 :: 66900788980568 / 9559802111854995 :: y; have y := have y := 398932100842554827 / 26856215504232639525 :: 797864201685109654 / 54526255720714752975 :: 551237184598262 / 42832879592077575 :: 37484128552681816 / 2955468691853352675 :: 16702403343384833 / 1499150785722715125 :: 33404806686769666 / 3041134451037507825 :: y; 4791118708237092962 / 207525301623615850875 :: 19164474832948371848 / 843936226602704460225 :: 8518005100455643099 / 428885623355472758475 :: 17036010200911286198 / 871606266819186573675 :: 237364700830403312 / 13835020108241056725 :: 15191340853145811968 / 899276307035668687125 :: y; have y := 14353622417729038099 / 373545542922508531575 :: 28707244835458076198 / 760926105953258119875 :: 3094297743423650356 / 96845140757687397075 :: 24754381947389202848 / 788596146169740233325 :: 10839966517223372899 / 401215583138990645025 :: 21679933034446745798 / 816266186386222346775 :: y; 4445914989628998968 / 41505060324723170175 :: 71134639834063983488 / 677915985303811779525 :: 21732299808790935019 / 345875502706026418125 :: 43464599617581870038 / 705586025520293892975 :: 8560313219688624722 / 179855261407133737425 :: 34241252878754498888 / 733256065736776006425 :: y; 5476065119726 / 40613499251325 :: 21904260478904 / 166966608033225 :: 409741429887649 / 3172365552631275 :: 819482859775298 / 6511697713295775 :: 103505656241356 / 834833040166125 :: 828045249930848 / 6845630929362225 :: y; have y := 340028535787 / 2183521465125 :: 680057071574 / 4512611027925 :: 667903294192 / 4512611027925 :: 21372905414144 / 148916163921525 :: 10823198495797 / 76714387474725 :: 21646396991594 / 157941385977375 :: y; 186088972 / 1003917915 :: 1488711776 / 8365982625 :: 3788707301 / 21751554825 :: 7577414602 / 45176306175 :: 5776016314 / 35137127025 :: 23104065256 / 145568097675 :: y; 3254 / 10395 :: 13016 / 45045 :: 88069 / 315315 :: 176138 / 675675 :: 11384 / 45045 :: 182144 / 765765 :: y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3pCoeffs_eq (z : ℝ) : s3eval s3pCoeffs z = goldbachS3_innerPolynomial 24 48 z

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q0 : List ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q0 = 0 :: 4597017211338631509654747773525638618370723087 / 471627945031194428793241968378424644470214843750000000 :: 12798095940491896447983469424900894061157618464833 / 1313012198966845289760385639965534210205078125000 :: 11364709187255943517775688250718438575009154642044381 / 456928245240462160836614202708005905151367187500000 :: 240213861532226543075844812666059045877624218750054909 / 4969094666990025999098179454449564218521118164062500 :: 1443232984566497305131624958542938683358537319903717319781 / 17292449441125290476861664501484483480453491210937500000 :: 51641912654349196331804364873996780269646339681143323033111 / 376110775344475067871741202907287515699863433837890625000 :: 201500217399963214889532159732463103205499225479992486764620143 / 916205848739141265335561570282152388244867324829101562500000 :: 1731914069888509809689909419187534678240784847997447884208354239 / 4981869302519080630262116038409203611081466078758239746093750 :: have y := 43050597411129097366264501658426201160554377277019867898513685462017569120276293 / 8649717314537120771693418625466164006976299560847110114991664886474609375000 :: 8945834390773891831240779173709696761595611745046008584412862516905626746102057439 / 1157731394407276164826657569870086567087597018144151661545038223266601562500000 :: 14022216634775550869040453344915479283711227683069041068862197783278988885998350689 / 1169101970602347627159776528145596345871493060286638865363784134387969970703125 :: 7209926510145710733978996995328567442616826762093016360244845375158776262017491651557587 / 387318806452675359487525324668523487001842164900722309539560228586196899414062500000 :: 22124004212141732457575135354479846064014842453684233692526380517294372114231754081253289 / 765834912758699006259425073776398712935460644235519112044130451977252960205078125000 :: have y := have y := 21210505485777926612710073773381627744345867621228434214971498882673299829240664532728796344430583812518850085182463386619505498309 / 649689945931701026719558972992926284336407728228077959831645467853412047294415533615907776265885331667959690093994140625000 :: 1317172443467526698143529024196998723209401311222603120530323365056568913695657016008745131828534057427717031602656964826234840610592307 / 26000591636186675089316750099176909899143037283687679952462451623493550132722509655308629206160730973351746797561645507812500000 :: 4445457109305405210840708548077377587127029512144567191763264769679060902244242669710479642936442757136227259158008909776687900524372591 / 56551286808706018319263931465709779030636106092020703896605832281098471538671458500296268523399589867040049284696578979492187500 :: 13664651455125805141124900079971749418517401808887421179313240698053656358458593097716012459353899293007253741884619660710797883243341192267 / 112023749069061337212129597161919863815149308006285935903491799454065218389528261484586885154968172173539642244577407836914062500000 :: 10355631985464560330776586487817441845680700131595521221963491759165586863167723710234181995528068563898088077187260041793889488374555738767373 / 54710871448751342621623929850283998943721442721524510832503074510645624499376654796415626706707069359936213004402816295623779296875000 :: have y := have y := have y := 2528460583395125104139338441343607530970517265488082315434162332331942139836785689054945251853991168843831586426547534438180261042556615656178323972431701275555718984894049711503171849664749620785528091887853878599844 / 230996538167668631164881963648447569426559401032874531576335539743520873689195267052348109154687656581044761543462169099548107345962038018834849943778597337811961907882984945672433241270482540130615234375 :: 1153672294158260431694615085174666127025712421906815081414288323355374218370415560621880562822681009099049791859487548997094107614103244983929237368488177230551356634490253612360121054667147969188185715816527115776472 / 110819234728625675931979620087208322219564744631976054594190823970772274157929499118930329551822436526087572169038354045625424632924218665752326732089945417926847397172007703147755819372832775115966796875 :: 219539469121701589059593176154881042370485553088906570778660107010237797550166287253456830250422336196363304420959755694504657901970725321306146462735321295482404975909089622804875312162272560683310654636822218155368 / 22354503693645351403053093256301377686441232358020115959000213523566536163470509714743365402066547411068847891302790558020784581867294001822727413914057806885028571730611446355396765284240245819091796875 :: 591757767661770466273301760881543251711117018542033155927003867565222370764549466697624367086906039204961757341593110420917784229586645024939169331429626078876222444605033645230236683828391845357721826920020593682464 / 62999055863909626681331444631394791661788927554420326793546056293687511006144163741549484314914815431194025875489682481694938367080555823318595439212344728494171429422632257910663611255586147308349609375 :: 1720050719419600362732936621403821899353941345655570446318240931173780821651537391127094854139364997168668961715394788197214238932487424430140968867589157003886300712143192344180530122285962606641120021498608551044 / 192729103875870740751268904499492734294895208055610529729027519949169172448573041945965790524908585262760995076588441818478999361607336810004046490591209422481473734212187309822184033691883087158203125 :: have y := have y := have y := have y := [8241148074816344208388093713670585151062459977258376868752805253084981197425495513692932973015521163271233638597864844055076901322470516376947344 / 237313359613453634510191491944647345255295108116223934207040607470787357089470869233298367264793958081874837956065932004197774448360245, 1272178317309517023297164171839322944259986348058515264745894745234676577734162411230479478370384999875744495292968407253489606779593280913760 / 52561098474740561353309300541450131839489503458742842570773113504050355944511820428194544244694121391334404862916042525846683155783, 43581942261850097999733858774124490809988381681750648622778711433944306094468169599918391399108743019328652596778633958430459425524829195986768 / 2365249431363325260898918524365255932777027655643427915684790107682266017503031919268754491011235462610048218831221913663100742010235, 1437623401607499921180817609366379313380814847609565338442378371284536830290004967242326570636714889186116512277689383976956064228110930016 / 148729763652350201905232882120685149517514158060958807500772816932796706124821223622508614161556653625734026210854676077664638245, 351140696578892281848192845595844683028309386462198929015811757612984922540181383660614075013050155770854030190876743281829353140656738304 / 60124798072226677365945207665808890230484446875706751968397521738790157795140494655907737639778221678488223361834869052672938865]; 202171150635657429479835914588996403749002206750601741225710260694927194064054222502529485472311131164185294676857508294053770455810953286064963561091168 / 2420348275596431012955890067726320765128218319397502674900567838767224069524444369121294549307106662748927787946208417543872912698975962543975 :: 52234527629291393091077757272091392720186922731399425561147004582591664676847760265010306191049557021646330427495288174102523051252414720043115329701792 / 699569102913254146601868557781361815834401972716221703376576086288200976905736412337384138836273354349357865619003761881451639218640892828325 :: 266477672803909460169940075011396236936965773610638499122783960292413356278229814539381204364849556813081161110833944244553973726123536877015963480128 / 4329782246147461561638443770530090814182859247580505679607455883304515330097396009161528710746165765203806418508422929416588394810332670025 :: 547696071108871630574235474541139434834276162433630512650643601604547940424410026042931071442656997209336446475373788594210390522128361823536771808 / 10219785002708406518422762636971103416639321591456740392464490676564552313369148723433978074145159162558158344237032878245291254469707325 :: 63648865167847176628110280926573228912008853955250864240805455532538858756030796581223444965974512583908102313964154749310622954253082914059873856 / 1525585883229344793279802448215590076641182837890011005616689619455061581289455587928346646702246873383481101146138134312699978596601575 :: y; have y := 701245037949404375829226896010654889371264598864349797404783621341496238481031796437311649299729113405898149348412540172647191969598784349056509502474912797531712 / 4616025101273440846199362608687002457628021139436492256508093550585911179891614894705653173712784249931670596887515692985519622262305028373838085500075 :: 16992563735324384836331222072277434105848131260354849109654668277353810604761860585648287186314521118992630453265489473974533660880223834004539846157303196544 / 126359122424062873893388152765788028185048893800785422148533945158520466997662667178715424535676117542133273025307702854712973153275438076533302825 :: 5206372160988888427871729212816048824394954182681107134061465081280912228236325728153843205975151883042701415057843627040800333395801067784922125027193706576 / 42119707474687624631129384255262676061682964600261807382844648386173488999220889059571808178558705847377757675102567618237657717758479358844434275 :: 70313633879873271588126353901371546570585233456077785187145928486834759382259895838475041354696923607942900500204847070868096368973917003273052950996540448 / 652456742292923617349680651114223897685278281243298221076767358821964545598946646361697544934644324658175247979213611986469740894709663045782975 :: 35512809189622294861708040838041394079319872544132692255509852794210250992824175678211060826198959530911920133755099096374273954559930990849555634216336 / 362562292295821649714040212574388130808680476994767607171340121596709678430787213188210114673534196444171369044573730563252217691749435684725 :: y; 23752796922494971679092316095000404436015060796382440632751975466009754952122263728572839699994496759718524286570431579614455106718428210059244575063079613420768 / 101985622154951761109334894022987513114372375295033339209367114250258011937191008556914996676925209151095182022853629789194153193797152752573427619815 :: 5696889046470358361385976355609377944457275593624779718490117726767784333018670264874681171194067481448376854674644979840009261274496906167189875290420482120441625968 / 26137997087714741806472549324045492723595610436739389539307907078312876137394620774060301413325838778543335295819179632302358716191466076109796338110006165 :: 243005636963064097061582250101443955696688035294871897918947337450871526673246960204920532277190578749259443644876664831690950169886911852821963121459460090144 / 1235912559328691157033425075147279094724240132699110748062327254074290662919995801833721342839422597293055918066581055540859270746798808615235257155 :: 1484755013880115826821234493509117220264204143040744777607036047653342194253031186601659592056601847465457773307312859632319007805105519338083818320063708482041408 / 8103688511124485041105547690806070981169192667010730850314208677695266293587501704038813349406887905435599492313638661019023336860491049811849083433465 :: 13524188451355731986023790403722150055688082517534106159635235368837724669638928389560110200162779567058380553005626628431695606960113682456401538877661746048 / 82480570021860820980958860157008888727383563645787407424427652114462810325946839894677980411199575626403477117618434610658797860489681557649210855 :: y; have y := have y := 9043924425726779177221129877774183087943466000961494795041819996223696743667039588843323910336199593755687396630265600588696757942056150866955837558311917619624946379160500576 / 25939738419454643911264819551981408357875183461905938514198041155030842098426772270892495972583156291970175706850243968352872902652250091562547824650716409988012625 :: 5075549227708773188673664293310359679971144517747474580187824659588979939461303368999305824617543148258036613217909277965424373220036871145273228803494727213986722780224 / 15921865299162821380893949252878931238336594406282103749858901933679611744669040337369659214580800573027312171050829544311009974070289396362003988885302535875 :: 2152325643693650143084253895159840175835052844515351392364780074599168372556585683712861819312746574938794417760985448985792952927713033591950923597395567837018635296 / 7175727526211613668477019884127216199252167033101747867808794627376171932619743706462425424357366861180602755082485508040686655525661974963703301968223625 :: 4133765630754358171770212952760529992844162607912565147263735380657533309114013125836118758270555902585100295208471591850944981192725385872004260106804053414284247232 / 15120479866251492289547910021727380093387079208245112772895443431794503081357113330835383869497436441621379079820350944264966737008821838900288688400097375 :: 40793358513293936623753506822131507848786529234916433065322243424403589040158236106228525212769151857055926543600434859278401268620044945679974259965405862098012310416 / 158947279587454510985306043186763131427270604007198990441737272773524246781453774977393724810765235815466228150251768034271100301164320733100112866885172625 :: y; 653999009085650627396879852551868193246701684740650137702247666534593852487547640664533797189421565482295922476786345241301627185854599578561703113135443651543774807819752192 / 1322869143342476297026808979369340115811816451494094425336042010123524098145932953947954340065216396264554415205223084860567797696234483605185365780413475453934125 :: 78699897853116535637800940054379264625328060467513377817642132627096030366129207720258583802249840288679973531981631255048695507439587155157462118435577272836741772714600064304 / 168663024912994119271135387888621731137070285716443254221009204303386192715931038267701840901901450826692155123443991372285979506274756924463654842982084336673111625 :: 296578835893033277162133507903056383314296877255968868478276527436769383696209511034205558242785466625166002440254730716452064992405277734525289423432865695059694444988408608 / 692931456036535203204518989193463870187141950782620889461736291017084051409774404448928463843684778995718979393212092069821227364694253317001858265930868094917875 :: 159218642502517688850333115083788711047986875065832427787283105657428474129537099771708207470341235024092555322468731950961566563930638778369002000804549909615427518275113712 / 394325170950070594817641011034747119782636628964862251042005913130012801231867655142450368386921741384873788008959425824267069901521316659576074003282536305171375 :: 8668808163527385111763194753068432992389842186781870256092492369280372606804288514982900682227187095086939713599169994294706740024995875639833193993830789909494776054323552 / 23432464696887663876481318475141290296183544229363991431073207908790281931731501599722218584085958710000158723441954804293471456777100353715038685321333703692875 :: y; have y := 3636375786248355348458243083664676616104140952981510698719680487270738732579981304000065097326472078809506732974944956367640143826562022728506366930728366010551157532444263732740976 / 5039280125745455696759128892258662358567158582578748260964468804335711988728044375154742062098831167509742872347234885422886038492575932437740186667650119394251894509425 :: 570191550149203768310126950868659830110863940240466456612126570328147995009383928209645256911043600219058048712456441816352286619846262868070638626431024188206511817295604819424 / 863531180512730170233471564332894675027216299065302152447215765865490144866860862824254651641999971584464992119820909137411213541881978483647715771003047819886655825 :: 3053952817335458217674037950395436391611700722966622182647770903479959920009773476734426724059394681806005048304181348326997868659858206363772982074711047351029178730505612416 / 4903676577924302547608965887908814182721610024305506184875794081361994807647800785456389649611610367523129106226484476209173233652069195391276164112053239148418825 :: 23325183936807236533994581108324961695225983268332559254431294544137572324988669845100337793140738796674132841614394098783656319354687302542281953387834684092900223084692736 / 40852904196245758680442414322028228173195421108365706745135678251038644891412218188126643562877204443619384203069323844216990023135336870606394912221442757575925 :: 68379825007428139761193570354301822169348895669651135157766661692371048659040475216762901614842117239796869092537763919220806835428508867775680741060990625170210407493109598848 / 126898847315490813546854244220963016760271929253323972223425972761595325948176685934747099345240139193416002426210241127719927438054340924120273643767472977115960175 :: y; 1155265605666090219798308298084874043114206310252935086235558389170642958147554733688176011011933318951590483540985908977882730129835511869787394077106759084878899756517490439393472 / 1098734395487737938317770157587808866058619203149098844777914484315620869678324531168254921152368953743809421539123644641353570846496600198916005223175746652848713141375 :: 20424794551664345268841664678581609867691103610533417421460963587494925447398260804519896162400048066354101489176529614439892555311468639557921349351512656473502516793226868278850272 / 20732932545732771602888366117770836202423971511147945194058610948104966256535861553273057933494457078951878247741315047317305783521571887433472287452052057160348814821625 :: 30309278530427719290505836941298046476476050030257639877783310916149873246709561162068833397367147043588685749437208603099999776313148068058188886911844789008418812864294648564720576 / 33918994080056942160326001316501067252196728303667341756531101983549973299424405688000643856219906088155665045578752513605657009680556335172987645115457727315361886332125 :: 13721847754958995446631846767656924925120930180400699483352106026604602908419136474567584837680795542981855783446525486841237423549700630035219417692325848292797734889693917776856848 / 16336127880163839896087285969409949404146283317150887219610091178890494908513990007369768223287419718850265355411365837359905289618790110649817088647876760673673723959125 :: 21079339487024328200314094369120640518341751901832067600968628382023006508400007900319203056949672885720958782202623499458433114174593306006884453748415036557307714689564776648736 / 27517001050666849454454653579861643749001594007528658141415009852579424765533551375071398227696566258698996390683845388184670759879373493471460793598380702917283734125 :: y; have y := have y := have y := 453208350206942926823709002696285567898111923239571887568765041414283260598119980829439056781380318085955352848755219816711155337610957817756297239764343210002231962870094269598711536 / 252941777057939813555238066636804201669572452436004931367515053566880588329737510949931306788632376363212914622444043577271130558963177026688361906915035097356255540823825 :: 57643092152899504060617968192416051462059338574600368847225380517017559680694585625833030989207678195585099426509263144495318164327670671998031031110038558443690929197390878921954016 / 37576716325680637490467739389503063219204776747699180491404675363594233742998698965954318303411018218038282216638028646734292122950183726802927378632610535527425989435025 :: 25987547496311173773904360854090719124186254954073358652949786049819963731248071392912659067552493363374044843393452047461747997588480556796918258033104096099929118374802279708891408 / 18334402159627083492464064693111303474786896119595020268615407777476739363244586981945976438700002758386511301518663093772627927281499669081990891918471710987597318321525 :: 2415957908980419255290613515735520156616702648710914666727195482722379666126508777520333608001286622715132907469533284482280019269577617288944420477479993315390111676318534102496 / 1925569783944358204584657534019241364894587008440829769299365593221250677714361018367229663389843294496370206940241485149264042284882949024682281578734613571926308955 :: 178554014688137533236037552779964582080841337753903797910088712612581123283285168328728272906458161816547733611018518099515681020018425381910424275636566713029270655315590852711444768 / 152676568134071779353161715897890824431183372191102075690301879180009003766598317420228806800345668615633020537871629907001493220275070817910993223092859022728550641758525 :: y; 40364371978782767347586482204020788332622743588792440406714153767488564497839770945590683236726180341153164564772217157400454259674686462382437893136536142391992536747042606722644218848 / 11078360736557647404284295238932322016652939811427528662893855867329921614771463276223919517829960100768493563418734121300718105617520382519151337529298916893108247786136875 :: 111746792062324729315049125222713948678621193141275757999228513779668300842132062313453880002696888181085402435006194485845556423442550375724474562106498477438731268212847080906393230144 / 32759986817461893006431336993100063351388907785449436611325495810408364697092221812927262979625827432486948802546237157920447107644792242264235046845899526173187547546919375 :: 8123040868525333719991030076200322273013160901296748898077852309887860628268442408967293110481558729264963653681989365722246202219600533865895616897399079648190140239642073332758391168 / 2621957445112790750267711666357116724623616885007368191004729213803030488783864442773678180126067315960133871086310207813176353355106103325428141718021705277473380606100625 :: 1929165491229901662331179375823915486979301882156424375261503660333686767397786307121575751359027658422563128862671347414828906061108522263885111148030265181379688899980332039595220306496 / 730690140754693526621707646846101413011413464953720042678694754379977873461230860436160256893393455341991510248096507044051711574859931316589242566606367692471530951807375625 :: 115586423152738715467809869640549884066135981047685251694016756520096123340115494294566598487918890058501552595252387815609652373164093414021306698718044438787698111358758445867233216128 / 58557049607518993422645560548642273516594110431831222932438952441601014249506305888612146022815503389776323120927594641160938558264036307601228498369151417863572166869580625 :: y; have y := 907975549768750244441552015922074188803021930298691877379948906167758545272685867657550655633490497330574967157867870975952805813206313596380942245843768953650826164306830008993274379232 / 212732572624784191294927542752662436699525439163741278248227586718221406197573541645970707703139866745136768806407843822951764129389600256728513658632233631985382429007210625 :: 154207016756684001742805538180026214069463307015518298321718518316449423878120416390400849721501163623146997196501132312062564372915875670820368472180082105512966560937262777633731392 / 36928978100180151412221291075452348234135449084610819591615904419760992799772738630615185635578412900846955930793101518495441596550790187682086503070728243344695501494375 :: 734975115320754132692116034253285411135410808304092725027281215033458266090318779165794219040739657037482252368794003567838924161147923924581548473707434036820832930600166294706738414544 / 180708314380193022712895439542584220422177523590704956791505154309026785909766771935824579661806983579202201459206663032399885658298692691199490097117703837923066794533006875 :: 374093465916194295114208301862124605067957639214689915791917840400437092569922794883203066379744255297867485598567407225406458131722339633666338548953094212817198475078245895601554867424 / 94592157058299912451965905501652903372959716851419667813939846251817023018433263358527312806086582398869445041498422112644593055657289419971215266596321521164231961866245625 :: 276119382260860407796493549225446941118180570672314665408667447966881318567321007355136556604120918900788475404930285400601633031529059864518263057671962259440460937156412762857793456 / 72423257522765161078582648767555660707097434730722274308012956051599539663241708165542873603302555549763410317452538863916616093123299058842951141099633898299848599719375 :: y; 512045904446425969815489308730112359440397245853121198171692088790062931397522697892207310963313199962144813926017459434210557397148562754079170186953829082675421307688337347953415648 / 107751675826553044531549794507826714710559598014001432507043666320672485840432785319466226580523314354526049496697679773144233699524908355839512673343357751129043038606875 :: 91751294442321530021863466239875555666473956638849498652827738655769907262558298811405142142816387941019752799796223116032733812080627797312806273353990093408742191055827338401448229808 / 19748382182559284503289395860705443594903066620370811964289047415675077661114347579355682618740363657891662439137743433623019231752971116664574123421793721418149485183983125 :: 622383220443613375023443593596010788190305376930872133131649794457387073617289902891547774770571261535690805585566035592578295597645842736399967732949014317320089014896505982828898625632 / 136633115750877651319506307946831971538719591007606186842357555697069033248848047073428340719902841242811420615497720829375523302616084717736199829528019975015001722695688125 :: 43539544245861576538476609902263288261829348417202049005319000398725325173744458946162332499241179123162659194769093178958193818261007934591622617707577576819771581860913488037902209504 / 9772750477238583705543288938240162337233481116845645075563081615084022730921676559429164125924432723124135337685338047303657317050850021485686710039899083306946236804556875 :: 1790078607119211249590904281687395870012854622318515302925857818264294551967288642979225355334845679040624155181225619863754699673167360178518717569455803116389707218873376513446014295744 / 409899347252632953958518923840495914616158773022818560527072667091207099746544141220285022159708523728434261846493162488126569907848254153208599488584059925045005168087064375 :: y; have y := have y := 3098688447821255190768676714893359619988314217355780405628990947459148074469796343719515212776831707181150729946126060736185771230061928985675583964070008089186306636647251340144648405438416855080810388406190215432020859279547788 / 583070856782703619568933163431351685670415627633074474229015587656964721474949976330315531572042238058824368252896346784721801286755588782149704146493903488228563860142407405083575522297678617178462445735931396484375 :: 21739978477167135754602000285667651363763853740286356967411546483810830003782764797987109455368235047235303338460853234686079634821667782334311685067040416880886681055946783559917080088359210016402672641046004201779404083083704 / 4182717767451245477538975347427200040677300054756631809390355722072917657639526372527371101664578465271336931512886275356684370780169216514703760017890268925599453803030182245936696716626101988367736339569091796875 :: 8936150505282391068042313600205753260527036226619913435016553576233987572871921131514397373979524497771622668491804107882688352443155520102861467924483148981333168950936376945532022656 / 1762299266387285586245511120010521077206037578447575341494981930588922131805548232028209924347028851710909651058011779021970991599333610431845144433424424858629649259838125 :: 2035009536956701697870959314600252866456879919858581869186331405183279695658288482619288081663560374266563056701959462200106599052312553595132614714512530839818807634361333994611482665216 / 409899347252632953958518923840495914616158773022818560527072667091207099746544141220285022159708523728434261846493162488126569907848254153208599488584059925045005168087064375 :: 14382053488942326324642838491248247677770292231291343905915056397758518854149569728932222287533427852944239898676084728903256504991935621092836183802709529166132497317142016596699882903568 / 2965742336004344313935166331316529264575737004812157820284114003071674898166172315887944572096714612858671423948156410943504005803843250637921043358578786516502096216159348125 :: y; 949253749583984372883334834178133696385750789430947260091942873222663442353634042574372859822479830655412354658643809978258712734396812248717332688444048672774356415841497055398384763604399324469116949972855837477151921575424 / 156506680953788348756043831781942187875673002782529876947107954384239765619674134261845873943428834724019210203343507001607412259566126223220756977925461273078189393950505718666743604217117535881698131561279296875 :: 16552071690468544967330348655891745844575590084106428297016015309457900191904608978073950576441583347348250367873820817912202386729242130813228498658138989847100679457649777672507541166549778241914864944396052753246376877148 / 2811333025282000014164995663927752009333145331403331901815912373931929078368419913281981846400348551428916501885569904080046690411927669693044529059910584541375893836479861465083018856603302992880344390869140625 :: 3306146416971120142688915995171066009484010550451177991124116864649903474538148132350074765649985530574645963688580449232117457260945124263678108403480768408496765775913163821948728772967219893064065788503554617598668584 / 575732992520529978244636832029039938624233471954097377297252985716691738932508338618983567271174609691836749706052137484347029894776416272943753390519613716494650855655390575549290588242001831531524658203125 :: 10497866535529008400561674591628140881613465454274972651668533131859721746945200616521011635671886810690117806660915683529868751577418904748926719114241482213244533885201013384804553916352166153618353560713725853202939945695608 / 1879661047010649966373092080694234963476517174832606299900114724877384659816086319569037819381180651382412534664398281059709224006304283630398788351044176299898658478860114136310688337516694446094334125518798828125 :: 52792382609273921565105716777080854793552368452539000603050682990883536671303835873203507974697773857398888119050189245301322938744418390037028298350319484911642596803638783728137680773865735983723936980134691999723892817312 / 9677385389466656959328936293552928461395558807448542497795587797746168876269829197427570030617134769715473552019108108841396493661871344292967915479399524348118320734679458083871139706388930790126323699951171875 :: y; have y := 137980554228479458950786992515397007215641040831708198510983315032108122575086378506559458459572839175474057230060723432471793103853187249183798703401618125758448343724528184853445757374036845937660955459334623805248856 / 19535941381468551370836462377301523751174509673853473173074412159888856306751011642384179020146418602205773533906730482992657234125539785865480827327780102504393359812151498289267692598514258861541748046875 :: 155612801102286480249510994436245607998580046991776383088021517452698713956994246263075087435707587725556872916492446666804971896375762888441662530351229714882528311179089657564695539367993138262567214484417540542174076896 / 22719664511481048218221965534643060690949249888588374553190482011473995531700800490933698275909304463028657521607221641786054098012096249342501666220343941160495513449830984331612171445158310234546661376953125 :: 4077564243818971460016351482386252357988006576420869598567642331968927134082205935752390310060845923961877320637980374109508736618053634328678411502508781685598966580331304068007448237314750259424737744807236865525280110492 / 616227208211401353980389619039626399971438885439712374419612612095825448036746327161786308621970827204915741701438950068750974996851164424474314423791790281014670618646954236563573203966370783746242523193359375 :: 136229839115948640589415337829078079626663596124872544035537286774112010350895388381628890070035085795165435038099518845476601390695615093705072176945488000196980679257932347252905819153115669622856956350996801495401624 / 21183453593878466409964464992005744852968474111003580046702845430090314217696528953275610405061618848113164108903412177300429898764485679340701203009825220698232237613589656888279932900331914424896240234375 :: 149697210295748012655620668644161331483050622741900019502726048691719389227436607286881405908173513267264804381174322021298044672603192230525375045185438637222388221171379148715317272074675629374888944604899769798105861873456 / 24032861120244652805235195142545429598886116532148782602364891871737192473433106759309666036256862260991713926356119052681288024877195412554498262527879820959572154127231215225979354954688460566103458404541015625 :: y; 9204419650723574222226941377922110756459259629976271151710462085289489321765835261302098910116873918734421881360669632761135943775592973609643411382610399985943901085524763935195147718798102861948267401057210812605928 / 1073454500896813050707392654601609293217540745976299293795912214102244060085083888066794154307077933523678597760794785815547087078294176675761949738735834687479117101338577100477778003551065921783447265625 :: 611587677374361673157436723466629374974812673105768827282520264263499817807817456549093693828017068209575855546076915696661338774866746652563896782299781085412834240876603549457264114586776500625142633447048172187902496 / 74653881198732907617377761888202828119219879151988087250352076708019700542280834033736138913174056285964920662455273740808501964990458650632535595466628503265593143865819225624136379337869584560394287109375 :: 2772927185889227984643350847303260530365281111761950968220227342662496940416834713219902313584362964513593304124725367111973489447408350969505073243077650026850334413758246964444541743983517557075431410748044716544 / 351007799942322555240617039233790475991137246612473437204453395002646561649572887286154201186527463503945935236379417424834288513238086518988325232279546462394424766184641839572577737271785736083984375 :: 459916140876297316091361879360510786050682518352843452412858458754024475485073121524864329128000057896524647132888486362123494325107554848380401090491468853305923647602440636142597847312241658667821542484496430078031028 / 60664685442573948352139406507350406273456154049633562792628444315886279179402984052639637206921620513459782376157348571359701596776030362946438835235044063014022536726999046408081994741223752498626708984375 :: 3702316608800685146865818401786890943934069881318993882575336831186093889409784237044684792593279011449738547966804699186113850061313753001635553310444239205349757415073150344082133920197226428106130863633105629947144008 / 504881433588467738182710345214290237576649997524186101182010711366088789593351122020748850575762321400636833813493814261912313289157694429833370360452087581344344743329577429591381587670184671878814697265625 :: y; 613875724774607862810333463704414209067814767599686350944348013598243604299363744199565325259497520546160142577259015866761258631171945927418762635908188452885379785830720209421216942162764053970862866523957664 / 38524849856904215942271292352930777583529224833082532323862253754311922086909038773304385456898222889483662691104965139193942995525642099431901150187791834332562412868128376430831849575042724609375 :: 433194094690180353696397971723126389300553494207894443745444037899985938154507101531097008492145862384858391540539624601709212455478113385426540260266265462099846455514419734849673613141696222133333559230270453812 / 30113590971480128794875393522540891144458677411192846099818995017953819097933898641132927965475444225279729670213714417136598774835876907722602732396790617169952952725253680910100229084491729736328125 :: 1569569444301933412102089222209692467017698183669442077236037512174775475335524065643345291908383742716253484517983053231556433338340776675056116687268870049102276366131789101857384086377942547228263469049669005464 / 116621725035004862423790160369112905704903605246983203986571744342257517597453098373842066484477629454265134904645839470001737073455305115362079672736661844676363253281436982433660887181758880615234375 :: 1668873148560175202345197561957768312127526058876844258845818601840618915478318250638208476968324321963059188479709054593991965705918291868804327214129854620917886518936913111925685773425719341920798098026509424 / 134521197041321278618094840511053370906421719499124252212830492617515400073961069814980886923267565171475740216481271715546063246671504379983523688360650175620258917064120396389625966548919677734375 :: 1097046185949359631991950832218759295595711878927876848405200362161833663286472826381281698024645078532553440358361761293190896983635463128228729179024941332860082147885193616743738641309565312209590816737851044669184 / 93647245203108904526303498776397663281037595013327512801217110706832786630754837994195179387035536451774903328430609094411394869984610007635749977207539461275119692384993896894229692406952381134033203125 :: y; have y := 518652984728290748152392324011394492346036700826237449271950857761866851016396325232242242937383829307830630687502449277023921499126141053509664148603856834744564006696003766346913651800015222592100443636263412 / 29963772110925501288433227385612827009411619314619747363003975142242606067595919045903410910920840025153959870859417330484177885408832744002589783479393648925326321119655403890646994113922119140625 :: 50447677241358560835541869517897918734018156325109473059274912836613727788051877887721985804138262994913795566360851030129650195583945843661748554690836524401944619687732102800794529438976 / 1878219145490091449294355684280542512141060569135807962754013762936290690927106355766271108108541984886205123582550906784651170930715465001714647996777785010635852813720703125 :: 275407630536834541698884260337087254019902335762300875374744538844695957222409905337018204741495469930159810014297800631098462340115993679192988261567900224478108076174652114806731980383940383305533786953834492 / 12841616618968071980757097450976925861176408277694177441287417918103974028969679591101461818966074296494554230368321713064647665175214033143967050062597278110854137622709458810277283191680908203125 :: 5182471529851242450084419599124160658841709225992596771186257625464837401513642656997635509441943846806606310473289256399613675244226359578495887770210408578304710323110072059713427918542904446254495083322675448 / 261857312795479380825003421935138183864858064445155183476686913199598426938555640357677634482395167176345475393162734062057380650746755719326980281711222757999590893263075486174784600734710693359375 :: 103727189700928208873050045306081207577031001591935127325242527904867679520071672175716115860763863137902553958945034965932230923465665409366974506205760853103448585744321583071253707922001022680257643568798622376 / 6022718194296025758975078704508178228891735482238569219963799003590763819586779728226585593095088845055945934042742883427319754967175381544520546479358123433990590545050736182020045816898345947265625 :: y; 195734097851399878445819732359837768729556391184424733299445506185919292293534690607802812898505284182571224184168650225550492351412198911806123475398118259934945651699949548026899767743929865510567 / 101732255136872083503816679894086213454768776925108906699776154543769268859397005682906023040441408245225326743392174197049513222963496296650381944814967027923557907342910766601562500000 :: 2359294929459120820558154863735377162690377278056371348347125741113191468484752718759315620487810398030173826853068302811667151514046629385616250353833104387602805537027217337573198517169020085665963 / 790241624723917077217147424177276836657578892186113828828618343331064856318530312001145000403428796190589591667421353137795325928377158732909216892759118877620494458824396133422851562500 :: 217602489933889635133929465472623151467361362297508130321259578877370628936723132521315324573695415781646108191397352942233193103203290660527620820519534383406492461800995682408101218733568292528365095207 / 46970697786990072802463695457218651527987837225315108203446948538249165355803332096848856991979162159494740385364857356345533700661252911630151197358573611495557997841387987136840820312500000 :: 17512815776410904494209139478935038146518620432473901317402325050861853110577726651586779222569501727470363954069880727965785651940900894979377450614751001138371010294452121209389227832409188633233131607531 / 2436153306375235122081626666309975060980446096089900900474931157839576903165415128176949371295534622003025284987096544039690469051603828897433034216847558273144613849581219255924224853515625000 :: 93918996753558271680755394353556022584074316576968098563942056526478244749461558008621428385879356713319063602665904973026284343205000548044751094654354527858496009467752469353027367942551865780452278069409 / 8419524490482477992587684521303534893716988646837824044116568799133877700473902245891916696517187647014275316487108300409136502665741575196323183190999506209095670783426612615585327148437500000 :: y; have y := have y := 377476190100922282972837283231736343684997909545341127805962383876833687388365811002006343062750869102604812781396568911604629925781546886097952341039256283214897087962029679443792859 / 1765039080283838672365601632426481181375222305093862072449961491572217245952467977113117120406505034618781897846788440328957008225441160931268314016051590442657470703125000 :: 2628426313180955521921194244849779627102410383791521068966333380727885299842937199199028517510394528345537888579017961928615160749501364951512272668586907250534521539528962256566852409483 / 7920380630789478168731115535825357132844813354331720015635985093234065388942495775192861351887295750084070768969325390655098659015848072684207181737292557954788208007812500000 :: 84273918666446578124109432068667695992045880155376478394097705360089030485960472273768722566804586898824949447726744495168924460650569084051591673029444319557624000917354951763288964053659 / 163654864783687592661406674758991441757405955933879164823078541988948876099024318954922497683371248436112112263828685884410976041914960801837430892646807478740811347961425781250 :: 702824958763059641733044679631587104220378533653920336157270729347421983450508595125894591828458634284627967836348038529471806166642758363921803034717916322546059980376054104190230767479211 / 879565914204220575230417340789637401259880658918763696655310156172265774246493637008695431564682539857405638112932551162548566217550677359682254063955042511224746704101562500000 :: 6143568670789681752832912980505643385405231185800681736488303377656033142029794480122751609978237983279920355863634808878995528229361036111898196133774387552065402617739647328588706151571578213 / 4954814686190925555416748485003224890647222721854125594183525937257416172774060280679233539861747917651730310899677293836426710645017353236430057705774743226356804370880126953125000 :: y; 97057225094892900588208581108126539767814351947393703561403686134142381503995199515768595115793948593316866542646045084388320184443012912341006780948756706388011056993202081 / 4082866808401636177001266731038585885765127422967375149821688033094759773212513661579357344033532503898286518599514815369699860525543044786900281906127929687500000 :: 1392164572497468614266561997279581799686915679993160784049456159061158558168684890683806518818102062319449741240520825909358091880426917795067792046533509309760565682264952152297 / 37741000060162624411155459345037928281541396616054674041164228755919685653633173159224184448909966082909786006304265074573663085732988520248909480869770050048828125000 :: 55789897525896879634759944318545288169755256091761866397560428400303981456644797057825793065637315621345711182881208108816825901111038002838691308855302822635360320830979913583 / 974684083186389112807576983456267090313647942292172657983313662861599302965814045225233112298379829079970725802885658326651929783679406682495027780532836914062500000 :: 39034152822192020151290811927751161645581517902375409271715856703579906693968710349076030282592377943677862739987138993010974860792375962534763447034685449449600813765917408228693 / 439479429931339852566208725819372429481518201518335119719341611467009385711306904064873618605845435817760261971872280537612393686019984784252301324158906936645507812500 :: 29046093798200912882211032945561355085451378044733705533752654023963410754745432974758310399845637847667343384787334310541269835672866830283929295758474717281328598686801539823109719853 / 210749723746994438259009997214325132323285164428908496650691953729335548861542958002885754560721543673792027067039520898128797717768767583379485586192458868026733398437500000 :: y; have y := 607846930602443054823152928079103540919709757093712230006216317598613923215553499056807693016638999315062500710582452006245521155245227020389923370803848395001 / 230040418964383196425136433936735093460447057857652259751793034531713848597892086560061673391786693524290515616703700629841478075832128524780273437500 :: 468910489511653860023523967988704245406854648008226128249483592417832256012337013323920166265396688911485206681224209604992747364212838152146741566391930203318373 / 114362951142293360508496398585691160748907965906375694848034251452909170445809208747002089057631099066361570620875554027406906243413686752319335937500000 :: 26820446031980544686709286929704380003927422733736935491658859238415778712186726403315895749703994523325729123949970068653889125737998739984675695561533856025310149 / 4215478570131850264848708039446779180552510206448958836148462526581312501143288386629627003763786327954017157070010224373390883556567132472991943359375000 :: 12933355487640315351435602599409008884909970864240316842271888598202231767175749922998282270759990167894748891728451942675087419886215913921062973659162193759615552360523 / 1310018982368454315705443905170638885265220281796904243756840808610514998105292872182569406197649294420302187799704657367172444537573028355836868286132812500000 :: 181271074648183134574315872610667438687413262556293368279099361945789508598132894948325473375811986118841680385082339942893201848379649312439681776300432389301043904277 / 11832605011010748075827825970706559698720324389153931603700700825281852661457691017429769345846707705000653066712448628627907254440287942998111248016357421875 :: y; 61512454383650526664401659169766736315080800611273856363861904902864859893939632177902652068598608907394441262107389239385386916203990981856583473 / 209433215905820139555576403466887147956565682737995827466821769226751450583613834560679019033274661509835823380853980779647827148437500000 :: 2595056679725619014902954138594186433984824774898214269465267892561442465510771810105224413393886988497009794069637562809477305990469979304638715513 / 5693965557439485044167233469255994335069129499439261559254216850852305062742001127118460829967154859798661448166967602446675300598144531250 :: 45963644027556115270156323821692976889463404459961527249486202192433160458173891460081154856168539336521741965661136158402913139414766432170276316030893 / 64993200458837258088142469711475621738213071758399507141951332822368550908162297665380959297577092431685841233957035001367330551147460937500000 :: 41926296984212033546113896542653322799068309890630912379518674747075435910774809594453387308064242051253103924034801971351033284069748584517728253309541 / 38205462431884063876137803141205264129895521912032142711822742942878810331149458762757726073575723253761271536177446250803768634796142578125000 :: 2770812217494529857653830379709705375161895701689373284739058380516731672917191436287282447177841858388369976512927790346656334419856133384342340495346593719 / 1627164767210491221397958860737295090790076448153154799305344187669063473725142964173734206131117195574115052991714946983847767114639282226562500000 :: y; 82576972749469308345137600717862804031267861565182510893663707695921949772387486461909772401845063058309133816911098717 / 22755537332438861505300332779919589687734875080076906359669565793665130248868422313535120338201522827148437500000 :: 13934869853098701961335418388417194106953065486458788789118711172482302952866549291460053982134709367343500900001831666759 / 2474664684902726188701411189816255378541167664958363566614065280061082914564440926596944336779415607452392578125000 :: 249486396854375163964793104505504690450011402806327846763606161227217752092014438598123022155469292420994049578763734848541 / 28552601733401722057444731460682099490590499218792327440248701862351831531894319482489663641899824142456054687500000 :: 196821409534312352148720243172761829954798085963147229218630102730049248914639776545269506975553725059102133083216577684830526 / 14516321175022269254767760504182408644138025993454136722668941581206310849762146364394510555939632467925548553466796875 :: 850268575202874474072586510923500643721451470505198287914369142252691604014526872913336720545378110107536454887338997702172119611 / 40413438151261997605273445243643825665280264365776316635910333362078369405737815478474317387735936790704727172851562500000 :: y; have y := 1770729932472930457742485918949296383957968629725343352931232091596020935018633848056725654294685490322611 / 4389928963532427002505360059016400245772396492254798625607184470176491686288500204682350158691406250 :: 95619821376325036861350521143957629730220602425827040033227800713948592693759714854255395650220145859965366413 / 152769527930928459687186530053770728552879397930466992171130019562141910682839807122945785522460937500000 :: 8390661627634496340321392131427472169185995650759995524066320112328241844119966133356949177437355694563516714489 / 8639116804494004395310398274540734699665329952967908407277402606239125049114591092802584171295166015625000 :: 4530964781074422500668489558300066093725545418944458060676926361491554462105333474934041514044976071231039307157161 / 3006412647963913529568018599540175675483534823632832125732536106971215517091877700295299291610717773437500000 :: 76460110262097477287587233973046201600672371404044625284130687235891643782552705360863238954166623926754591438318111 / 32694737546607559634052202269999410470883441207007049367341330163311968748374169990711379796266555786132812500 :: y; 356728285286445091281898107172761586450424424577798693177600365950004097484953481276936225483 / 7957243553537956589037214923700718741317417653791110865313385147601366043090820312500000 :: 210702255890065394401235381432219103202707778506390731981524532126852953752741572282310964419109 / 3028725827565384726702289930333586070913942094474241573109907221805769950151443481445312500 :: 45512968177504508947289170168052282575656493137344676854574362958475545098710927766851255375345361 / 421598635197101553956958758302435181071220739550814426976899085275363177061080932617187500000 :: 16896986512286318882750961050208284392170877310583670646584975937352976880812542138248858940362282849 / 100867473470906546784202382923857617071289561937532351654223106152130640111863613128662109375000 :: 209862857422028311533758799504500350061011079830676840493599155686482134358549804412039978772908022257569 / 807343257661136000460755872922556367038601653748008942640401741641653643455356359481811523437500000 :: y; 3780847040170504359651127086718623592334968811386522877912114191931 / 6934762069106560237324865525465611426625400781631469726562500000 :: 642092407948461731593935027107608110147683765730050014541428978349051 / 754155375015338425809079125894385242645512335002422332763671875000 :: 765674420290779140812122546821428645051116246746187215280307988120392621 / 577381355111743098799430978784741341769404243677854537963867187500000 :: 12950313168733669549509097255204210966199582011037736968440767739342234567 / 6279022236840206199443811894284062091742271149996668100357055664062500 :: 182071553640720411199266897326366189990474018686471563728639159243489516931709 / 56812593198930185692567610019482193806084069365169852972030639648437500000 :: y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q0_eq (y : ℝ) : s3eval s3q0 y = (s3eval s3pCoeffs (0 + y) + (0 + y) / 10 ^ 9) * (-8 / (3 - 0) * ∑ k ∈ Finset.range 64, (y / (3 - 0)) ^ k + 360 / (29 - 45 * 0) * (∑ k ∈ Finset.range 64, (45 * y / (29 - 45 * 0)) ^ k + 5 / 2 * (3 / 5) ^ 64))

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q1 : List ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q1 = 122372661240979258637567639340668406957046157947969230217738063710365930782557995312098481828479659429887858560558145110598477158947588534306504071341 / 36594558259040265086621461002128054968828955678752883258463248411011422173825180047647050970995919773331994662157740094698965549468994140625000000000 :: 6851977522679626214124371946291945835597464830581909598528968588733778258629233784114244917782261012208159124150991023632854838406690152790808278671 / 192367902234699600567990407971385626420202902282001451466623665729525921499503434024991538005798508148558312313980422914028167724609375000000000000 :: 42606276788409824447096835920704355215314447051799526075610603145604801437372288790055595752402262513549423507872467910384449476932770639104211683 / 236886767322122798385591798386425065133489653944474074552704654381023592194014156951554707888494277767676976509392261505126953125000000000000000 :: 52375121478552847851666480017262284851416923419556286152673320196165385209599729039078417897097866289781225344224541155638621751101349379709481 / 78375622849716611618399656611124266952976266048753731240740205244620587169770180003759328570822617621161043643951416015625000000000000000000 :: 810643013597845725355676653142063617068587110959339894426125493182019388013567211922945676173583495722102150931953365372204238400869528404057659047261 / 357681471488455638688289127282139890939337267111419224865357901844650733576502561133369715970301285778987221419811248779296875000000000000000000000 :: 285114409293306548723108591533155992241477880024144396505110782221194632393518102597629694037511113395467913778640108880495324636699410505757231683377 / 38327903565544423586957885816685483912366794791885718699693919830272562342679187568826452534131021820940077304840087890625000000000000000000000000 :: 3005399803077292713206166677853893290807515594778033615762481683957553097251020893920929232436936036662653303986596795672918352006373994530536423746886349 / 124632121620866320325163855906310077553973518851267854353084708909424966721768003523805269920318314689211547374725341796875000000000000000000000000000 :: 740171262999504752489984008742444119726320387385863516876981267310810834945293338685083623072245222432126861902628375984046849707414109293674124479881 / 9515861103864773062897591967203397022863916994461782405828822043424693654799458718101865454227663576602935791015625000000000000000000000000000000 :: 836436238846438689256042632331653660164833238182825046938276952051447170712455779050546660358625362414848790525336579779757779286816434808630728662276745713 / 3340566952162707525980460274548618830848384231774153771378407240512450390080892812398746380086480639874935150146484375000000000000000000000000000000000 :: have y := 2604534666350802802263097889477643895045174969986673555482453527419368060105280176245311318036909094672060358979581010943827124975943279963989609551370272740083518063 / 9421706149340886838417920583884597442649269057424875984898617147384191439662002872000713231678236572265625000000000000000000000000000000000000000000000000000 :: 54310845416410735682152189631138546312968043517104804437672584153932936170240008028234879947931366081001717586359035699390207194119960622769586221038112081880767 / 61122285166128169769588536334585327822657667567400797015164134791464231956871633988501111662109375000000000000000000000000000000000000000000000000000000 :: 203154997299484444363552872545810292347771507096412392425417511779990712273162402850626566796952032294137739386918400242766361038949992950318290313813680619059590195272277 / 71130391906727643449744775252556901581838037209832841509693856271214577150396395015875014264640434921875000000000000000000000000000000000000000000000000000000000 :: 56658363972030565615096273076450752709143713135013344436265580985100167092649811564131009513185389598292663520056438688826216165390629147001356025378135561481125047603 / 6171729249697863893217976474127627958902048591905993428285009011603484168107141218369381369111875000000000000000000000000000000000000000000000000000000000000 :: 2194076733123760584679741643935876230877629192843461214500184843765609468712311725038560742942848087169998816954129090722296501986191683809499682331934705952049010822660021967 / 74354969673165963286133205064006147786881361563345263658133311088842971314547698256594681577970801305000000000000000000000000000000000000000000000000000000000000000 :: have y := have y := 194035534772135363124578869565201130275049112856857050020644118802894244603353280393891056831578625152281999795237620532131481136064527148220815415908543559524438633375562512258957004538955669478740977 / 50650959217537168905943950876305452302766617051956774174881050009182759568815264405023276515046941241032106355636305920000000000000000000000000000000000000000000000000000000000000000 :: 28120300634762558668698156949320534730350855235576814523477510350753053245612630713461897985072773931080798921891305301138099607598845260137540099458527271189263625852046844064607354316338171882091 / 2283714891286147640944214101676257149214939323988715754438831683346553590714971124403184622428420653120912726425600000000000000000000000000000000000000000000000000000000000000000 :: 668491224397268258189539148679409597056765878219097493848606015373853805266198245981048807022370756776583122166704911219932064577818751567657999852453186575620119471073433452542904808021944850842329289410653 / 16890136395292234392934611117813984532150293144301575192054734777462095249496563155518268484409573088822887561492290087157760000000000000000000000000000000000000000000000000000000000000000 :: 598648857669226698158921190676151995144698415937713481935863463782872518680601279358028202016541148430785769288020086107119506198264773806220162159164473981208903635046265469977738638721749594672995434363929 / 4705709642469478238827553346256632506469733413337752292313756952924762855581132023427975299138985537184486086783921616322560000000000000000000000000000000000000000000000000000000000000000 :: 39306956436591934515886161441668275754528164846546356291886256133424984290099279614946754655420562859393644496294798935356269357820777495404427531126672643830863247137957539620347769897653127751955525697029 / 96125344105324526212500232231685777401793601561689106306036292839927645211054347907454815964989648757404065864234511525478400000000000000000000000000000000000000000000000000000000000000 :: have y := have y := have y := 286502155223608689163381273647928724239908957519955315580999496441681590064244671979210908787516488455963798125536137153103087133914025632589302036334754401574987991260791703024977693486077591226603155196026549145556345371089466816548221 / 2233667489463214790226747309543527130387194091636073013892139669890431545398326783023067553318646069550672507211832306763690945737415196672000000000000000000000000000000000000000000000000000000000000000 :: 95018702594938566274311317890247075615930881314140569390774602290797440064592626401904290369145015819115470394599099547762162834581987957274211871152410540990025597916568179648047684535138058665258676239696839113168195017229040148889892671 / 525107795768545231386638841190934448196287733823217164669380203097048819444518927938756231832804514596123010467343033519885239875111642726400000000000000000000000000000000000000000000000000000000000000000 :: 60857012972822167091890503074597446269958912359554085591166061631354906313529439347694722174510371493363814562973978284274888809545948720176058113121479422012615461302669278233292561708502355814335119861210682332285479068951727171963 / 237384291350572803042323960842077382473797129670659760230845387097128598267530345185511191170481542010805303917512333999010674928254976000000000000000000000000000000000000000000000000000000000000000 :: 37719033110598709847339630157164625367350468089992473071844083333278660871536014025895378963107337135567003689953614395393078845471163195160615149333404662191267092594961305627789754353904694739762899268364789043161806591594777486313064677 / 103465684203283727073219208708732269052009286812574641334855654832455545164623729504969746420389630283384237618009812530584795412429405159424000000000000000000000000000000000000000000000000000000000000000 :: 41661597648809299446747455518097791714499536842008916315105877189729085282721113454584504329299273323116236367559260027743396041985495619318330815660882135203887299923779830712415586386209403521156743902635433622706084418860479768323 / 80104987204720040532800678144240104373873928530839919090244122394915823283693367511160155045183071789654464696444491308308128988135424000000000000000000000000000000000000000000000000000000000000000 :: have y := have y := have y := have y := [2813877536139736687282518528524198492639126912082510060834983827364319973147415708591675475382647793300922526382425093541900987205661390792963057252740097 / 58565421552357029749568664763086354416096312394940038261794576247613223571506791964905592555847273201765445766563758080, 7417875499961804364100115411604656393004420226262080801647236623596159781912074996038967550167589167475098253490611748321044566396191827309333141835865 / 1245244843638156114276543038152002220142911625673143670682675375364533657334363682974736851685789197645511139222618112, 171158147055540612961455404031118640545496729278120370499498878933590152572171277572419578815684193020905445988466718125456830083522587905267606161961 / 311311210909539028569135759538000555035727906418285917670668843841133414333590920743684212921447299411377784805654528, 6744187622378010020513183567868778944852162891364398186065910744753661429598560244415749004694631042827763302615060288458823747260309676947059206491 / 200845942522283244238152102927742293571437358979539301723012157316860267311994142415280137368675677039598570842357760, 2174905174873409613827428931669509696206472148769164033316129490585960312508123089979256247023567084226275700596486491961118816271789809455320319 / 2136658963003013236576086201358960569908908074250418103436299545924045396936107898034895078390166777017006072791040]; 280646971882484860277633757631373240974168569708273907668841328481312140410753199193611926509104013060044110947839227198896159485016088217086752940118049588592301871 / 2828061529810133097165036793230252784377258678804266883261928484801764508361040742838951479842811177382504384639282273530675200 :: 6616179652343038315932985391257501453701202434336508910141196992307855607590234007452660194921295787473471711756630756940103512179465738993842703549750366953559417 / 230191054751987577676223925030369412681869892460812420730622085972236646029387037207821632080228816763692217354360185054822400 :: 8968957866896983840716698024919584398704894731640810962631123351895180322610628488793024852382051288265808152908291987400332479779595945613802314555418921945837 / 1221172704254576008892434615545726327224773965309349712098790907014518016071018765028231469921638285218526352012520875622400 :: 2199421688253036903540871909763510536015818817450247285750791107904073130255192928622675719863043601001234585220483345236471904710403578053463431610389511 / 1349433676321590547225084441545768534933094755643779683451487931972654921002460644352663422945789705109802897847091200 :: 12872046965842923842969529269562830470435968909880761647146868877621055581560724455152386810028324794260977576396180204553469768669588037598756991298581741 / 41832443965969306963977617687918824582925937424957170186996125891152302551076279974932566111319480858403889833259827200 :: y; have y := 6142633397278832815658093336327417524871729709539815499026710037560870304016879899795009649443728239014361942140947316529681089894369568813183617750499440216136423044763643 / 572822717438542937767390709536926398422036926863754397400683304682795709161730911148652914120485842643610985468655837490961815961600 :: 18121347194840131380620879565662841887460759333143375229641125359443493937649146452553457099176611933967203009981561046842253572704932881987308635599822270037239735032670369 / 3617292903026541655790529358672209274292596824186191848774159759948120132356118924504131927749764256871405957017143736528291024076800 :: 3903019372216043759894850244778947545717461172063798864930467677616538914542375111069614222404872420825924796762157561497158565787209454474352676589199350725720584480621977 / 1808646451513270827895264679336104637146298412093095924387079879974060066178059462252065963874882128435702978508571868264145512038400 :: 74259513633929169728730820046820129880938798951367555710358832487300894464833823476523241662720916463084400038405592395662096208972763874836662665273735938625826922087571 / 87163684410278112187723599004149621067291489739426309609015897830075183912195636735039323560235283298106167638967318952488940339200 :: 2549651545972857166758015227638361692357526279742958950771577766496832261685923434378408340524417142012477408401619660854049307539730589811799394060835180260566817 / 8329936043997912843626262673959826583652253989563584619533724668649149429849310289715785303180731644248608420388187563622400 :: y; 264121208250213220153836965054006981380436785528519645609600061248712496353996448018409011634330661718349884274422442235898307664228338924634376698761117964383389468868322856128013 / 1568503457395435687620850228457778436206744111625273668198839059273905942467013706046430081097266225638655248211627696084562278148682547200 :: 12289406162634607677881589614708747466095012197557973028207571112299824262515674615743472748428416593297196673572270261546905009429628004154497125312253863093859422857010158015109 / 111503378885717014094049205955619945011240020035590975980427409356334281562585892240552181651037292185634739987386670702640663247821209600 :: 36898175176448564189188845725896306005602263430582806836498321947911317785431831948790097533991111530060224703989001537236848929886861397405533604735348620854224385280816486861 / 543050603661007854956353623454085689989149054124005439409989140307427417079429574619577121432413113752508612577045485602127623906918400 :: 349478042057429033807951954418816052058718020235889593189088168942998184688934467483535992400360737904769037134077759515153472730276468174275495616749326239818299344510492171539 / 8888312333926389838217984173802216843708340155098608922756864695668384289359735252493635617503196600556642954659573392328722820471193600 :: 34712436382132177518499064520345372749584162422239208581862616039166880435547351961037102738887616413918716599555481159603120085306808987539165394993154802138252434022577046497 / 1631399099264970286761528740761166382705961167707972523797146051736602179692609634951363499415143679849004086614731825174259251858636800 :: y; have y := have y := 19796820322997520438230318926822393542178934306834943645664725824499923735590528569194994642773491386162342464816519289242123206675625757576600309753406073969467423595344366975939272415149 / 31265168089131027416158447381121570711295924092111545722184277886551300964304025186676016199207139664121495250844251091654330062204031905824768000 :: 66617775411171950778604544706485315837548475883699102856849499699507207492129027439767737000197149901351512923618438052202678143125943862294169766505818344425085978844992410169121666007 / 124448005253736483897752546220018499463210965461558510223023763786027836048974993088422599690659159716343979871700938209279329702588002074624000 :: 312192841656330263033195190965013596010289165447255790852139682344136770636154333783800729339977903267438018876592440612437472024606903280199382030283529594612943102883947840812353 / 722258364598247770787402185788017106179838921101997111053856926049469751421760336895386060048862241830392677312778218783541471484051456000 :: 68617264189494971491673804148928904113749690702279537674681458406912920978508733324515801085202721836564909499637012318526727709288044038879158632315087557296609929565770312674431 / 206350807390505860071768031477945643993488471382039498653224378448021124640662775737966918161664495429524108563821685188150895849766912000 :: 11200015738935444411977580101061521818087797225024140046641279708807087868178593557940032247564645662628728825392903195193923829547258251194484601018809554304221023746108909913703017 / 46074789060990923323862475460947241563573108278992414003340897366170987059968527615113883632232195378135497916216563572484016920617549824000 :: y; 12232039668645471142874713540976740766130755928549509782056184449774752313632962359764563632309021599114877981121975899788868107336395668329170638573985438835501701843831161011025545759021469 / 15276466154379557859217126253317278684375396276518795011037015582958102737022013086943430061432112899788924740491777612661248637466667589497257984000 :: 48618539630935292433685392229658750650278321712210429534271874956973377283261471277570197168329887123156147779660042887167640161645874186483067096349866745243371163821029197528193887995369 / 59166362396520108844502378271869301535933425971780709942614551190372398660296857789975499009891992149191943544319184027877498029107629998997504000 :: 1172157791150505899354679869798060284145538417628681768293690603598614502091409235354666804371509449141130753535726071511777341039310691272571149810411963703244057108248265135853701273093493 / 1438197732100027261143288579531592252719612508237131103220476782781359844357985158587096745163528424549588781538835550216099182861385467667939328000 :: 2407984167422166119516716242610286214950459363914600723565574613403101033910963304509997115633705073193921047531712483374177846464331291018567043488540821559587790895617654433360053735487 / 3089320971133568141913871700910558374976034799584055575324884034394857563888599977136856855110024705741020185063592556643967180634172352888832000 :: 99525485201506905627876869995564866163703951109334045376100450898585275507009257755157496270740817889728818371557856787174138803874432428892292397915803942442030773000632221675136540944881 / 138786843712727975359532620082051850474533126457665885888720453057374067695203233755488657274529254118783222820820821919050928568808141630734336000 :: y; have y := 16516249449883261044536538728479360592635825710746310829350691615663139816903989282091136483482125567179653558347682159250481638142883607716245211250006748372051458202922795346427465861103499 / 36113600457829387293856448570607898211038032982628594392716017110433267675027935805461286298626168805620573050632476333975859256671541319388102656000 :: 70235687888533816853680677861881054035185829991741545965220238924057264643984376538697061961351311908035903077332211977511711542381571030197639133828690440772663289103532329230018338707543987 / 130640124354694149968477493476644314266382699192298660784040684985296878578671008467654160525350482729229425366964167170344471106611502144666206208000 :: 2277988825421761797260503398124218633991628816975536233384876272091792237672158658923201380919373303712845025506112958627703620696964917516023389854556166144714803114359297755716150605994609 / 3686647707636689598987021429221828028098161640833209306846855978397288615114835195251431093236086947436974059719268593511690863109466973458661376000 :: 10090318211653587011110405573218371671544635975994696456187840871924886526614516673193915026130249328322344759736314446275473201910431113008635544391669629222234150263024047446660527632014417 / 14565932844873531912276794799674614559520726682262106870988782300029818888788431082899549593458526253287114287445648421374678933398450492311339008000 :: 4961835091934485879748776982569355522606703165603728754753726604433859754182693137453366052004821023290809056753218987322989932294361250428547544500950833237206804325741182311497019665627 / 6564807063658832301566977364434936546824073949116118097565378573089072323263274951415820817108802499699667893260134182868430258847616249888768000 :: y; 84425110756094248504102289492998124598360959367336897467298584251662953574025513567716208431100472408087719784828370769218453717055829149931904877012126716087726663378198179010327602467401137809554429 / 539051096685790998063296425413362368507273993080162368796019528666608174710920742738711159817854085617557906870686883158964859138481873174811963785167765504000 :: 5282815823427706300849997508644539611760972793958961002251360137937726044439418585575010782062035279540806931934719156538936445147080941742653314079239207935221972573075831135914439046684729953 / 26463498791228137432163467525411503672887273681465169520985358612036528867463759869051537948980367497379326439207219066707855111324767426786610905088000 :: 400754954541124639329248262786606257801127471541355982280869520956493281458524634738089026130930830454948602608846686890725563934788407008272621408621351247767223057557744266223373108884016072709 / 1594420048998748833324350684184977693566944484776543154096944353408920140765724527897372738941731055463869864089867321211067181541033562983418313048064000 :: 162726563227638926082720739122007026591433624118243259227187929010007312143630115346617578192406662388678081557231871767899564980524636971786565790282924102974193539328546085315830743645204314739 / 521489419011170809870110581471720702141941955777402560179417466078933993544322150014812339473736534095362479994395616381694901631151224537294049378304000 :: 157047240535671266306896221264900015938631221821375634971195831908470358159521373708118345896285216895133256833709277303060855572135470830266404343420200894707305883996549182669436665473169374349 / 411965112144417913176682788015979803018542208248618676869812471360808578540540416223934287336658485298620912714806264378170180212670679958717185654784000 :: y; have y := have y := have y := 534234129558660940290564187815496601192718493484473432314559928479232867390392903676496225481627723863969771070175828996917992958055515450556843471160718063426973835546952894486145493312405016317 / 13060939539779778010837769563223550312736818983334036848129955627704210474678250211734618138637674103933851203495999301196085945398378396365864600338432000 :: 2086662344658881105407145736646984705577738056466691920092519802185196452177800960474079156865969784722932570477434775373722884013251859484713402805973796654172970078586930985339461823354065368568161 / 38503649763270785575949744672383026321948142362868740628287109190472012479351481624193654272703863258396993347906205939926061367034419512486568841797697536000 :: 1954304232967544441035531534183550494940741902086748046456068223664614082676325425029006805966072835040087837898048932329673329701259457990064597768171661770701585498591996089272778700114383307 / 27360566546862989548507991848306808882137689738463988826781472463292004422293039864612607031996651141358286657485429882528460369335776492101411274752000 :: 1112031878087844456862304908925166171786370839208327609367941845311003120822778757435728633860456034798045743253720584364557178228092255972058840457673480262039828067032956228072029574847484738839 / 11887511504560291934532184214999390652037092424473214148900002837441189403936857556095601813122526476812903163910529774598969239590743906294093498548224000 :: 34936844440024509009877852244015378785377752562345176697915505201041566564951875345793546227462509946964951827354266524949893620782552728361285493861947585699018614844896034262635049089493366140879 / 287340669875155116238430930390918106880210017633348810658859023809492630442921504658161599050028830286544726476911984626313890798764324720049021207445504000 :: y; 82479522149766030778404907737906614015640761633035737243252232533620952904326558306158352392264625665829662767573797293220884542857425227302234200375015739800859444060397644735192048664446195719949 / 8629690784121336253014445081483341430100440608685149514579839897666766145668756593425077424337055707221475107638833236371035507443442738461063550567710720000 :: 65966700749971939983277539744648466067421556649797354892289661982105760906278100380281781876626241818774947397494450640340663392324246408703314286657024603286298263570499005765016402818579337674843 / 5141885671450144185319290333311166123119547683965189243369056215538289176347016399146049667211042226180274052744740777523511730083151073937719326870077440000 :: 197054728794666116526882152716451712547765953628331074731131771312888315502423434304562988970239690661455716230205882624481475367626566092264243383052955165017255951951487172135082269749316385024756317 / 11454835804573058708845049040033950330779572352953450336915414984165423712607065783197612146129399319373105521002096267128003256692739804964754230434815016960000 :: 740642842724995626553864729295938933659741382097752354549698320863030517984459985770480270435180104660112523949684085480767162200025287688571793750880449174285762796971699329701950197315030721 / 32165917886909525875988457673968891996383693680541221555176176591047251543900127024315767514771973879658214232706206522615255706802697471517817569280000 :: 983913653927284157445901121208646900504135720039632577727874458987930214237772297379174219309450084721882960309949230106850844753329778292160623376120356424401560024371063386277564639198041643343 / 32006671913842165332952532880401326474911417654505867285430440678996626642917401158453073847280579507537548013496073551095460482699216251309076921712640000 :: y; have y := 969799892361716067776926526287536562488701324934243126387142837079554712080803508870910701583307739373166839711443242194202546692176551192907489759259714807225580292297217638190802421492953531 / 434219117824423710714454364301451413113672512779737037868066722795599373980378464939975393245136726183265213883827312850886799848794047809773979566080000 :: 150694598159898112723612263165393499385423378121031081763928339699496791867799639146419696254998081265756597073060702686734707231323706188768577219684125921568204542791765730535027846522038305933429 / 50797498024714229307516847184186032509000320855669402824458603033993009812004726311297614838711305185690046656328586550456777191542083392304896809023569920000 :: 96735662661299787365858582398137037594504358431338913702504603912175388986302502400719161970137766379993927110518514096425445725240048251023865224225159894651324661367356026150341894732401354784803 / 24423956939388184880266629083228039084817851498834648906003017023806873587648327895943735919252450574356301750537518693236680717894967601204166802632867840000 :: 69450560090924180438508566350891898457849946017496751760344582268461122305365465809261509228792854305786155889561089644272491741122819824179684067954410810420654927654927710136985726580640373038810153 / 13091240919512067095822913188610228949462368403375371813617617124760484242979503752225842452719313507854977738288110019574860864791702634245433406211217162240000 :: 53520230655507896027549429807256470355117423515837760533776120303474945290522985550765555503707812066316811775037724855851661115431452116987118620094613710677589115105951830913847720931326927463 / 7518533766165363977302333102425131317475096659638186518701867638542980941249292872385327357011682491721194936289831827993437191902406526459648084541440000 :: y; 97610069787075454733239978482823024046483185346751002761731942278330984444967559213785442258486084935171038916567257601487073756328941455977254978973266960686620553099450226579794467323985692261769 / 159649279506244720680767234007441816456858151260675266019727038106835173694871996978363932350235530583597289491318414872864156887703690661529675685502648320000 :: 214278877218989547333817265690625220876892891868343374441452632100047380422170619813689881347040663634269651381572343095418059698663143766440903945800628614411169729742385739925010411674690538157 / 274426482465035785171535158238517293087841028076793807932618168806818804355599189842064448530926410947823615174578861721760457504437838215777155085762560000 :: 6557775687907787237349637517372930449471752434195114992129877376814638695287871481695252581873980049952201485791004608561130642985131663397169579533789048522110709030792149494638586130265598870633249 / 6545620459756033547911456594305114474731184201687685906808808562380242121489751876112921226359656753927488869144055009787430432395851317122716703105608581120000 :: 63321437134890560118159368251599628696252917967839242257320741614166795082883102034979231679157104443836157462129557651683886515895879670682431028007922622964372147684620368690508559761071439411901 / 48847913878776369760533258166456078169635702997669297812006034047613747175296655791887471838504901148712603501075037386473361435789935202408333605265735680000 :: 33801245670636641837690795237981728891181108214868238980866480916052277680763016451521057215467878197692092638849239138520855103310971752602007910513411412774021646659936291000009738019597100352823 / 19956159938280590085095904250930227057107268907584408252465879763354396711858999622295491543779441322949661186414801859108019610962961332691209460687831040000 :: y; have y := have y := 1086011509250625951710264338212434888116303240884195814002733163800013303787887516819924054916643010872675415519392935626311663919330708832438214407331492089581334964813120876585449265793746541025260501893947834725224758862365496204430293 / 6779009836640532937831090965826741102878097849591856579044295845139743047394011969937126482547276755218441032940090621782458701309594828800000000000000000000000000000000000000000000000000000000000000 :: 80722835339754853606707126236647584883260181426667107445716703586566645613117396355390489536922548566805735994448684125759695189238210928781792995598046650982266328394943587923963546423170732004511233120622266828073627655522723454500033 / 374253179840899560674590552661825687123296436983070526364508752162461094409524391880180845691057632333252759728894258124113985652391936000000000000000000000000000000000000000000000000000000000000000 :: 173924757021851897897829733239957502491547052661223405099144982277241078756561396656556884774344350802271984413982620623789252981198754988261281138002234330686460917182173324496300902421217 / 609435754403849434975072304081131729102281672670407482928158741820533170082788187863237622654712480119351749015267427917992737009517824310624911360000 :: 1216560881256113858340537757842681138378566003884419113209659098834920733641080126314776749075613701520196899455349097571164913483639653600759217801204525445622444773336769453482470765973666784883687 / 3272810229878016773955728297152557237365592100843842953404404281190121060744875938056460613179828376963744434572027504893715216197925658561358351552804290560000 :: 67757429266801679228886503369788150792515818942682518091418371958341418679693786008362602672578025525592000066364043294194510620656734281091259333957980928618752108674037142907753378837134434413 / 141646809093386324906268768502565263955033107284045188352958673708904817823975389620220506573957874084916414460449569886211072928968329087348109045923840000 :: y; 287271337323143610898125978676676641816689636358454296530511336429170250377288925621772386654089502443692709893287952351384331595600472193629334342012888620901750083046616012416571183106121716666397004426092811475047271172154697703142464329 / 9854380281280760425073927858448676062139134918679019371733944701314299692376956150227353237710019004617092719401572804753590188930492268544000000000000000000000000000000000000000000000000000000000000000 :: 26921836490761192597361740175051808354580527074580758469986899782102159610310703684900837859310217106755722393826395217064017969551287742807984550306627195430667285545390674404091084182532546011422516398617910664423600040468692227058694711 / 643476324337363087458185587771835190624756944316727011213970269675374047076853479958875677835542285749250457423610164489506822038371696640000000000000000000000000000000000000000000000000000000000000000 :: 47390120868959925277414373208946397218033947663678842838228431148044625541902593267940237968776784788540687314635234983246945447729967559993393016662991409077738765546102536463500806464618502436857468182777363133524649199541545587693787041 / 795084299734909557811871919422019350902241615338515095959597884720635068315687313139677363215463095566512369250883305436535423291294220288000000000000000000000000000000000000000000000000000000000000000 :: 1838736463520255230468373799572584285715939564181617444407596430039967228582843685600072154210634535498103263473622064378341947120902344894596403092812606857878424358180789330706893962014898373819661521349822648143321878291659451730339 / 21878229212203489041529937374769544558655109005376539282117617477740026569404533013184606147355542958510388224884346974435379504585113600000000000000000000000000000000000000000000000000000000000000 :: 1593539039455315705155242940687898313405422977111395869442977723576660004256119915558794337240766480655366366419032101319874084449993467136104107954158866375454436780406471745102093240332871630786763283044063958252953660955182506479383433531 / 13625809771647471205040492841311749616784976677679631723879034648730883525261964059573624229920026277989066476209582149782741989632285605888000000000000000000000000000000000000000000000000000000000000000 :: y; have y := 17425199327589526272027571047014354399254622378748094246334680517223056087023539598701417473372128886735750397823426487101228760948538619302862039815391034047417957935378665778367583797261650279979672538066030092218857778350955035453 / 3780207804220331102052580637886658046428348443595104203520577923074543556815338071212495994268341974130601328325069420705048437352038400000000000000000000000000000000000000000000000000000000000000 :: 88149781187674107864702981887838007051296057853055879410629035957636446402591927347094591570600006266518850834864275060407914699200125605381218057616653880319429253199904809527954582492156981347798079369348707018813491153163653079069369303 / 13216874321670469925527893780580483328759052628955656969303717671543957245600790389542068091736441811041730507157165654157979035182942912512000000000000000000000000000000000000000000000000000000000000000 :: 548367558413972005273542921514602673002977874350235268654550464265876796273168294070425836179154156898365230582166689371571194989484144696720847605881982241921274239035313541089425326093792895247201601816250978830375052468202580181302437 / 56788921780130920078025776081191583728272727261455785259333024821197464420265720805359406092942649120260714526455483362506015754969677824000000000000000000000000000000000000000000000000000000000000000 :: 191733871382088146969603438111285400186943425494395256624675139721911502593061338128939841280137829700173508279951725750568855720385848810390135442158711652327085587067948920430493928462745676372918534433682915888634153327948840116651 / 13715384515194886858186207182253387793109346879053481426397093590795202951444752504670919984427264995569375750863102446550661933826048000000000000000000000000000000000000000000000000000000000000000 :: 350769155656312847383454599339631226045022608434808975498277462669962049288789837538970349831954018773688623647868452455997975962560147661029971442529394042261606724236777436316191717174559447955729935189421157744058831212971489554347901 / 17352170543928892246063431580364095028083333329889267718129535362032558572858970246082040750621365008968551660861397694099060369574068224000000000000000000000000000000000000000000000000000000000000000 :: y; 5363418642114822124664661254687372297449046582102681862257746246045393341669597917833830673337122328875984030160430385868528660552013494089996970423436451485407574304584369767748377230040885030119765223700442071453584307851138331613632221 / 7207926853667913967181937820096868831665549963133506759659256377216920694890012902021701911120617982704898387850771772412873754481413586944000000000000000000000000000000000000000000000000000000000000000 :: 145861339946505068158526809915866364442208273895773545530425464588162306715220966571270732524889416981225131381648649512246254547965903753562753223792336863578041809664907233998121512048478500104362742186443013848968074983221309691613 / 136662852916589195167112945563661661806545586911735278630840772835838351969004309663983851912704351389108163220687184739656780019138560000000000000000000000000000000000000000000000000000000000000000 :: 564042631488803474630411475091335049328354936052873424104395131892473706692408824676495842329174611658981820637460759484512831525285261705799975360642492089785284259557417817188445900405428808346284982018415126300352748472666285019759981957 / 367604269537063612326278828824940310414943048119808844742622075238062955439390658003106797467151517117949817780389360393056561478552092934144000000000000000000000000000000000000000000000000000000000000000 :: 404232911925519222119116655447001838731825085660344218865183991253714714211165693227366969565731220706180303391946520318059998539074473382205365810852128157949497706216739235717062961287576178430784335061887169615432678856138090190832753 / 182887696287096324540437228271114582295991566228760619274936355839832316139000327364729749983657471202960108348452418105998289292811986534400000000000000000000000000000000000000000000000000000000000000 :: 527463559975623588937647991645261905118199319227473537443057664347697194988318174035045464541973252467449976780005878400542708941857080784222643961537772712725604562960991835466483352386870860372198967969393704238527524116739722173965879543 / 165372110415047587116970963644824096284229121918396390859824565012245123585200133410611730025873040221083115857844536111781542562167066198016000000000000000000000000000000000000000000000000000000000000000 :: y; 591564064291503454682551356204831556429453716575735442357917476502806712217801351263067802538462184468589453945851223355813223121765865601696847681410671848853049495120814708313891192832048275328035462633367855832018404873107912331956099 / 23388218146472827834382708178454026117328385752091391561629639182896723899048272142516279397762477753138143346784900499337354355618275655680000000000000000000000000000000000000000000000000000000000000000 :: 232566521163202281821759363252939635667188704086793802159275311795844326090353871245735195483294029271826574192383187341129890996598851959331822634957897457573683374834347519065030667783256576771815417784251677087267051187327932506451 / 6765075247735979357394049571460727212000574381606904883035300006622909840057929001074939083004303411181922754479029416677471466972774400000000000000000000000000000000000000000000000000000000000000000 :: 1089642900452499466609005151841129786876538149535016024126650514145353589468637310440093340153886917874349448805981614088094368748254486303678833794877831200877428574770231275643824123076541328968195282415078209956203192741927497452066679 / 23063381783327371892238503898197720199032158172201233345495894194245380511561490584981331072793554451011224689190665770179891100679132938240000000000000000000000000000000000000000000000000000000000000000 :: 495214395915732406255070182325173079785999005868854442306311870315282044864998915741229346907389402153308770208095396470730824982777071312797533998819439772067585894552487544440427484330153174013678973617717992636614924327531638087 / 7563822870921389063987414246564711117790139012321790305393236255848437611402936072761220618330088007887793953499039335353519515369472000000000000000000000000000000000000000000000000000000000000000 :: 410236116706100199449225199271997728795649055931288766410763416591419341156348096213533662785732238743318571704094564935229807561468051710469955957377540764821994055787803798097885137517117430171866060843504350893416069508175894438921306457 / 4489671653821061728355762092182489532078260124188506757923200736479767406250636833876365782170478599796851739495782936595018800932204545310720000000000000000000000000000000000000000000000000000000000000000 :: y; have y := 37581661962145561892835469617509337956571403453465407708593513719214763965326404298770224679000244455185740184714232960031977163900514847991527984798283197417539243968002231492243571730240962742026208554225579291437238743942604888967785751 / 7263700158497843917855470018985164774239397015088965805893298302137676552600317837141747362967225999399495119164404215779640200551924823490560000000000000000000000000000000000000000000000000000000000000000 :: 119762530372716182202880696264612658605160087314621779958088607608776175958009049496118533150180003753259678561093577097943122228476365657616387519748654477671694700273954139277903947335629183336324545239311931223936173208014542847211477 / 13254050861923734057264454494786213494661375321264477960531721831725522172268493774793507214683493689394983286540883445286793629699722444800000000000000000000000000000000000000000000000000000000000000000 :: 19478317042780078106218759245856310668909098155277885372406172552230729431854648739959646545779410683238070208361976333068188991423104474135859810304245337913157554439011819529642912994731777199250956998087125195028063105292879460608199 / 1767206781589831207635260599304828465954850042835263728070896244230069622969132503305800961957799158585997771538784459371572483959962992640000000000000000000000000000000000000000000000000000000000000000 :: 335029290753237251384390630335975080845461111158088301995234730607996989313453261656729475775271309961123232254660463607536677345854542716681244134155030003714229434704554833479431307736850398119641501465585151046113879402085178109598693 / 23388218146472827834382708178454026117328385752091391561629639182896723899048272142516279397762477753138143346784900499337354355618275655680000000000000000000000000000000000000000000000000000000000000000 :: 120276047452382013312620835792849198991538707324177419231866573279212153395622035928912702932561226872884157751847983585057315584381602611353875194457298394044726284187982973451786898095043269661462571809296717063316102893124302849727 / 6385571026521521978808529717451954709863956794346029731060149030641624653908337861990247378347964439335131965813132644522393799313326080000000000000000000000000000000000000000000000000000000000000000 :: y; 48379187480599997023063625011641604321780255247278697528142472313576093398759572147180431580870149382259124321811966828095098356716108035645626395839199669572848620333655818832385496504095959268199221169713366229805208275679842944220405351607 / 2656152587330538598461282624499736242621114843267752263096120039088625477047884834528588981701038340647029352506670913712587405655347555410137579520000000000000000000000000000000000000000000000000000000000000000 :: 229533792935946322397755568630638837128357223446497761731791003111655735077740922197947559420754281360561459469460906377853298058868766935587926267042517934554382563398950478587538783661648189444647302662881273525253536520131727189073013122567718237 / 3920636738558611426052589147700784301853985643503300915969625472259418712049160239745813213794878564634090889496717673719364501372203826627737805861683200000000000000000000000000000000000000000000000000000000000000000 :: 189108438359167716363528193621199922504816657132953876928644400230412297708220981566999788874992772892578290393749361938723060043900762728235624020015665324845349723936991334049264975087115214294887251083846508033076814121411538281429607335266630423 / 1004931367017610252090693496962907498664265374891990364133109971795051005197874306227384561068219620148996828989407435572247060252218612675925630636785664000000000000000000000000000000000000000000000000000000000000000 :: 3801079611019271098906948242318916198434046080194928928638087402185397536308981477630065627109379823292813537161890701629248375558851588529804182956036321385833311060981707464432064639064110022931668188652244777519403264910169029103756620794440327972271 / 6284170815083456109740470001008048224980539477657913077045714356958385619170707328275244788546600024665060170613761163778451616777207057933454943582033018880000000000000000000000000000000000000000000000000000000000000000 :: 6749408903764082408215887794171593341453966822440983141027306135786861436214023016947924990606741619973480472622307581941884912622783519559156828801043214787246633323381005926735189304870120732467050438974431084493408336080779204427240239291468825633 / 3471540831644884060978645964392683317703388649109144945936806423826040925645003111179861184743265839157583229467704029471873519443663328212935423746375680000000000000000000000000000000000000000000000000000000000000000 :: y; have y := have y := 13578387956601762898908890579231037845301939936841841789781320895686663584825004373826253029351094054009555545620158100072572717044131675554555538218666577608874309852307946614835777555639626277489512023505200218065687943126507087271321257 / 255779099191831728240519971530825238350766510563910852435137565664893805160978100447853883447165429323075005562591683347292657116217917152782450688000000000000000000000000000000000000000000000000000000000000000 :: 874688918621840416605992902469634299516027360182849929462923072615483728968185193664864978720685072304221557104948727947752345117038537669830580949694392163168091550802057708808697962684797790885771233733864328879639498723697467338997 / 5126087167187618848552100023600585080339617637681267995850533288338999978103259195355215990513581813304752014111610539659665675745988926504960000000000000000000000000000000000000000000000000000000000000000 :: 244410983218831732182412603813948542544965800792069933433963862083949461895135972599503720104064391411607537068560880279298396260738745963821328187937852584900246787729401037880058303889236600460961780631542122819319873056439929838812185139133 / 445624030591991277645705905955926637482224320626902462909217447736170540547126290558038765827950436865090676357937510542838762620255215661736536309760000000000000000000000000000000000000000000000000000000000000000 :: 559793928178120375211473328114657875442920478082442793228745429669271344913170683143711399324974133808473145740701213801458527294793083661571739216168450308889590215894337056503233961529715613004943436292402181077614764608350943199976489 / 317534991091651429574899703749984959191792251107682131944826041702818721438588850705082171457042975963052485537678005157743604890971913762897920000000000000000000000000000000000000000000000000000000000000000 :: 10113557926296485469630788993847081114721883948793486496128824200698271620951246365689620574560351413316964848168932365462666184235043015444470378678046987361306432905468849390683888418592734152797809334280195528740657804132697407496727250587163 / 1784772618054258808042060946459496724322165350556789429991450722989311385895003891685835976547193576001180537750309109913591774683423188142025259089920000000000000000000000000000000000000000000000000000000000000000 :: y; 110443957864310188676398329634908742441092426715942828971906644574054725734021834260076261511881778317843614195428240182171863124593665695899135381792272526856018802338634969768061240579191461895581800220884230082362299324207 / 713807641035068914784184063145715468397454493222838336974273133732600166248313417390373479397380653746118220741276598513819285968650240000000000000000000000000000000000000000000000000000000000000000 :: 14551598890391121071471304165689757887628452364970594056535403199815782047210433031895007028728627844618584439224423855096394675012149268198930180105248869967737536567872328795752415162028254012998451457636097494701262526442016853949 / 29259403490612095858352575258780764478892698149900077135577640315579520374618115966881843144586271425445633539117372539040560823426554527744000000000000000000000000000000000000000000000000000000000000000000 :: 74136154677342962145955889613143479351232628099905718857633681843203578875952423363054870324493533294800066033966140747067550298403048531868048431202475472321640708715046277926642589987948492648673816218803645444703493671613031 / 46376752150901795051700513631295175687994138152769202475528709961002925664059576789509520130731103402768704569615947065590024733731061760000000000000000000000000000000000000000000000000000000000000000 :: 419086048043264286982249759541152307593767724972639204258775356184874051376114538845147753106056927982807176303873151622997771338296530970991900477411253927259801028455780731766531340648838703547363048547590460943631269648834619669617 / 81562212752497362321594378676921313249606667909410348353041315581917667462046588153014631201264486391286672692152960251049954437569488888004608000000000000000000000000000000000000000000000000000000000000000 :: 99454748714744808406802442085884634288029604025497596287293371398305718928389038627269521372297894627840958289951454054641429660105930211576572718021141406770057751062538185094239470717361215975225961213751241447028581843450930593455237 / 6021807150482889835086868555052299943403795779978356067458373747441085498192892379058393666799825761426339416674377761818812556485229925860638720000000000000000000000000000000000000000000000000000000000000000 :: y; have y := 12475650626192661252525449693092569616482838632368659844065276842745264848046697813453695847514356833520780650040526114114889713934739482805103625539972744356155947849681198583193902913393260076348993086690788214888638581 / 27664627415724339154709143312171696684927459330138799897699461429267352452655654776176073015057219159609127103873733187004226433187840000000000000000000000000000000000000000000000000000000000000000 :: 324145776828817101330268476670421027329102291336520580885987552534841558926309327278506624951005331768468631430405614442361877346828885782016613328084655930893344655186413104974133239861287184452045838340059363451394291 / 223623536372378387462644999203443375148811703930219231829898357348504826546481807711807513040677310681329010337614980004075850956800000000000000000000000000000000000000000000000000000000000000000 :: 3641541263861641867803121021757310495326620672114096201160247556689692534318543632403902471781617911647190433395763599970153608868112797175914041132916735343609479307324631558767462096887860611009329167671826828616921150403 / 781588032213617365668179039882616583819211823957795283596265865244886642266019219622415900677652606166974978358090335805813099950243840000000000000000000000000000000000000000000000000000000000000000 :: 1355730606368077310497925740715510886674280302126301927823477267790932619706942230586779360403354340975270256371691904436008541145410372229727039372460855388534744826284362708848099057988751243870422802050772935648514490427 / 90527721099369175564003967278035751672726642028092784818126383408094646026898754712820490033210140308456154908489193123687447207608320000000000000000000000000000000000000000000000000000000000000000 :: 6467377284618276020705729083707544301281855841589338587207943468696666158662859825843213531397610480058322511193538084496585199990675568504603392674514634061173924216900629326037956142057114705536790291010771448909507099177629 / 134354403783422889145496519045421877709201164974030966438876919816436573148756654949967647092487981035209541761253241250696452760632138137600000000000000000000000000000000000000000000000000000000000000 :: y; 65623333260536481427599153737521130604705538091937346326883865163141745547929218695011702174882213592833551103703654350938741063713568020358628703711800263849510731913830914247361589008658858403624517090433 / 49927784844771555058085277190303447047183852109751669453481054523214736034910393260017561172179283499320119390580129136640000000000000000000000000000000000000000000000000000000000000000 :: 14439410446982214584344008901414669512291544020617506911509589782998037376011899168752473131205152748407245306271266882909054453876797376749218954977443717060871539789721522039172283658419799050836653136597357307323 / 3417818494217199546674441590528748140442261920297556872838714422839750326806439349108884554256214174973998609710816479279683993600000000000000000000000000000000000000000000000000000000000000000 :: 282363038009733203341469705172962529601412902180293311710456107141731992082924825113677972444618891598177443275012642154893986556558101487857306128657782677980117258185279594386010473923459276740272576158447253 / 20793275208862682396921249095673493637258262409609685482291350071242870514895834567754907636546820847019832831019672120852480000000000000000000000000000000000000000000000000000000000000000 :: 150672109011988613562673306779802877520260268584387545941605454865466171459383380228726088050854759751383413992296232274649853199272113120073381135502003408596217987129360161692457180600031981375170016924762654737091 / 3451941641824521023629967416392320183068255517569448744999100943647490185141704927151517540144118406672611800339169236399706603520000000000000000000000000000000000000000000000000000000000000000 :: 6973922872263771068332729444975914499619801445974237016686162139042920150146733026454233809658424841893654234254523021696478858771125483055769307048376089828848737931139727318726366533599443105366404211418432659509 / 49707650899099816406008139441146049480596043452730169194016904415204509569707819846510756237974448071936094793860472653393952768000000000000000000000000000000000000000000000000000000000000000 :: y; 114974217156432617195925414608974800570730504314043909178350211780401834000739760542118896322527577033749722849275972835967331733664271152592863359782208711379613754495945009974039935473073543 / 10297439621279212621647469762122205944565192755633276433074331310896654765097485036973373722827614957463362600960000000000000000000000000000000000000000000000000000000000000000 :: 23880144903998590099801747861147279454165882439296904749175108259161040139549176688343921455326491881404008182164013360945237412239068746125378752192381962499555897339250807244633898105021225612139 / 665397665127904321360589168317754454346814833218454249157634235240562060576677044233581691360847528295821461579366400000000000000000000000000000000000000000000000000000000000000000 :: 4632858293923510096365082508842047093162609621067008954349189048013181960206285777266705057780926804394532648112524844307299723868767126441927817054089984455094235773745752844067373022715711 / 40161400896068125190329162536773776068052799088852413455743473102471696267857163560909394597670414781450813440000000000000000000000000000000000000000000000000000000000000000 :: 17193704331149671933414226143246851801794793374897368551078077786526142766996854237600257673697310967973541991182210114838833504215330854535760805058524134878710845614697955804681777615651768144695679 / 46370823952024621150817947374321732640702473710512722785740910260320058265965760238144715202391507749682135633619845120000000000000000000000000000000000000000000000000000000000000000 :: 3079469432450792811335246298578983238701434635298980982110706206019314534449525419803103113305221285091475876869147112911183346274834192066293616652067453401314831163451714848345835547670861497370039 / 2583846906779481377558014978071658734208297042575833309454219875201913694421972709787168210282511874609153826350956544000000000000000000000000000000000000000000000000000000000000000 :: y; have y := 34122292012717521974348693167123037496580220894920186441802204056556100011487990072622253544016823148537220706005437359602971022453506924197363114237773836660405164854954787358849353749 / 1048550567965987429440367822157498293988526720751915555151071264106201677696370770856755185672180679110819840000000000000000000000000000000000000000000000000000000000000000 :: 9670024200381681223278145177287264962198939525210070967064936595996836833046380809012326221196217976633011341859079490573241554458732860686290582256766874919303891190211505172484268071 / 92447307459687788980194908433811802480253001388795376107531945950543633023170166836668383395746139602944000000000000000000000000000000000000000000000000000000000000000000 :: 122840251501806404594062471334007107165757165326346318081652581939845084340986919681987733442549545337297586433143276640087584713660110646845456253772933191866622983254194139444240018394117 / 365361620126815175413888165587323849994224421808667464550417720470783162361757637489642695807550956632392335360000000000000000000000000000000000000000000000000000000000000000 :: 180265271605279543578686720939114664336782594160896432087998567207859739388779041422657937960414457933345909516833801142718450610636297097946098814684339766910381053023000323068929 / 166805288814276649517710430770068226121432054187630636647270136733738698824078980948560392324005232640000000000000000000000000000000000000000000000000000000000000000 :: 13491607289270841867103798577353981264405566717962556822206097508560747358094348375269932825143725638595420144341485153285594187712199599343649947142530433514313457797722335384530334123290267 / 3883979799043025051179502668752025740955551819633834470610542275919918634462616783618710149330439999997228351488000000000000000000000000000000000000000000000000000000000000000 :: y; 538461270721350642169627584355915419200351299430306339817931722822792570509560215487139597845611659392675171902150311008134113222185371379992801424507434031667926490311907 / 5677120429228608865815427498823155087900257887797699314956411994528871664716525760304127714900920000000000000000000000000000000000000000000000000000000000000000 :: 3037953163704168160535495530641437605715960462097551605484767062374787786792078450451987141009839652156676005325179918133327035874895442413801737972105449117305039282793740729031 / 9964836961326857301936484234218943566652134609514989180850686477547502480445366740712859890107539867200000000000000000000000000000000000000000000000000000000000000000 :: 4265182981475324142651640866389786174308752022760958875990159891844496140080808284823232868980172998502641004305622639892194873087388119725752006388606402138120559251567421 / 4352535257490253418291729830517093662977793500832719584909243728778544847638705191935998711710208000000000000000000000000000000000000000000000000000000000000000 :: 1053157150081772033875479736961019548215406556444910795030746649991896261710560418100757858528239612779898809713983898150567863267470564120555136742407269793416162262345185886066493 / 334359237234052113979709126963487976399402653300993480596642622482844922734812108053812240329139247165440000000000000000000000000000000000000000000000000000000000000000 :: 178934846521040075849321636512645895289595281681268388237350648514912032266619213489241234931593717632264356495619429026910084079537970837356209049302570105040403736964341975493 / 17673826575741385557589857067257462304316155301207636189345227582952266625884144895095885658652180480000000000000000000000000000000000000000000000000000000000000000 :: y; 2657394390583131009906136039847614726666276500834519187943325595407759114124607056852900360638359304097788558784159449766818575718662588033591571803833121569 / 3299773054510788438146234843787509509983207219445839817589525740967522230636214338434582584400214254856109619140625000000000000000000000000000000000000 :: 25552610019154071507537380028946971156203245262240638848657506810515540672779121084814552189696857745858556925104305360559265410805548316942982410405265967865301 / 9868712572881830465157348150202760325799052779780340648663399013131273732088249143179137132127945125102996826171875000000000000000000000000000000000000000 :: 2219236931714485289958122272275067952818935218693023839101327188482495859651868426020106270670724709310752022153872407428169095732547063217722235771154690791 / 266620222115423633128131386356392989195917664462582396646706344930974290738890762294410038182735443115234375000000000000000000000000000000000000000000 :: 13227788216355981200194850789838763683279778275496301571474799720442669675389535238837722285784154450222416043392262178563014516369010436090688193683513871509589 / 494390095991957540442686674916445067305123424771229122819047173356345617716699646958187774524578094482421875000000000000000000000000000000000000000000000 :: 41381627366442897959950426903126685999870548484208555377792420054658766667687147728996008252555308323267291662433488189791426233497441136294434936307004728055837 / 481166947656471526178459470950354112173022724911910935516403788159340631798625114110593554430694580078125000000000000000000000000000000000000000000000000 :: y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q1_eq (y : ℝ) : s3eval s3q1 y = (s3eval s3pCoeffs (1 / 3 + y) + (1 / 3 + y) / 10 ^ 9) * (-8 / (3 - 1 / 3) * ∑ k ∈ Finset.range 64, (y / (3 - 1 / 3)) ^ k + 360 / (29 - 45 * (1 / 3)) * (∑ k ∈ Finset.range 64, (45 * y / (29 - 45 * (1 / 3))) ^ k + 5 / 2 * (3 / 5) ^ 64))

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q2 : List ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q2 = 46680056272459144415657249931714061178414199850964399327421963404543275656529017031942387843510251154135104816547534833767801389 / 2202748130928455226645306448691320211017468065548913868800000000000000000000000000000000000000000000000000000000000000000000000 :: 3490601599273310819542666420930246517983766575217071586183997955676864499184165180924353542658471194637802686239786133158560548323 / 12935338913143681025727321220894312138172501148523089100800000000000000000000000000000000000000000000000000000000000000000000000 :: 69518684226091478103203436664884244453051029095472752834810107046315837945289044464552379782488558507946317024827973806329947481 / 32017550877813239274880265485957601404404574842824350142300160000000000000000000000000000000000000000000000000000000000000000 :: 108802469502239233258014543346865270294633785981012520015903583066469517388631380539213625507912596770529744542874069889199205929 / 6995431284228102698713335316259644004323688621121286585712640000000000000000000000000000000000000000000000000000000000000000 :: 293702608052952753400836869495813636474338968836990969554209754171392425487507125710980191335460416271430285527454374392827797660591 / 2705483049175218718727382433563417318672186574218657587024363520000000000000000000000000000000000000000000000000000000000000000 :: 1112873113867465646006416339329608344038484547438297673491864853084173734697157809354247737119164488506824448089703201711751407228871 / 1477784858793186695103192085559849795913379221211871791231795200000000000000000000000000000000000000000000000000000000000000000 :: 1713350979596976508094121203381721626701917259340051702199566722868931747544811619693602776142812847221426101041897762945021582492821 / 328467410424290203638597436258776958947988168852696215666032640000000000000000000000000000000000000000000000000000000000000000 :: 228818566045903271168120203149135832076727831360251485956825481552689623119293570670813176690355350675390327125857759849194348650983 / 6335505863420815613202421675789310388365324413617613716848640000000000000000000000000000000000000000000000000000000000000000 :: 80506495976515858616141044554327934237963005218956806228622810647939598733103357854243795816067016853482363413707763640474303781599063139 / 321963755697889257606553207020853175160818003109412830595845193728000000000000000000000000000000000000000000000000000000000000000 :: have y := 15411469250980736738458304492538542625871464336384297962709194161761691570852019499989164943562196590712543649567956221431080841611596356285172821 / 559783154420440507595081379180170003598205168694563129119152971841280000000000000000000000000000000000000000000000000000000000000000 :: 1558355547096354503322225153260907416186181842160810564531190305259026150595425416702350009066526257300964211478185592888753237194149402723498463343 / 8176043125689592679137092827256817089506189916422950365216775534387200000000000000000000000000000000000000000000000000000000000000000 :: 503458313454464284210840362545972879640145432337485978172172529314108944978899222784566002678694253485906878102836282671676563010635791000608295840961 / 381540795961674128449434309948322153196290716302297606485246147881768960000000000000000000000000000000000000000000000000000000000000000 :: 41223015300516506745109908828252033505443202939326239546295807126282106869321371018075832861774682433102447354786634102215104335417951133540401032186473 / 4512508812388822586849324583073013135171167644688076203017234515924981760000000000000000000000000000000000000000000000000000000000000000 :: 822399155304983168138650305588088761480793258757010477359008400177783058190519560449349545832819412142080996418059385236087809184937285462421845784530083 / 13003546227700457087770803673555399517851581429442806258361330796723822438400000000000000000000000000000000000000000000000000000000000000 :: have y := have y := 26159858976454938064662107396973163380576705637041267119126859784184251530900423082108321952142491752087740818745733122817365781559910459107653813141070511938516469247930767117371917 / 14853473805186940761887940916375046165382033236684533735187520111151315611140177251244563798828125000000000000000000000000000000000000000000000000000000 :: 90902984860268124549466172405083608241263806903278416952880462590414251449989253452507083363202100936487121447724156342269488814201179349195607360445262456621480667721785473673861797 / 7455411562449043625658039842195969117759321701810769828472500441890621735321324489041672949218750000000000000000000000000000000000000000000000000000000 :: 4606409950201847789675297423054481326693321151396563557811684833061513245392711690516310354272127513521158832971213471891543292766809944668522601851477607426768646694946175988954991749 / 54570371153838978016501348149290930477164426456514917418406323886621137788754129466528940913085937500000000000000000000000000000000000000000000000000000 :: 1362181228131117846375820408724155078618016956335690810237790554328607641778734093661166736048133442756379445819018710299446542977662053610449003230644637195005260583832103238827115202479 / 2330934424999693489561986156662569744667451930071137186871927263157102885548212101498879047573242187500000000000000000000000000000000000000000000000000000 :: 27157410560841906430912371973002093694480364959216039209790191227897069487669088583634462173516039181200847071894050271262388807062677743139536681962072179746728600027699602840792130893 / 6712501034018104669308251273933349581162598912546629240675486738838492486863522191025252953454589843750000000000000000000000000000000000000000000000000 :: have y := have y := have y := 9089310227047101296047394084413762274937646125533175327222246203579384126131175215345343492732932831418258990989928247527878044615950477148890233141295003951967419738496861741122091489095664968946116095357058423319615127 / 1714658568399459248974312377594727675336938407526662923867383794640634850859445003461041899867756858222789825351117798390987445600330829620361328125000000000000000 :: 912415559084910879095356025849210598123985905012278391044707617218701950081779672979776313162554274112202556037824490032348148528349273056971026592542740034750973941952170644551250561672534678080662032384485933704523803 / 91796638018259880652034812886227232311125289665744265867272567065853826019476156538166377108605345051664004881963876414374681189656257629394531250000000000000000 :: 114809646866887624318726420952885920665970796630737601569354621930075285695194874892575311365152338651200036414526999620010364382162586451900490876538400104017820798665492749798491326879806701002409370724006412713142290321 / 6132570717122467888077983264363918360355796457541533663114207590879782540753278182235066125125111251299212413636174900943842658307403326034545898437500000000000000 :: 1436849892145236339239063672334450787394628794518346052259078604952420001707557724247456916508822962948606599164975957639118628960213221031611205571159169061927679470482318291218189260271980940192283598789555389675881873481 / 40597063163575432218362395998933993489595159354675401579801292784873854557113330229004080276280713849098406159048524344257202756125479936599731445312500000000000000 :: 9544317592954830811372709964306570778231898047274354665660817593053490934072353856770967629277984531376963481335934192284302753189464203487012403834092682678728341250480142852750948713084036799002774811640149040746663087 / 142234916534822863615089943875627989314892740104112719237267998323627768889541364089924629366915422088238569163924954977945569467578934563789516687393188476562500 :: have y := have y := have y := have y := [382191103621120321177504245043438330509994107385900070165936887543985002372206379122698986096529431970104949489226301030987507356078432588892811296793684737649311017618535825453088768 / 802727349353387484651909080527547223826620653435634216733368065448460246541205012648680094944353413666249252855777740478515625, 751280549961333466322566134197630760604064517426617536874115040936860586938406076282499265590931664085007029200943002588706709036423798695319990849390844648843793942462018892070912 / 18668077891939243829114164663431330786665596591526377133334141056940935966074535177876281277775660782936029136180877685546875, 47183778127564302794164375019337663277278683847215916642773401738229513413536150676811498970441806232883585730452897188870575821402285671333927296651741431271707515313971657703424 / 18668077891939243829114164663431330786665596591526377133334141056940935966074535177876281277775660782936029136180877685546875, 467710299141584910548990558128653057577444084128070084567124656651712633070871988359409444471867368010776339842971204697753856153168790770536951402265140085471120116445872128 / 4460711563187393985451413300700437463958326545167593102349854493892696766087105179898752993494781549088656902313232421875, 1022635498655140929041915889616657398826349601613283731458503653805047761693458538845342799489083548217208216565112001455169668724022504213841400213274536153224442370064384 / 474543783317807870792703542627706113187056015443360968335090903605606038945436721265824786541998037137091159820556640625]; 222626363356055044989045684965161341198111364077478247434786168841531884518710154030825073469728891527222923838787039781621172831599172928161988683214848711722500949551109637382248569639354236928 / 34385316475962807824817647780845687663967053755134640846280245171372783669803153393068940210479389474329536824370734393596649169921875 :: 856070484819212327884593473261552693618865376103632507742473173228101404881011517341533796979312299346465431788710567362999130650480638517361916004231445717931922160363424561258123792127885312 / 662574204520213572704127432321943483225943228504255537901745588019807791644047474019268615351430096183094065054319798946380615234375 :: 13960405997272156225850159454627396178483226634429932190891439767592628116423344031250140224475527205077160174288581000777694786637550477917463976588491597938339556764080517274851786111320064 / 61512194053600729561391140931745416214610114052119214394061261487250060232205998914255706995490857735831013997085392475128173828125 :: 9792399552475185816527058244756577110474739496782164684803533299202103887119291910784615361923450951248438229942787186471143358169810402822863490421998942553517310245342608949321920413696 / 283466332044242993370466087243066434168710203005157670018715490724654655447953912047261322559865703851755824871361255645751953125 :: 2226290900604141900345066929221292332292976814921516329473849040774794516874038685320774991389280450748926325247232269597219066205878076372800916601343723518184190293699553227721146368 / 498735927113051395789647653582203896460326441483678063650909153089280034833293055195925502776077564703882671892642974853515625 :: y; have y := 53796103786068389888051638559602618925571914848990671177116129882245257997198697346753016659072220246570467690280268424258571141951077302648538654558177229175400903492175424417578815621883108313160916926464 / 12429964592233020338703895233586490220423216630096477539284092887797474999106087095377273262846435741661721419148989298264496028423309326171875 :: 3015432149141420333639030006858627343308151422903202002042147404560500807659124366178241154751957793699961552798514544916296450983713245944967146185566737863517376191714756588491394881667771274120751218688 / 2134438364322841876343093120918892260072673562743839577452824031237950252371752329509228742104943511194437011369018364348448812961578369140625 :: 1298022412061660151992479770873419236708098632790113084147306575018697666889104463270588082060570153003304825870390175173937028854285425667956638371704724054828889855230324763666899772567097573686378496 / 3062321900032771702070434893714336097665241840378535979128872354717288740848999038033326746205083947194314220041633234359323978424072265625 :: 5606756419336551008018807911447161970936466433643247126856337532754427404778305461727362739347909912803208220186283999359291738411503146277857812636065754637364357725148603049208660311800668240216064 / 48247889064464429040961439474646629898340232888262383359769073243923918993913793926382349106104195646249621631795889697968959808349609375 :: 932616121367953285631872489060841718342167947838396044181318004085220669374269682353425638163899957447506413826622737813953060159286513002629478259885591236236710480156852456391913330746528366592 / 32256902062168292355332519731463037999157762440338756450479719416753800382670732287780182589477517840492737377644516527652740478515625 :: y; 10535187344764495293425602746312079047936833271407629398433505260200073566635049511370778799114727013954622775238161064389759862226184496848877506629839985648237996489883505938628956904406141565447243003437514752 / 27348831243561890771185287446817288089025218190104400825849092119574993343245948353618280965621548222999580290970556006868719123303890228271484375 :: 1941932600519692302933997611412264758859409757433520815713648991233913880722959186337036305799191971019874002883770975297176094076569516645341602567607493738219761129929897863307042796850314369719961425964695552 / 10801639230650494674333684957986660001547775251553838981637876719496005774223189685882850465413552659504035913240471700191847048699855804443359375 :: 17069170075806314918530591950718453848467779767139784720465087477560964879171780722180678149065175638218372634501691177417879795853460343126009579452909401600296347879298260224856044308014053034199044812234031104 / 217014751815796302093431306883186532758368939144854401358360977728056116009393174598191813896035921613671994256922204158399836160242557525634765625 :: 19799715642249475622887733853499755398825418253396464192268392885326837144592312218068654705411460002049648516029956586452303871385907147584200471864232040466284363926665644802978721107605648598834478055424 / 615653418674864330255553431632183528158892861302584153983350055257680579893028765225582813645685532032147957437473451136611402034759521484375 :: 73946244269171019719061341738902131404623340379632337536650444028756036404345077426499885481635629024692206276179640447587709684442851599538183272509609186769910204204563038899811272357152714387529763127296 / 6037411373370324164513320542027723821348419506046860519080845116930202142422956589183247013382554503092836117872366230585612356662750244140625 :: y; have y := have y := 59128138914829739853295145785864029715117511046281110462401483324486799522375210337761006560406901482922412426857185633421738453700515744726141084320075148736643128009586061137821269758858335015994668095160834196504576 / 8214335622193922125242730561344030142863245410105486012585616706312547592509788295307434945149123338364174971674980252345221742871217429637908935546875 :: 77704927872972342143451289563082153144513312538382102360951577609076531728032152491633970783647558991116487186534891586628730757563250022156154756806697959653889375562571342970369049192246765802619426563765778109169664 / 17359260399382256738648293427555571355187421867895916858195323486518433399725217028233899568713793411325638595989195867019816432730294764041900634765625 :: 36879722848530511951951586986287378325926198069870884888187217524958986185133069659887565467769379784304703810677811978278700418466645573210346250960747443914887868098394267867469490137162646613219397820909355008 / 13974148655037353250012109910682042659345023926835386095125924427320007470148881761456834518192358335722004503143267584164277650415897369384765625 :: 350149412671378355769209855879061250091187139299009441539027586977297774933450344377309734251117745660466905155608479055681550614897347391795128624825932932097423432783707683303025140290866641375492736059210482057216 / 237798087662770640255456074350076319934074272162957765180757855979704567119523520934710952996079361798981350629988984479723512777127325534820556640625 :: 29930445030778421198615974891498941030270143344044197599044953492588921490594157562358910400475107995352568609793394061239146187954921473309238221962880959840219347312312894782481761855921202562942690635989123072 / 38577282966608909551191731992809500005527768755549424934420988283914306336511391735295894519334116641085842547287398929256596602499485015869140625 :: y; 1607971957797141484890520775649999822682966176226247812273087910171524424468562969119779013228436523271732163937350000643905901699275512803614110690290729682688384386021632943195358565357532950146885932428257934717598453202944 / 43683762909806678116741713940652500203475453321732283665556196373619771284038721566350281271388531571310637221792799907149618121593448449857532978057861328125 :: 1274871238436697856742522835560610448637372124952583353342749373999915786215569183042364700894976579239286697779604007179026086628178118812494400677329117071844314948490891649348448989162776421612627031515085959097828975312896 / 43683762909806678116741713940652500203475453321732283665556196373619771284038721566350281271388531571310637221792799907149618121593448449857532978057861328125 :: 14411316906505530200386316741119305338412880573361079869373500360157192573196400384617870646881894002925862465007979760280480847640493040964079080498822077566650163163116667173809383019509994162086115605788444178284441239552 / 651996461340398180846891252845559704529484377936302741276958154830145840060279426363437033901321366735979660026758207569397285396917141042649745941162109375 :: 612515321413246097583207303073259161932366199581167513723644706356524141923739136638224657095790441357139720141885417522617419444380018799372154685584864033790054515213709698580469094366273235037854455403640253770306158592 / 38352733020023422402758308990915276737028492819782514192762244401773284709428201550790413758901256866822332942750482798199840317465714178979396820068359375 :: 42112422746412726925137450704559026620959139858418580067118950689167534331663194491678575406777633984078224695170598493245731919671834779468206529221810364500808901385933986271786375991411516630063770163852456245155856384 / 3830766517863679088407116644215979462570413501388382733707157196416838073209632352311615945366165491985779436114913087951805437114671804010868072509765625 :: y; have y := 5096190536540192402327899073775658557567546329372429670476389599568488684544648213905657103772996128770215667502804063792823316390031265630308768038222695497017821489554644096839744982161442308971850145298981361187397564350070784 / 82605995662444428318758581061773877884772082231395748411566767342514987498117222481968381884195713201348414986410184624419927867933211018680594861507415771484375 :: 81791840155109751160623787394688515830891277474433018976311382129148638574217444655678583673119764303607489998446688999960082334973172664091715444481600059629659508818581705293139969381881983512935188663362899448121255167787008 / 1354196650204007021618993132160227506307739052973700793632242087582212909805200368556858719413044478710629753875576797121638161769396901945583522319793701171875 :: 2481991961706426922559604722538666670132617557959028783489127399731860811989732790544288515002440511407307752048607206333174194212959312832767086356653367676063192331476539492264772078474801953191820800668383816931820789825536 / 43683762909806678116741713940652500203475453321732283665556196373619771284038721566350281271388531571310637221792799907149618121593448449857532978057861328125 :: 336227624966411950915442391092194284245576885700130303186131780745298366586206707167548288600518259328764876384396483265322470687394998148555957019647721845596972993608038744248243780358225380945421474583950403559177060352 / 6554202987217806169053520471215678950258882718939577444194478075561856156644969477321872658872997985192893806720600136106469335572910495102405548095703125 :: 345446539007815828459990354124842563830668569401391166936775033282444078687778766499098243857579761417191352535336208162255395234809764608343514471462752682850453597789829985308025828631233674606208125271742870258396258369536 / 7779300244212148157775921660664143871851793057294790241811377436398041461541142196747310363397957677082716217579539709492397747681025066412985324859619140625 :: y; 105102637078981173781898432359370839980842802990417119553829686118717459957798898475328620579302645751012010230688725363920863665656123787924357779199109857514725009500297108646649265386019535327909103832942765869428986751649310572544 / 2685438312990405920214522711737206996156055621260444385111624039537819728576292785666310126673318440462635622793208691955267435058640757006287458352744579315185546875 :: 87017181563651450817344265054278976948807982841339559500597501921884521109988575744150712557315381472872252817901634750719721290045900918368643884718988329035269663228223217315054139159086365164017864491916938636724808731066368 / 1890478760745568955460636738669508137697354269468889899952357883162715656153959667686474003066030959694415883056689401710281916990652462118305265903472900390625 :: 9246141013563852656461599085720305578387776449094458488515724103861840691250754218392249071839520029228429864746003939429417325699170260756845353540179689303408382530931551745520457157151302322568800029093800407428830251188224 / 176793129576929419586740448474149524942298520246714497594236526104582153192694769421130916537131817000630598994754985424371351854233580525033175945281982421875 :: 279487405036382852378487737266218504535812068272241205724641534643554993595523913351725689067003604820669318826356803603233248448125547435017687208268834594899112953544123902200894890286496074504978743837069957665203931774275551232 / 4873753744084221270806756282644658795201552851652349156282439273208384262388916126436134531167547078879556484198200892840775744208059450102155096828937530517578125 :: 37533923558587198559796956093920740733242333389154189143172574785804270515520488670108431671005533894678029924701843692850696544560307791073607551223026886559425410459137845664781243304264129375167513392558347554277416587231232 / 619235349793436494143617549188709729271155039215860182995253128504610101185286525352086820721107295362431896449851458953672622698150007636286318302154541015625 :: y; have y := have y := have y := 29042973546107751827184382351876114330428355742662747990683966795817988381697551351141175817675097045613763063407023632597640153761471911493590778156183671573059687794215435139005801701681271562844220436532991893319664392914688016384 / 2685438312990405920214522711737206996156055621260444385111624039537819728576292785666310126673318440462635622793208691955267435058640757006287458352744579315185546875 :: 518052612799633633783943499852437379031311018495728729974112251523890881651267773012065956178525832082003886635801788438034149991385887690270028521959436843430006530376925929323099828192121886364604928918286373216160933295009996734464 / 34910698068875276962788795252583690950028723076385777006451112513991656471491806213662031646753139726014263096311712995418476655762329841081736958585679531097412109375 :: 69305302854332517178485254982634154874931263163929587925094749092629505274893623858792293956040631507712457021280845101801706502026639103064798058922092510592734924377179433022343345722376898926509797131186389239111165121300267008 / 3501223354615913846433536781925954362654570562269158259597945292748135239343276122120352186014756767226382819808616286773490788863938405484077520668506622314453125 :: 174278853187269746006047572695336546297599099437380265704631481568777927428143672487674829000797578902005987627232453304732194645720386800036286423603851211690653228323666302243043983295827645240077472684588720154217453044216365056 / 6798578007570647899277272687942296192800140813317580721801579846931189186269095659914709181451439089778824361501794156848778316604153815205791033804416656494140625 :: 86438165766709309555638115534886105782387661290418973237858851176453790867465947418039745444598354891983049389504842318040919288645882061592544173895856945995899862740260146282414667246139098273618249532655162729655634397916706111488 / 2685438312990405920214522711737206996156055621260444385111624039537819728576292785666310126673318440462635622793208691955267435058640757006287458352744579315185546875 :: y; 13258934485094742429167728005453984585697712207020361334482087224892050220324549170814764800630006276996460867430410528128234307642463331297094228184010961210867090332035981134470244444056597593056939967894617414341946771374293909504 / 8636950249888062283933194667479125203853259971080888698061709748783798586502130851197051488489862011217665921956536063315589858702114867128329933620989322662353515625 :: 47863569744063009298350313621756271501644485373998963595592411280571221686777553874517934697195533846314536114041890946689803789852462530005659615821800014436476929002258779303841486582047503665502823688283086135047470249611886592 / 20191265511206059550485133170956443580120718956845446504598676989006163372754081095235414486265552183929591148821117984626070940290532007566071115434169769287109375 :: 1146223552885028538059706442733887998300555407593088283879334105794072408091615646954667434822483354351672028762993193009472660254310768442041151283969776147754352416632641474994979037641153514756610609930318685930109140535014540181504 / 319567159245858304505528202696727632542570618929992881828283260705000547700578841494290905074124894415053639112391834342676824771978250083748207543976604938507080078125 :: 42455559802747476674638687297965912075931274592664173003514976174970855899497487948003095349664054588448794577581573322131941023233030526166456752756262350497593454134854011859892599626372675331428331208153796269909096529802559488 / 7997136131597397022675767456036947576402786245564158383298463488796366076760848081198064701230847053194269275739156319104429526678501360947848297655582427978515625 :: 302000964235722911362045405302049094365547636052186048819055467043987266918714997978637402878687968544224551778308681545153261920810865219473754245207784695254093520286740543677920620713084419261488061468343709538529836439731450150912 / 39355561483480086761764556982355619771252539277092719436980697131157702918790497720971786339177942661952418609900472209689264134480080059574902406893670558929443359375 :: y; have y := 1009713649651688443688867922131604122489408446312188089951252960464129797140396788016950543953040515958192468029343860911569842561787515218806984121942480721024680328207052602307272110188485241652275191281268173940268600844877824 / 7357365241069605260861706059553991770290563345919025712634586409692656790619980234702219525132379288938727733680023813576075164544221252072020433843135833740234375 :: 1196327457819700533754834175820606838878090501687056804908047564588308287855441051801587128133451583783103501392132554209639208037220744535716047511859812567959381365577436494696017848194191550610619255889958220141270728683411996672 / 5238805889276365647631609880274223484304436375901522652922676405000008978698013794988375493018440892050059657580194005617652865114397542356527992524206638336181640625 :: 34790208249583532290694628153502502138969268651283493915330993153866943010051670708598762213124381438352097165099783994207591556621409687176780191000276175537801785393418459042799228086735153972818149110950492556741616958105976832 / 92601321137600204145328369370248517108829504181394633969366346190959300985389406402286556092183394498711573199765816963974739139953129551940946839749813079833984375 :: 194950188745344451852630456618289972491765155021246624194363529058716294796252164841324537434841562068714977326418854742495134574639451791425061935711303635561286961097923646315676484066521698897168672554067188412733572190461642145792 / 319567159245858304505528202696727632542570618929992881828283260705000547700578841494290905074124894415053639112391834342676824771978250083748207543976604938507080078125 :: 13103258945741876412225230072949279911280529389224393767772738325355203649563875379819627866939459838004501411268023911946103069139714010452579557235835076018794844088651098757954614907479737900291215304621916107836583516765964730368 / 13427191564952029601072613558686034980780278106302221925558120197689098642881463928331550633366592202313178113966043459776337175293203785031437291763722896575927734375 :: y; 78066493786582858202664879170046731388592204239667855114375298472318745107095148405495983370299232780113124589925265688445083597277814150673371181864467805223416268987431534495102941162761163632463878418113601934474626746146816 / 8084781522651815328902476856243267451174402786196596802901390459812294069890931299979530575913297098566894505335386807566393219115497004167991690337657928466796875 :: 44464300808317769455146217905986676577934446322482163809750402386951808900560381740394754598536222495531954573040876575487115262616762251232694003407975779816039030122963218356009514911440722936020645175134307119103809509628002304 / 2685438312990405920214522711737206996156055621260444385111624039537819728576292785666310126673318440462635622793208691955267435058640757006287458352744579315185546875 :: 8662037681157980354478161001443967045086245001787250177896520918466392099951299999244696038386340142244697780005602533502119124120895706238513074730921161099459238324261799211769808178169655036275616415412284949509381385625550848 / 305805894015175411010074835116485772768010161655495580696921780578947892536439082769656368491985544894788171399418023294427583513854784769137040711939334869384765625 :: 5596136798916821837059857753602898903788303869419378293458515267737144975000890024544226749563415781018440907318661587822428088380959639412344583513661565122018132117126172060745146635056401832596891019115086942586236001352941568 / 115982385610881318813251811470377710797437618193972681084555191076384240769075768151701101816455613707688581715321305632619523773296776880670222453773021697998046875 :: 10040875383164980655768159799619234929025025614046290124430904098451869860747398422479440140510355837250004943429704381802638288327630740363717693991706489496877350575549913783453237546954171418996551728357425419395887078876311191552 / 122910445863791655579049308729510627900988699588458800703185869501923287577145708267034963490048036313482168889381474747183394143068557724518541363067924976348876953125 :: y; have y := have y := 6197558220082923763101605568471256114693649310150528102382280166558542021797614699634246108583828515742133953030662151764257791525715434552137193112515782550001487342325628173511941932381473510656549861422710465948972968579625088 / 9130490264167380128729377219906503786930589112285510909379521734428587077159395471265454430689282697572961117496909552647909279199378573821377358399331569671630859375 :: 364413001537538954979829377897814856792784265065561584431575277017767772846428079184086237523677551226812441623824476658496780880378966096309286858548556039782994746847516364456914902559581080399475215939254762962751558533880508688 / 319567159245858304505528202696727632542570618929992881828283260705000547700578841494290905074124894415053639112391834342676824771978250083748207543976604938507080078125 :: 92863772354595504810216497965680489897632708670402786946146125315295668674118876055690940637156402235378386622239604547852745377088697450581940017824927301162582960912603001541869769758156506100787131575985576407144462148064256 / 48105849653147419013326539620160715421130606492547475813379988063375063630976793842283743048942479966137835181754001857997414537404523571240133605897426605224609375 :: 1051143030726751034322299408666542931790946005503430027694464484430099877684279087474590079942830997124099061590683073523087511595234806394658976933741429368036898292755071535805974696419599466233023378028803910941594692039441288192 / 319567159245858304505528202696727632542570618929992881828283260705000547700578841494290905074124894415053639112391834342676824771978250083748207543976604938507080078125 :: 75592621681929492813740213494311197329994433487676307579696972033037599484396645980850495613734498322256212632849074102633622115849841718628324284847334562156742121253721961590000277755241726825220165897956358110214627182692040704 / 13427191564952029601072613558686034980780278106302221925558120197689098642881463928331550633366592202313178113966043459776337175293203785031437291763722896575927734375 :: y; 3347116678098295191124691956461744480618037079639844526097910462918220647915395630063275911424930727053069204128764286698360599934137070162000632574077348904814627424731060230875402398284362613271625354218814131899107787100586651 / 63668552799941118139032438851455313763270774652718888333604327803295128277509960757483245455381205017558579440016763930341742866447773963045619893819093704223632812500 :: 2454534347833788224502253265383510754285890588053642737533476052071491797708132276557834499971977063698737826770620621567548687617137475649734021743579349654510684011515707489869342688439198597998437489813463141015547333443826 / 27718549678710929352548200424731341186795959660854617211231092089947137453428644417927912661473232233069098717355523839246840556160833557441947050392627716064453125 :: 78001924615466319695567398174957284170539452424953417607726964425429703476106802632056567577171353190638265072403799841215597307712646860786690864543198573624823018056825929693199776610685212139024756435230992153995180899026041 / 528210180571666619017401987928475425690199370132219639385592166454546359835667506602133727395247759363725023326267494781284007887567355510327615775167942047119140625 :: 47611267470938735193097977399941336253180525402549454538719784791854433496716028299050757511845905266396873630822531274200645868831753649548317708458197704063037292104001601912289445793008175634007880132164039746457731791764676 / 194265750301433619760199515317159655041076364091181083178287696477203980365093520665222434695516653139850236542487437290381048493603799443008028902113437652587890625 :: 650195024209105024926201263537984190909625994731094138736529187097738794708724031502385127352732555134802112613609346388589981422089921913228369347062267776387231836117024555842361061260651148679482195087290272052670304208191109932 / 1597835796229291522527641013483638162712853094649964409141416303525002738502894207471454525370624472075268195561959171713384123859891250418741037719883024692535400390625 :: y; have y := 4040018001325310574907058654320764227699526097627826151622499960688868986193958795871167602341133469676132186061215982558988614525228058799855579130125527992227467179935914651762234766462221153408393912373838397637734669 / 1335360207926560065110580103751122173227649889799673241886887500934343343936782092410454285145302930713226150150514659475931011911598034203052520751953125000000 :: 20720962705631521460131975534771050367338579575299656393553504822732058456206682094648605011470966105967395587410507694682098551709029640314126743185706004656604810853187943928406293514043113792859504231545284821295879217541 / 3737879654482352974525110515053110943103531581628867962223718793376241024447197893212210020146459664872034116188222012400199645298926043324172496795654296875000000 :: 759477332024900597533686316160413283782650771457867513400439209876978053936789049593507659809716242671236308953361938810573347842945232385329248900348245562748825634584656785963609892085621643583922421879092963418451477370427 / 75992428332645693955300684310499407298631619744365467410566140111765185827377407168251805498870434436728765022862335019957630288800487505795899778604507446289062500 :: 62758860621130548221993110193833293302715908722007207903444984841044910398466979972671912196632063068463215447463802756419391784405420799005375423698914188518043986676306086917676459221859829003656233407542859488262934575041777 / 3546313322190132384580698601156639007269475588070388479159753205215708671944279001185084256613953607047342367733575634264689413477356083603808656334877014160156250000 :: 2401978172690348309858626361822789649947560939296905419687057655744929029648213710149912561247060045344203011293014540036679712219177237609298338715555962920412130962556179171340514792514375072350046088183000062345903824607689 / 78074412670526397899281524976540486950648924394896028161540554909347793658264459419436786471442227161022703790611988034203044817260774834721814841032028198242187500 :: y; 120769254571235053383418124836236677912392333159966772373258679847006859451389217819777509529235603557917660030296604411376313720947058158684581909225895183208066357419581008429614738647471636287231670099927248934818622184271 / 947572360658908383824049561156936620768505196755719032328543811137851105230804321481527055539552116432365071030518965944366982512292452156543731689453125000000000000 :: 46549482984013598096700445334942161887100546818272682794318972616751571874793545275762569128446597468141781560259036733923492973228365949029689091361284659796061451015872693373848104863968321709017589311362227168659864169 / 192219108052138830187208755425372566381850369252627840551587570871837487338595693107560020335215335537088995841711880352420394046930596232414245605468750000000000 :: 123349986266197647095897559560366470508034851443558842885393653005956799244209679557258754568048825235848190367014533191061991079980549344252966728618804080076517931226883553534046827388148499365010648455970727235350867976233 / 268478835520024042083480708994465375884409805747453725826420746489057813148727891086432665736206432989170103458647040350903978378482861444354057312011718750000000000 :: 79734929025731754012248582810729256021607933585866848717592122462979535308346277030463220119715925464290238062018806972361158669686710396337345106176351319304193891662006662407545122598325046993937393693372805415914006271 / 91844155555563780132553608714581751465657432179616080263553895213826564432378178395741880725303240623005645682350520098147228509333217516541481018066406250000000 :: 69830021678260214271773719719651589360734502769529993139042381264052991655717469342005997593503730746517683259625139487940824767233737930333389794890824446995520017874038163682045099586232680862893517007952461721008222763973 / 42866542297941665691229799258503820787946317861339372198355113032071018950724097722710663388937238261967371858779055765475973771572171244770288467407226562500000000 :: y; 510271633214046484364515998869024944523776658292595943682136502641695959390638645887311993575707265196896019473644377232793007208011529537086206694482085433952757457696326543894326452847875465502672655404291392862452011 / 2005180044351786735076359902706367419127216051475381594526168426187093723060199216404600530721177454248348828230064100353047251701354980468750000000000000000000000 :: 10722142834480257825292171589624478368630930214996677773620159393876380367327659865024482188747796074429572461175196844657146565898995631267193679297072626606989018754947019661761258051392756499772267676108894769059211 / 23412129638722784681523432929950718492556780820797724661363230250810847041224853488240528174629132364163413516422451721155084669589996337890625000000000000000000 :: 5937841205647939540418330010459899153602271332103636937676713695512306491143483416119203905858740691181016579880838965595732856159817841439490509573529635566814191227741784250255365906875297990727843388222742717146236039 / 7118389157448842909521077654607604337901616982737604660567897912964182716863707218236331884060179962581638340216727556253317743539810180664062500000000000000000000 :: 127973776923643361380973781039320218668926020159042235462762732777717905172350385433266326062820100831903076186520225067504421327276079618055668572060562286498076003289211076213896747606037922721044466608222572028897781 / 83433960063865367803266905769669935014015091496510810279684407418912786946141080191683426660937023830590079828795069261104799807071685791015625000000000000000000 :: 64553860504387108258031144195598228157105687341413430767034340949474298779063814006267389001511227802218874580381462878461062139833561851714187368794532713075844759579740049800553805838050723146353280887553572371949825127 / 22711643727874367674608333425977059294878410827790434450238485474055303248734730198044240714003196558936171277789384248535498045384883880615234375000000000000000000 :: y; have y := 1360087830696553490410687803723935646970598024167941632840460187532246038304635292461331508173805809554500833476400027965613106269747780681392082791507463928867669052341788059764213046870597553957874088611468787127253544919 / 90853040389073492793971530772943086687533776319513558387379699480758510906245700103619960080650364398246082302534887276124209165573120117187500000000000000000000000000 :: 14584261498385164809425586062579818232092716881809857624213574348105534427035556494962960357661593851353097179871123631745855564916132585609527508939827278537190526805020322010645924995701662086349478985604422045838997 / 478848965815352056137638185720923562776648609307553813618189474910350739835271454663785201366251332357814645547477994114160537719726562500000000000000000000000000 :: 4675221799690087201123726493009184455191968292773108909986760074440356731533097269442847132557154451591511032525555212238127972745292359815069842355006849080483467748984576035105878861507600941122772487022275549321 / 95697738395337451264222810557412072876928269987637717853724502415545501942062620253977574805161674152201271681406069546937942504882812500000000000000000000000 :: 132732300016777013636367747649543805028577985070806006132522265984066173341000346201653342154857422705178773425261553502538850561977238097016596969083353575779373772982142471908041414211450240815932479278189005070017909 / 1604144035481429388061087922165093935301772841180305275620934740949674978448159373123680424576941963398679062584051280282437801361083984375000000000000000000000000 :: 9272448564985320037334250559989192489491307117728489143615021791566173960099027154903379015856420150596423488532251083261199556876397976441999922378312967345388608050993205768804463708671232372099252395341095844755143 / 64585185210269750845581883944691637220846291919441999065829600691891991837861664795146284619666572039071485562544694403186440467834472656250000000000000000000000 :: y; 1435428753662731496544424793079756739286356611048389974434342746367251144484250271686148977253991537927578968777101548426168170266083849525232087631300596367935498222886878695588364139452128844563181529639747868197137378059 / 801115896340263018033310025233816158486210984821213501646988397260696313154811527240180796186192001076963260863598407013341784477233886718750000000000000000000000000000000 :: 7870653227786385421133855998865354668622196290701715313830409806207257060252832510542403953669947568828064114386255689014956930594920740531662896958350058226202756161505443952410485057437805569373494974740276614010068823029115969 / 634490799665581287583789331447903193412465854324518278922554221778947511111350834175086542161430694032964326032502494840628060046583414077758789062500000000000000000000000000000 :: 208340820735521967030013835264082917701078434154430652701025195694984340629231894545142398032547250851875555913007718419334411832693291643704553594942807110631529075796399816705111963817834181888096910176023046865511928886463262107 / 2425994234015457864290959208477276915988840031240805184115648495037152248366929660081213249440764418361334187771333068508283759001642465591430664062500000000000000000000000000000 :: 49806477457085720243112682492819822512992643941624587330171442025245017135957297538419743838547131652653718298416398139926624934776988164559384849869835543933245465405713086674834577321773401541664491439300736769255151796105809301017 / 83772613393346279376297185167730968505239632328784054013993487094251663576420539824679395019751396321539821171478845021926673553025466389954090118408203125000000000000000000000000 :: 3523973955808820441327915272383627700847334142314710107746743582986182241036638529364458401346975651092032757230880384018256291011552852320311998873694215852661421532144747950237285808926760622619915711998391148268511133881072384381 / 856149819471709779203917695941905694124026823587738214407669135610755784275833429154955394160309861975997071778640345343092121765948832035064697265625000000000000000000000000000 :: y; have y := have y := 15165463156311347207387214277479753950752300509960935169341100961616282726827793562674196602747385321145281135429089977137376170296721075722966841687848226982278871211208527742380556302012360832155043098896500159679 / 134606233405455910620412010378420374631431456025773283678035638680055964795379981721938576640033825802876283245780505239963531494140625000000000000000000000000000000000 :: 21996642773054331163011269701421089247545685198433026870180884114918941069840729090257289478960747996627342759694551506898284240145332774546148449819066277558641282092493695582747180971031554922932350662858382401881 / 28201144790828796745614119821425702984828508111765555001038892874145488192424492544483505178411599281827424370590597391128540039062500000000000000000000000000000000000 :: 3071006289153047809495910891189652118183545500887819587051243762390536018735678355617130932976793842531831467427718351570509045819748047773878363326029170763619566092758953864318223804889923538176659073230737934147058379 / 568711336138051222371240743848826082817797901708892123539700573423236451260480422775190486304142914017152296713422634638845920562744140625000000000000000000000000000000000 :: 1377819372002862925496669891361259697204110400486053663847483008921691853520713807435211098498163177514757296786499702087218957145142334145551681663674190821090421567282801275205731736740143328446512671004286605820437693 / 36855669839454964560449300448827213741931070399878352971167036164018314388764932682340360528184735205498404074150021187961101531982421875000000000000000000000000000000000 :: 77734846694186522677865244433238070760150852313806052249828393771574953895309859172512882112714467242741897057077006381638039019427233355578395428278321570925111703691351648353524337802709908147142894595543090566958822539413 / 300350674397908301814811517845161274988149516840008652744404365339146750821941223278147475579375476465308556701776328918640501797199249267578125000000000000000000000000000000 :: y; 93925833218796614073327160615414780174925433326476048609909991505752141721909617169547625919505679159740001646711052297045860366069183458732278918495170338663776653629208348746577261435045380578151014007441 / 13258376134903360156774713022897825362275096849810935076524902167019549438474764566303729945987462118110159635543823242187500000000000000000000000000000000000000000 :: 16810589468136893996078440678358315549159510166905015610671757609262176308158440319787596330111259398132669915147692756656051307267534690348577486017616693520248446161229303083363307069808355328491881190058713 / 342759155760285731325709910535142644308816424242271332944251732158744033778751015776602109399107685439779695123434066772460937500000000000000000000000000000000000000 :: 1331398685876442004489412501726490360457112043985122870220043045477306478324476056843429997979114370087912989558386063351665933374673909834209427479742863973453968854437855862743869806297492816312987212991552033 / 3921164741897668766366121376522031850892859893331584048882239815896031746428911620484328131525791921431079712212085723876953125000000000000000000000000000000000000000 :: 696662103074882444209576309042984986869754768551563539820767119157350752824713853280860457904928313131103230495079129658602220341030882183734642158953443456431370123562788081906387824506376534567844416769659819 / 296367102585288918388137080783641942218646387286689492066680916317723329671952622478466661103693575457000210806727409362792968750000000000000000000000000000000000000 :: 8405433174217008125401540985165224883276456624893788825472826331912648678652957104314810205691566189918208116487250696000446561849274174310620840446304959671285440234728975209518288366191451702349017651818482484463 / 516498126370256163828549252492762342477166853890749975379973853396775828717114138009972456971713503533208543857112526893615722656250000000000000000000000000000000000000 :: y; have y := 1537117602247743615250913335422905210370286472152102681630782633850964050650145346815648020139509862959278186619283547001974797876688855898981691897556005610081611043211624936293855030479377821549 / 3450707603371877168733779377210086302202393184673145427289005651642170677146237629400200070720832118988037109375000000000000000000000000000000000000000000000 :: 2436728527210670767580893169958634651587239570327840416126827442010501028036456145756351546780788799295092883760484588393173079350120802738682475026610061287896553140532564890097881474563831608537929 / 790149110334408408834526654656905323940478086830855351868745412664021057637725871765544292789525494480133056640625000000000000000000000000000000000000000000000 :: 225473536533462379462719521315297470052180400023542749085954709317402109186049315729133298553042509479930758056923939513370471681061685595501222508646351014016121254692453418208906688571249285623905483 / 10560836702813327389328970318648700220291952429298651062320700406137556448489229854816352938315001687161028385162353515625000000000000000000000000000000000000000 :: 90769329775841718318791196744018712041103949753894187455410479538076722431565931043766405794668091537591363834796929568658504438269979123537545980236128292800295197955572132921980639714751607954745611 / 614105125575949705613761763007808120162350043414626620341824345674199536283410626167682809943953131375312805175781250000000000000000000000000000000000000000000 :: 1461068516736836218918422498449196361060591031290826309221139684495212967981779711380822007376394899507146044030609659589947141038995219005408471324978362919607535573135799930208498350328214683662272865167 / 1427825122220361863037276787081304269783471968441177623625758694909797631835743876371170917260188228104171037673950195312500000000000000000000000000000000000000000 :: y; 921622782146847189746506245784469365081544313680572731749208043476717404585455206790152717368766823798128692162702225230270789846459129229243313884932556496001307875299294006643266499393 / 32904102725104259917806186140659395827664498511695805594834255552418174712466408716447590965576171875000000000000000000000000000000000000000000000000000 :: 2172253377235341990642653221003627708980873828215693447487173389395710646492323969767654795148035710480729625620953452487373131762761743571188893206530414837073012886036260321953111176564316301 / 11202325163146964429991807844785518782262732260176255874032302931279089149014360596547269022696528625488281250000000000000000000000000000000000000000000000000 :: 25980439063279837761839070524156772191054647716433459399511225753412397916879539833845290030518418496899055349020788921217700250081441299112481992565179371732422267840397454306997205514094521 / 19352854102446583068424385645476643743443922841500508486700324000880818463413513322938803627249816894531250000000000000000000000000000000000000000000000000 :: 1289974512874359979780462991912237129816714855461284754790231653274398129203125315850497003077287372585022342267240647094789291838474179483609523998224921285710804291775645392788896647867652551 / 138797137285325292424385302475715005440058779469925750931925160952064960863887605631707365457163734436035156250000000000000000000000000000000000000000000000 :: 11311233657175459365560689071923743881216679405696405500469766624473925523788162278363764506962781412657932041660566976476962901363064929134132742410738078893790510091005605318565573773567608455273 / 175796488453099148947800013107098462604508734111480243966064068143001134717032501647245357449030524215698242187500000000000000000000000000000000000000000000000 :: y; 85678774842138634096057052283329697307262013091929853684241177531103547579650311047709460292638374334947033874344037825896449294765462336176250041970807362278002760645947 / 773680533192006945823537203696200558987254630694798369376185678487112425342471532500000000000000000000000000000000000000000000000000000000000000 :: 15948702317607034303968016118502485220754904393086066512509195721358547750246525824525981904124414789297666660930667464413316562184039597481761243937093779417495365177254150583 / 20802456223783398006915641492069670061107150641342437218847407459334498947712163091270703125000000000000000000000000000000000000000000000000000000000 :: 898870111051042247729210751593821130025216561499252610040423158180412115773006951135458277283557225356155075217807483205333160942411002866554302116016915097834133524007280827 / 169350719943129032698178216452074026329169758645762306908816467770707466971590212249875000000000000000000000000000000000000000000000000000000000000 :: 123621520356571270893788402963450464149202639013678830511147775900080985825941896964184166562888281499453477283209625075354895432921321242311310983931020432284811130795708022297 / 3364224977817602165711716183884951426150343022379781712904508957538306528385986184138515625000000000000000000000000000000000000000000000000000000000 :: 332188685415300800814478748934021265275132435042549293449405128822840818361333716890839760117139520985182753878181458783989593887456794669553491257718995075336278575570278088457747 / 1305799894961489297748390410230773289264354570257980987708792976804511262517817780329192421875000000000000000000000000000000000000000000000000000000000 :: y; have y := 113816830600612691622619598936821251687574038976132349335813527399603282627283043061535338157578467847355777202531062640520278421252923250071726802110823252775585577 / 16345217178067868639418204455403714685250435913507135998206978318125967880226840000000000000000000000000000000000000000000000000000000000000000 :: 176734209007163757523888044687650697159407008153757987765329740053681997679901037801888959977413757444718773907946722275654894867908550264564869654892308613804642177 / 3666111513369259701732861592826920132992678862587866942316955109310517295427000000000000000000000000000000000000000000000000000000000000000000 :: 115239540983121322025393850906262632896386437675698001488599977038596334892623447850712204818742779521790895931973055645528748305649811952792349883047892954314661197399 / 345292712886683725007709569120403472725915458672838247962122416970411071469791995000000000000000000000000000000000000000000000000000000000000000 :: 394133827711449582154538582504660085317050701706840490879077422352186283729182111639042204990749154024126594501653343507375322844949363530890658692625998372507044520369 / 170580917977798715661796001071444924597883639682148099978472861867155926933000690000000000000000000000000000000000000000000000000000000000000000 :: 2520288761300864605071257809531826172408661251804574067224027125551697446121507875396906034010125654215911321687776298811380314996433457398825258484437432153164475420619957 / 157557064890193783721017876389640104604835223792416092545116458863598571911666087318500000000000000000000000000000000000000000000000000000000000000 :: y; 528685171277994525253073557508764295743449853156882085710230309221149982848661079124193900324514758093541553557071206531456092801481419879701360259383343119 / 1207472149715042443864431769687287098086218275591117723990695002552926369280000000000000000000000000000000000000000000000000000000000000000 :: 333872952994125549665773781265348204384875080557734080147552469187691146892421727195651973316498114251349706539510836911491142173931315689949487957135064171 / 110144311972803591010087501044048843149404433719719038575735009254527164800000000000000000000000000000000000000000000000000000000000000000 :: 9309456276915656557151163483782319325670376755478347871471597649865091015768236840086536096518499506624651915343630113886694542191892325323345123437040836927 / 443614768047482984811062976254677216470806279510649772509624903111835992192000000000000000000000000000000000000000000000000000000000000000 :: 42154381703925173278308609803159802749400488265171059181653309937831953136283817188496639380413681521317111170894630042367171320845320232793258472322073564913163 / 290151784226056839752985877906574816897936732192434366832076538191585228643080000000000000000000000000000000000000000000000000000000000000000 :: 802643328577490989390545303718615545281487921737188080725794971150877091236054922880489533174093220937093068980677069485296128648770946956065372706113583232703 / 798005647630769327082840516800226925408193265669148308841592002219412486880000000000000000000000000000000000000000000000000000000000000000 :: y; 14652147863527498148201462907459165612219780621516201860388082730852523626176420108452429043396026364836411096478699368039304954929319427 / 8463973265773837940944305311966885699414844372399519431023656960000000000000000000000000000000000000000000000000000000000000000 :: 797417190382809898021694846627095897191537197188915085646430038768167555520651507575245992391026654290549774555619328008609486315445547721983 / 66536259839196951198310791831347510790707090044757733061994638540800000000000000000000000000000000000000000000000000000000000000000 :: 29991453955505520405058748465029072818022057067714996626103141526685566163280961554084901739635068300908742567368572367099283534162241703807 / 361468847457095406010355244289310119944063955001272989971135987712000000000000000000000000000000000000000000000000000000000000000 :: 14855894406168266196385204344081512154175673785924288748602785462979854390363715258883346319652102294162234846463326143855357706288552830831001749 / 25862644199495854930783404784844777444347845900397330841197316000808960000000000000000000000000000000000000000000000000000000000000000 :: 55347541483400399917492810174037678655311380569331194920775768631080378911901913953023109824253132326872351909878681189509894061383785028319391 / 13917886103135576193243542749637045443412758070338423684048727408640000000000000000000000000000000000000000000000000000000000000000 :: y

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3q2_eq (y : ℝ) : s3eval s3q2 y = (s3eval s3pCoeffs (1 / 2 + y) + (1 / 2 + y) / 10 ^ 9) * (-8 / (3 - 1 / 2) * ∑ k ∈ Finset.range 64, (y / (3 - 1 / 2)) ^ k + 360 / (29 - 45 * (1 / 2)) * (∑ k ∈ Finset.range 64, (45 * y / (29 - 45 * (1 / 2))) ^ k + 5 / 2 * (3 / 5) ^ 64))

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0 = 230706600404117414407928878394116608565015272112192158756978170478007678257868614878952179142243978278913889948204447846526788688805453338339074099134289982176299622885318151718069735653224408526483325335606925006187665601719959217976485401760166472282450276331070781975564091302596068240922099432824326525228572856164967921640729497418761017682402693 / 845541804659899089021690000422792871636647751677482815767733154222108859266556896654923767299910467314612831542345919163447828511824601143504130864442386636978975684093493113580275452688205153890171269335147442709573619579914658385732105201240423840933290031116357012927482698462826465253823523909957465827247347078809980303049087524414062500000000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0_value : s3prim s3q0 (1 / 3) - s3prim s3q0 0 = ↑s3j0

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0b : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0b = 2625892413591646433209074886121040804818169618858670254983528487239922705120222451042964284117290689528929574324635307051419086559836515876304874796546968137986398160352794927584080027879200469299032460412312891075986685177960895731329659184621720648002668126311125771749278289893937252517964830277333577945664048831311660814684094125312333762407266169400032137385709292416634906452156576537871114100639757002568063495803502142096116885134984525103635378233176016757274478471700407283435254356935033566371274289479911300092141565768898875286660424525712876579191510566398140558030874122379612126326500813947308738906717357437 / 9623940651079912072992486745387274629566961774818214731005486447776320000594251517713549650628937258164855817914458159136080748448151080459829494844940543049841562569089270293764839373401238181679825002403294557335278244281482711431446551206461181162436174154642807789393498696407098327824193455784571481649611587239772029287870837771637725185045143566936818804861152809177852536232049383257892561233256401644934366276875155519288604367226928701339595642948742862881900790696048488211735866253966811479730309202684671968879414276618655877687848626956008850965887157105977105394072762534207754470116924494504928588867187500000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j0b_value : s3prim s3q0 (1 / 3) - s3prim s3q0 (1 / 177) = ↑s3j0b

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j1 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j1 = 3474608788572890306213408203678008632625131652427899874144803470427186604802769552531208156217848338357434534663103063446808690369664804884317937250520639031301271896222112740368783878431583111396977079406436937688361168161867073030052446731916388709146040372263658365406882143060716261544161660967363635340318639296495177943634732924912534658287870577 / 2217577889603736438824779889444574598862573459041472927828774147641423450428763179836931639782377539238346392249463340198892965945751497695353581404804705164723702212345087074544961111029670725779279047332685482569097025043453125111894846770116585939804315713514893566578694952058880000000000000000000000000000000000000000000000000000000000000000000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j1_value : s3prim s3q1 (1 / 6) - s3prim s3q1 0 = ↑s3j1

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j2 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j2 = 179521869652810872995773227846100634322867713190996057819835623772713259412505852451855771719027137529529258355586672983703806268828268672288390385426978301201203316395201279799556398201688770505811148353655632764023946254624886470637549100956771813496118059819438248306977626086285832581722266605204019500113875925071234984416519372782305579921492469982218100960356893881795367094963881268968045331297356455820933961475326921713435112435833133785989559943179657280018658904074577697949136809 / 74712193717500092501227255582599166017200689475239404282373350321944346463936821503136309828621962615079345583727830622997127203467664428591314886074384487767365472545468999035820109224426503945362335210604857594029548015759384065645838490580233945780035126807955178003075415633659035893918817533053512245484650061414102465938309772211378693590517606183555787825861474066688453364942405492142499283998106027004894264688640000000000000000000000000000000000000000000000000000000000000000000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3j2_value : s3prim s3q2 (5 / 74) - s3prim s3q2 0 = ↑s3j2

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B4 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B4 = 236054898823 / 10000000000

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3Base4 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3Base4 = 62777569620538103020818452218887273870234121511818213238800904485658924982626518722860591023787046855727059204834723336958277424424847621433885154235697962895887212077869731654709013410020753519790047681703560801882288749776110931275525579574991518851307377384395274697670154241241560281673042234418512961440143093430220712381373874431995906935575295614393175086548714030199005588666939078362788392855312432641613453665696780216752172853430251111705144969438830956669088263350114710514026147828191295844732892181481729204014307774492687 / 3242149865418519563851975547553435168059601619835917624601120449301831484229275514676112558216001676075456317531256654704306421821792369450087839374731653604810307898674437045984145296902521116166614214790998552262723195396540366814046543266864147831570566787796643931031284583738398065800597334385935279378915088162789796810141318795965515828309046676827176761896636887425347633564942281573666989139405520548892562744298921245516631453789052453392022212011317427145789147268742019159197499879811569314103742511160658650289414735942875

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B4_arithmetic : ↑s3Base4 + ↑s3j0 + ↑s3j1 + ↑s3j2 < ↑s3B4

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B5 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B5 = 195188842999 / 10000000000

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3Base5 : ℚ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3Base5 = 276677810403302105278023250505234395807965993871892757943178264481982866260246322472627165320087044434318180134333385943260051791817527345410840743661355113369729093521828535287470690615975797739203646706863463320965219816145204283798719696925952709488133925673106935840907734331185183601674815824016561383886536730106814126074404451871062001154455012135534417476816061891338623100874693271601265886126465741300478432494930290395082199444245065531609896034285986016084476107428951191063 / 18111524730111079110809418070453876222323868351804689477950081255226616259085429503883465361453606568533949037390606616311000899916776563190853728885240183052906026338951161515294002910941587254344502317827934204124929190182245694272613644063139411121734865523477114151091256023331008417304192943123098809882248172919569918941103406675000306134473941191994578378667843958803870535005832224813258631322934474617638304398850816741564121305348679739339139272745418723087505099624597525125

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3B5_arithmetic : ↑s3Base5 + ↑s3j0b + ↑s3j1 + ↑s3j2 < ↑s3B5