RH height 14–100 — Mellin moments and proposed rounded values
DefinitionTaoFivePrimes_RH14To100MomentModelnumerical-verificationriemann-zetatao-five-primes
The actual scaled even Mellin moments of the Riemann-zeta theta kernel, and the 256 proposed rounded rational values in the existing height-14–100 certificate. For j = 0 through 255, the actual moment is the integral over t > 1 of t^(-3/4) (64 log t)^(2j)/(2j)! times (the even Hurwitz theta kernel at parameter zero minus one). The proposed value is the stored integer numerator divided by 10^64. This module defines both functions; their error bound of 10^(-46) is a separate theorem. The proposed integer list is unchanged from sometik179’s original public certificate, with its theta/Mellin attribution to Gabewhigham retained.
Port note. This is a port, to the Mathlib 777aaa6 / Lean v4.29.0-rc3 environment of the Riemann Hypothesis mission tree, of the definition TaoFivePrimes_RH14To100MomentModel (id b049d5b7-18fc-450d-8b2b-aa87eb392c26, env 0df444a, published by @raresbuhai). The Lean source is unchanged.
Definition code
/- Moment functions and proposed rounded values from sometik179's height-14–100 certificate, c9908072-d99a-4431-aad8-a72c6352619a. Original theta/Mellin attribution: Gabewhigham. No enclosure is asserted here. -/ import Mathlib.NumberTheory.LSeries.HurwitzZetaEven import Mathlib.MeasureTheory.Integral.Bochner.Set import Mathlib.Data.List.GetD import Mathlib.Algebra.Order.Ring.Abs set_option autoImplicit false set_option maxHeartbeats 0 set_option maxRecDepth 100000 set_option exponentiation.threshold 20000 open Real MeasureTheory Set namespace CertifiedZetaQuadrature noncomputable def momentWeight (a k : ℕ) (t : ℝ) : ℝ := t^(-3/4:ℝ)*(a*log t)^k/(k.factorial:ℝ) end CertifiedZetaQuadrature namespace CertifiedGlobalMoments open CertifiedZetaQuadrature noncomputable def moment (j : ℕ) : ℝ := ∫ t in Ioi (1:ℝ), momentWeight 64 (2*j) t*(HurwitzZeta.evenKernel 0 t-1) end CertifiedGlobalMoments @[noinline] def TaoFivePrimes_RH14To100RoundedMomentData : (@_root_.List (@_root_.Int)) := (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 230337744934871206978100825168182415416511235383585125341261280) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 40521025678005477415456616733783672132802773496266119565479671793) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4474037647682628329675671257143783483010223849002749953812275576994) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 351481606056109814371215101276232647382890680092901678739777715030727) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21079322957780478348614085877194415708902446857461078509372025895219048) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1009906114954808594635649856423182566693468066012802252484490411697737673) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 39903750943173106741665468822383755693987872165751985529597445144845680539) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1331470276361406723382990211054507272438448335323970548523937999689088179798) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 38210603612544347746315297629478780370009798584563038472487139984253116180534) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 957002659355094357051996352730687697044637763073824082397908009095374325090813) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21169112240876900122895473916783501561578580865741024483646570063992924488197112) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 417707216394437395069182164041149338016821602508332594906122329231102621263511994) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 7414448651866805443080890666142606697008549203242062339680258167052349871440493647) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 119251079574613808442263180612819754528069143272698342764324606930311890518183788945) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1748827836515974891785470840690180915227738473359199733984814329944979037706203206215) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 23513723985769920939217262691957387645837874121950613396068533358212430466909663734953) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 291270693313355443376206815370169006340788048154649240517879787074749061828146378513085) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3338518131038545549138164387804051538738418214480060569168393458696955129363494882040444) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 35544985229591172625684774299524936842802041283057434755286810486152610397600730676270022) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 352769653373032509609294502733122625725691175349819236585001236636052871362825144240626591) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3273942665769892066201192175725157345610380961494525744239269899064956498739987174598171564) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 28495341128344223264466382890880235996054876098944147947017153717987076374357885201505864504) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 233210830796486179752541507992613355223459727378496691445694279470086198699800967116313064979) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1799082808553918074328921290271516627531882269244807441711139435166392296396227287227260877117) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 13111555063527463899658137982623050846424460849761654802608628406121496667428135423995979666172) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 90460258395567983297826010561080796586035155156165822644366792665546611035938819704943792696021) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 591966227421235819961939370242284921900605584099330505613232297216647356213622414218353866061424) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3680851328381476238093626711503856449769026470186667050464951856397664754592000951305749289737319) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21783938234617465080465127501663179183803511947053137835933650329491848105998827901501454613760898) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 122896286345298928202889691868195211018389050672765997938259510159468210422008747289629807082647581) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 661896764059095544418944509051882905440391939571062170853784862967738469690496177016535758832757507) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3407902375649385423255931472837615584956129100135229867353169374123845800389531134558494071019059342) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 16795405641116791769934676225690695569672686211415590869989697594699871268080253179556179036897751009) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 79328504834735992797961735483857995183186360903777911376594540590744634700654477288783620592366924670) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 359503402400251072302632420442272446033649605800195348037908812570660365117829316867924629309956614099) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1564891578809607683837439345958753793693489138324228564605133413470409915656456978041071303134103249258) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6549689607050495289748831679864012911033094229985282350613899131183797739851433544424314683038868332273) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 26383790673483976500802973951375480799101840989213513544639973606510202222807435321190830414439171669686) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 102385224069815496424048117347336775593083111413716788412394968958275130923522935816824924157860649531804) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 383093681304377101691157527548427416104242535409492481225575791167407445709517213576338822897395161226712) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1383267233012268096728763043982505147210531055195534803842484055609078069845426765276971794093832361387402) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4823801669256233717509961639779626798180498814081390138875458993263767919832791832099673248596818563159920) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 16258786912812242851070023368221738286650130503766421712302217438297804186103604983098180301577585905467889) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 53005453321238144063475135375553213102108249789666361835289818298916112267130272552203426619277441277344180) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 167259699739909746586097975739608894466640887421980309589859051356015158300103430632898041582321425576128576) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 511201569199618328388682035642015183716223428657078761898530422970635251622387085480862514343916963521077446) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1514268360033576699239629210702377404203157316318801040737917153348240908029663237214898033548070250584733811) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4350024466032531736137485651158028549124851735541798791494414684336922034796622944044073832763356867556942868) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 12125969447371700538144145523858465768072390111850709665141931270113182005634337628419551349269330031662963366) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 32818965027713334774607672466550353878562293347435903669565112216134936692058699526343165169275653890933439669) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 86288957294445055453723896102565961035526299123475221068609509920240769688194119818758828575657862598883674965) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 220514359448124013124360309693042963618313305251717885468867657801667275549776073439190573376017655961643565449) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 548012950584713318471240374180930833187282403868929268726136061469816186554298556635017901922413077283474191585) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1325043362697313661267273124401190889083615877032306762592870194947488991977360359051896126781680612887009017353) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3118603695531478887931894731224078196241574803072467660459290885064421736913864638145833839019274111024284178871) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 7147916901257877142451613994534244498891099975609559706458204629373123562644743662953505755920004710191712756016) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 15961717749099447270220922223775485461823794648968745871376060444538355296492143824801841686549146792872238636673) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 34741277717018998441055817119538311887331505553002022821256599645183350195301304725940839221873166398824406255724) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 73732180885805818997195033400198578417488576000375397042723824904020656267752346541585961063534657631169786041169) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 152646486618753505797712642726787604838126950708161968694527464265762385133015854388207189859135513562504335527355) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 308391766521426586150620190528414116333451354928206260327662435502671379948002469750059156354308268726793350292723) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 608229524880516581095696726084999815537489900506554426024281557583402842240547443625026397508703078707024412270470) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1171489780547940326466838979833870263082176599874865247882354536210955207753067997058796643245282944398760353931680) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2204289008369331614211393192734969310993912795935596010424838156469634079887456127982902722961703777789873768480800) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4053272171115841125896038746079161026203787208888575616201569194886653253250115135638516581780654873154752919733383) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 7286081356399804410160825762798926719343870265243834117930823813855264120555140941345143137203971444012418987732555) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 12807752599681632682594465631968923341882774085929257005367947208425015821862785875704479277157417194951509064851554) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 22023085559476589648315906949873989177570956203642298778304535176403880895601429389498726489101536252388787443069479) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 37054551713705799431963597350577060771485155049770234531134872484328507438646736753642822364035197057628436606185227) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 61022683659403032432002100378529671339726819561070662378704454026256648512252694334542358434747243494807425892910799) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 98390248774068934267818496253608159345669527825577705641147623001679881612399922307052470703199684162013657401011607) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 155362120504156392253006756819371502102861726633411812665843332583965484456445617692055288014314955685357000879132586) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 240319288647697787465250087363441510160595712827731040046055083334949488764089353082400005936884487491991342670001249) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 364248280011243983928797243522795257841133934717581745518237469613634674608997694881711842161524294553001711362349831) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 541107787007418697784410183201362294013501196179903694285905223858669966419416449768821043307339417314748895183543560) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 788055116748299936781383114393733450895207237085888709262836318213897820100190754347406783931034451016357600308195398) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1125439944043561652792779094446107559017022660671637247540184756636004062239697789015159637919979694881578422773395940) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1576466392591880596347199661982691471137965810011608752063057918239854687430762539239506937852725634307541914456967142) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2166431465244016535258128801836656334132133849122055142594873758332598963983219213131361100894413176725852844603534717) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2921472264772708457662769876573055850874158803435613538737788515162063294914296659613122157034663860123284769475102159) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3866798274909779750378055930680577087707182518092710812078820332062061610144690701018715392851875319483457861788565354) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5024447094416485861170639375149215236523823673073569482122014224502665642438287774083100379864705927284553385868245589) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6410677462716058256830386674163337664583441535138435840987126266048393328101290064509314879101735491193198555649041922) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 8033193236813446749855158340740884468890791939824631423641032097492682601375716611501805580601185352745911567540370250) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 9888463992892261026294399053302050353315475755986770043146024921981751181573528907016258458696004950479378982133934344) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 11959458355805667432840357083911271779243644253904285353297505408346295891788543248174284203189065026354757519898461126) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 14214122009168935492411437611278131328892767265799177436345601839295380919886842683727210518722209651174934101709415441) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 16604904102785954468612350603108138951522203916254430092706955436179017489435843836894531335025626336091447025454085867) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 19069559934555604974272203556854497191679987078795605860357947493854713111245860525506225114474583435991010916615538655) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21533338488066587164394371988267857042086587760873074203424439347967880800321413106237897063512771708831624360098066115) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 23912512827567368520471245946349022060662646536742222538662198688126551288707656235987546918074812350659353424398720060) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 26119048469582367014988263488255144442775100970635030486929259871895764787873083662704672194888052583349584279025495951) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 28066052736065570155910996473431311562695168169936040290420597647273733027223147204134799510380805402299634636973088997) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 29673530122311393504673243590584568917775152462440663883020155148884218775544068780749032414317681680851346014662324924) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 30873904418246021375508235302891495972536309292439648952355343855120366032945067167079339323237329862993950325768156985) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 31616769736638708498485330717603240395631976551395580032763282800241942160595581701264757530264366886817991084104754222) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 31872401853628104556682396338515436084415629360127184333764883027551715987188171490159605085528753830484618024383083395) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 31633689961338423795524837129142484707100960356733319867405068202285497053189176103942739918717739211535212223311035615) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 30916319474063644929093298891980903097400265550750296554278385658800961810071064937323249376826867178222643985715472643) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 29757225120046884352371459059332046256328854231758780953161282104759368970069694311566051451638609037760381035606472228) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 28211514250876815925070829636244409132019321224818761063927215945801499961477186047300747881032585585197972117238257682) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 26348209340089073455502688921264956471113530343208911202852767530395999551093900924914267382432742076796253308723124053) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 24245258146092610141417955823902796228146542823828446491405190889214568825838575574944571757921313966461982947712186691) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21984300471538932719014158205683329480515331440037348623648165494525900336376354971565810031874668106204673722403591305) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 19645661563473902849622212119234762090192892736824460045757115798855759825972767722205302170999291058154928294410808391) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 17303972086882990323347546994630570986381389383150177448531080322087827998216413415331616626748808246991738244020703427) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 15024707681771443125228122817061082970304835954624598181834779529296532559599966890044946529984599157163083972762964315) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 12861815158134630571814639260113417124123533051006205795871069473099645877468926637509083386436492322031698224795879472) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 10856465426923995844148268577020183218910516313331689568430848289913452548213222422114343357044101462560043691928382155) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 9036860879065487806368715471363029470570340033033666499983088167548642203675725409729224351270421962103748712506200999) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 7418938305539314973164751917034906166089750341845617578379201791312644816269906264863651249751131508729451077711335286) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6007753516400793449864977883785246682598153650004064162729661575917763140706103782026762892886531136508243760980395238) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4799311283444681351323325635120794438156327909124966865128343046689550714342820801947252457868227820991338080957981657) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3782610492737314363585041922809291142303162768195030715034604995776496649488237622638069013662080912617744810433363740) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2941702883719540247753618494519485391372258014759462620867620811061959885937975917230257685345598793502195846336844532) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2257606480431147015634527243756413241092724517247810393168459660617037098489921245838683690770426137041152705415001897) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1709963786594029934198148238161219942785634838863411701208172989743005906745803797948514281033620633312478943475591334) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1278383102108132602914421361878262378158352979339386496251673552331256302548278850874604727649696315422970207826971988) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 943443763558944612318017707610808411273887314735250432224416427802887561567347223675471118089514646927394817877515471) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 687379563251394684755067780715941995323445651468136693575339997585136956681214036120488521458135739594657030439537169) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 494477812054412051850217461144623224737510897609951119568730385848780066648952390895154674654194847261363653201510939) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 351244789036113620270913445498910441870570534242033732902968911487802793610087389836905272625600865367917833372786896) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 246393057296385527927625321801261584958429554665349433629837825203149306004573134099703916107541845397820854118182731) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 170704306511498144832131365133348094690576538087043079584676446264136204386565688161873242797837624176850679225618006) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 116815160441825511579597983372462433697761608772487210730254955409765946275095566513344232870818847525772280647190139) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 78964758551213488567191741501448918974074810491770403187942454495016129340408120865933118055438818901596375352400124) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 52733525787778959850093870273125969060751345987106333399282340713222661814000048079714128034946992652815449139207094) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 34793580278346091081561925170229068398788469309261747585284095701998834829406913551667770423511983416414489431588675) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 22683447823210819510840556670341483911283287054625912140906130879751010151406524119083066874989610438225058271674139) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 14613521773999908153576242585867167705748049021504075955887079974772880637663896698379791832865959290753102610359217) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 9304097786168062233919889702895019864127394590317242394183882927491824365101373899113482989434491834341249875394142) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5854695471590296594889268485516069710624502931626792698643369273633070248946396071107965676660081652159775479677374) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3641510768964107417180507143758806896272182343659176857733024908494371024894190125898556739215964365407358287805250) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2238938551548087204043180353426761744867432305741688037386512686964575599373813756749606195915481205729546298344035) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1360885421330486093682026502271488948212604237540682412072580849542756178111097563063528042102124898118787448570536) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 817814442757512222191498690548480755255908110387124058086076137406343528204424030574211684453019871896896485385327) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 485932935304902485532170910497585908805188414244843874851724444621448721353524033401848093861107235095246531882998) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 285509307783714983951466760154658945128542251471548036259267581372277817257527323122444062964170876560291183093961) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 165889973386589654877158296650175768336046352771272056895425710234530369314682757151126263140977580729158438175944) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 95325484777461657595177313088853274881009194580162690699427886083499598193650976792720736744279178530089542077821) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 54177574428624942806329572906961615291850676073509562539302795042159473769008174255146586362645538606613036575596) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 30456775763927113466073714225469630453135090212335782121720343984871294520034649202655590328680543320866097004887) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 16936898050875261249102959812866180441801909978744473925308521906586332475592442117343579794686059022012701588370) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 9317528210135331745884269504579959252549755746191899203994783915592278645937426361319676857122436776526076593905) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5071253851409451194529197009000903828500390748571667978434131758119884995335124312752267541980288874352600902642) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2730915483896227844291346380728564275966996781699100837078740352126306404706831244432968819696621582179789353986) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1455155899101426667562329508852122212401563629446993923938819029776785019679114132599142345164519453291371396850) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 767271078112243542872014583274611064826529388547039749236929573309609013846595080955271359518759363838254688122) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 400364412855510914705351579923493252269719224169127031331058385937738738722804181457111247525881769265725012549) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 206756112848320950299126263066873832337706173026969870983750191987947494592287962740177768376060718343683745802) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 105678355003605692066794025514549455806012201220062138851900921351412831646318793911879824061609488473686071150) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 53464646831642376647760878621640675417407056521717965017467225622273550580502346884310850968099206718651731163) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 26774918106615866193036307190810755244898150238624382293098356671627280189477945355937315554942734635720191340) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 13273879099850554908931965571781108787668622397939498185378583368143511526558818357815268334652659122428222404) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6514827842479392165031781418775183687880260186024336708113265137112123439289265245887832825786622276993332118) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3165703179774824618086768989640998123745923155894566626852580956614691239826936451631752133053985423195554778) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1523091711261223364068703398571961436126544028045975800154231033484571374940418360436581853832763232946509370) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 725598966115632643891052880061095851796853223215076616625309797677360375538038964581349381103467892646913777) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 342300709155401550254929486278323892647613868640702992553576620034732212487899071298259805629037777553886196) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 159913443840765758647254087712649319839494340822775911838391191982702433349259917353376849153848601404280854) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 73986650981835381262877710348956892281457683674913100289706824914159828407701304084401946042543369618586808) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 33902978772603085559596380624168863702614844091091365457344330328324635085280554632014188452404079317475776) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 15387321335580810055720039958490666664152019075782669011076303451419272284438251729996094032758834944962391) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6917563526809352821660728922599506854507371885081832380572043324121401129842343124659841649268636865448261) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3080578353422031391087923828966453956408314324983125302078899635582350534130147055876842329965119154660134) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1359014387758804552797279302384167444186322963556937131272306014488640427451808723143888038531316477116082) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 593952871734669351352614675366201680438326404109783533863605871378540181710918909004191933764580691660237) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 257181205609381363445474742255526888919011444656487668987937061184880954029124176110164821981500675200467) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 110333827571476178283805974572422078241923994869405228823571824976813835443464159149617092454601443846856) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 46901096849359548598030680892988600441945956833899401006836693275901420201442377073625181036969722002401) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 19755342244704333562853842753561747862367681632745902144886839983216306792444025802084499395764742337696) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 8245851158358469345831580273399339388878368624409501035288102986958210435536871351748583632669473652001) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3410811212489669455387005762578972016401218506714583352046524601265310812167666205970074317356767488210) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1398211169295878244953717693619777455700273627219000854373461124757180789801012323138332582661781135955) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 568070376924269854258908334669388668339020728965513199837951168077962876904314029570652046087170143636) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 228753089573969858797539365414537630455718843484395797755581041643323701890505222030291484736930509413) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 91303656490973206429870244988201108681940160409246801292555423368916752806781704737771709294173274326) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 36123219135367658635354255660358276393724511694550236673574519457168694368623170425579131030450443032) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 14167142634018493661728131641245212439054101759777379865676285226039498762611842360757890130796016317) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5508024743594246970220057476792118666813498790747765443471363665982435928922200540054110167403127826) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2122986958788415678036076216755721467920224495089087434457396677308891001315768419817478101313173333) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 811253185948006252156337030880053540675415404880160201386596766203745964611164179453393158826618382) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 307356750554571663111671953857747333623712185976516135243833759786556378019769281026411291637668679) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 115458456482844912278364916051942933587315365338516480858036415783544939131370493459272978994569008) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 43005557640193437513758370485790451828343922428909937834340925228009171326936765425702338164717394) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 15883940722434315555583526513098283513428158550630296853696526294727739372165299661373887480197655) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5817622880100087289706471368268897823925865461094279778685530167794735633184587586512605554094139) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2113027292388215383384902730748577800965869698254445976104928225671717828483657681964463901815814) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 761123778402704116290219071467663639037645253999010817405412392379819402620129089770796174579985) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 271903210325061929562216655058598158652380701216334257562881898232453000901024256602841866154467) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 96338587819901656764277777811343395898370623624615114974481554932817621444371573457547156043027) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 33855634887481753601934627470482488249490093978944039022978218200323715028386602618333004613559) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 11801142784660292186534810895891576637620037023985003722554303488879101684409685068181512409756) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 4080346797004230778284237670592229353363951694847475434032435654359930307364639214392562719754) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1399481989559843430660920757181499912956361150288886898083540907610469273025768568401200092913) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 476158918311473346377755538381091878761081950130130398354706346638323919655542280116848758666) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 160719243492927760573229511524478280117459965816923882158044386161166424281530519837520022895) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 53818549913498936685516959468622130449770070432897552830458261816568092357816117751735593512) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 17879727850704803165154005146105716568141667156875353452403019822385690549854063241717431229) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5893470274131850050455164699819786557069644888091093665784854499907028684197178150140971172) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1927431238333024601928975790464443931942664671629763405595811934073370469604414666977622512) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 625461318901260630002780142214188309568333154119687878014743394258733320466146951484989487) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 201396442462929629780557831201350302328678907688739924332273516443432730099118970359446013) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 64350031595480698195187632786846164018625605752032864882432663738108508088856005377758103) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 20403612659279058811629855164303095980734681564212864555437616704918751116012388731887185) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 6420107032673464067478586260827535025706505865952476985262515704982045321421165234013162) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2004794067396725613361889452711807529277381113755822137760056210265476119880015404391831) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 621304981178716779407428360038480251682997731531771054440456066314969110343334819320524) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 191100838271598461840789183587450734318889830718539672128266077179380698983292398735863) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 58338871041528099446932901933760742666997727692004285454098931991285546534192575253936) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 17676894272764358334185761536639304230478036761916155469457036277860228943145444805485) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5316442618057808921118398829027243898708000398300859133430232367136929134823185601661) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1587150433662812134344451743489804325493537934508286475132215825087676638419440387552) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 470339321087277591251779861881261768728636751086183134497247586403883568139259036115) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 138361425199269938520982181645980820222504917244541730707410310752765026122598399639) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 40405779369493323177137705013206813864205895197663672005725192975235532378489814027) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 11714148454305351304191858180993050318476430519134695562887480798295624085425732765) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 3371558188074921700297922131675114341827848694791383519806308740969539028810304320) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 963423193803261889964685815714152664253103249045141373192704022569284709107148512) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 273327744485321878291024431974313056605948782996938525567546754792227199366933444) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 76991730027329504458982487871966581527445582610250072824890164569643179984196778) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 21533351016136120329387220052748946269276628929434789521261721162634530079868402) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5979979070509533048027262821970493939428762559133625902558835247014974159029670) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1649002889983821557129845325778487549188142351077220989216756344679693659455306) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 451533492660709838490739461029255520118855101183326720183669979697827493940374) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 122777363042472423826084446518287987115484367901030976983025887857476007241166) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 33152728650116463955828458361552583058210906932268057411888423622642813614057) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 8890079792316428993241760103418812617948744664767479591869701656345062229588) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2367500555302219402185818776098054525625249822058751604606595557624219621297) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 626159698251605642668385708271183572281544077736147167710314788759171553110) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 164476236405621721362112883438033227096563530243274144786589079769382128734) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 42909807333401513096470074960289146104365468314301453696369014344470201044) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 11118790639712553134222831610813443944024426202288570094142463800943945858) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2861661426727762745451724033243470304714019204925753100645534500993743574) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 731561226051720630884607364036597580679771404906355180620191204655841534) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 185766229493032334041489795924184659589824975660773452165571304662300350) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 46857416268228191555039384647565203313294710460675863181564794322218593) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 11740784677081729058657595546216437665062844022753008790870201803910499) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2922367010278589810234328714192591214787659798010120363397893230811162) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 722608019498618097701432100076492212567464681928526784019444539472502) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 177505833604297376144512225956684151282906999547666033753469454064308) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 43318725458201218833627979739151936843150513501542850079746761125724) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 10502753157728905916634305693036038530276826035185762025063070003612) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 2529916967615284321400157210514678263046911751565233817624981825749) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 605474811966852462774833090487881352146598353546103511944758143083) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 143973841767317043597185403333825897348073231886751391407822883105) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 34015723555222151979559668184750159455109614228037050647815289054) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 7985374033618188486601203600617152286198413367844692610875450818) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1862691705350919262500260844422122112753419971266193632064575628) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 431745201371402506008809968055918255176220123123484430029717402) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 99440992463567904872281968953405115938970789177988452222455195) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 22759633378880396049095860353839022177629066086599119650132626) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 5176513643619638944048951873943423628269559975807630345639002) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 1170016755389539788380436228117947796418712408852049646995106) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 262808656082222555837306081210618205835764028970434795591968) (@_root_.List.cons (@_root_.Int) (@_root_.Int.ofNat 58666514479806482326929441881640849167599909289675930492757) (@_root_.List.nil (@_root_.Int)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) namespace CertifiedGlobalMomentEnclosure noncomputable def candidateMoment (j : ℕ) : ℝ := (TaoFivePrimes_RH14To100RoundedMomentData.getD j 0:ℝ)/(10^64:ℝ) end CertifiedGlobalMomentEnclosure def TaoFivePrimes_RH14To100MomentModel : Nat := 14
Source
sometik179, Prove2Me submission c9908072-d99a-4431-aad8-a72c6352619a (2026-10-03), https://prove2.me/submissions/c9908072-d99a-4431-aad8-a72c6352619a. Theta/Mellin foundations attributed to Gabewhigham. Ordinary definitions extracted from the locally kernel-verified pilot.; ported from 0df444a definition b049d5b7-18fc-450d-8b2b-aa87eb392c26