back to table · edit · history · where entries came from · files · download
7147 bytes, as of the version from 2026-10-27 18:01 (current). Recorded here, not run.
"""Independent checks for T555, with zeta-series tails and an AGM bracket.
Run: sage -python checks.py
Read stored entries too: sage -python checks.py --stored (key in environment).
In the campaign, NUMBERDB_KEY_FROM_STDIN=1 reads the key only from stdin.
The independent routine uses no Gamma evaluations:
log(gamma_n) = log(16)/n + sum_{k>=1}
2(1-2^(-2k))*zeta(2k+1)/((2k+1)*n^(2k+1)).
This follows by substituting the four Gamma arguments into DLMF 5.7.3
and expanding -log(1+z). The constant and linear terms cancel. All even
powers cancel. For the first omitted odd degree M=2*terms+3, the positive
tail is <= 4/(M*n^M*(1-n^-2)), because zeta(m)<2 for m>=3. Exponentiation
is monotone, so a ball covering the sum through this tail encloses gamma_n.
The n=2 identity gamma_2=4*K(1/2)^2/pi is checked with a separately iterated
AGM and its bracket b_j <= AGM <= a_j. Here K uses the parameter m, not
DLMF's modulus k. AGM controls (1,1) and (2,2) are run first.
These checks test implementation and precision, not the uniformization theorem.
"""
import json
import os
import sys
from fractions import Fraction
from pathlib import Path
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from sage.version import version as sage_version
from numberdb._write import to_text
from generate import UniformizationRadius
CHECK_BITS = 600
TERMS = 240
R = RealBallField(CHECK_BITS)
def endpoints(ball):
return ball.lower().exact_rational(), ball.upper().exact_rational()
def narrow(ball, min_bits=400):
assert ball.is_finite(), 'Nonfinite enclosure'
assert ball.accuracy() >= min_bits, 'An enclosure too wide to test agreement'
return ball
def agm_bracket(a, b, iterations=12):
a, b = R(a), R(b)
for _ in range(iterations):
a, b = (a+b)/2, (a*b).sqrt()
return R(b.lower()).union(R(a.upper()))
def prepare_coefficients():
return [(m, 2 * (1-R(QQ(1)/2**(m-1))) * R(m).zeta()/m)
for m in range(3, 2*TERMS+2, 2)]
def zeta_radius(n, coefficients):
n = QQ(n)
total = R(16).log()/n
for m, c in coefficients:
total += c/n**m
M = 2*TERMS+3
tail = QQ(4)/(M*n**M*(1-1/n**2))
enclosure = total.union(total+R(tail))
return narrow(enclosure.exp()), tail
def decimal_interval(text):
# Exact parsing, including a possible exponent. No rounded decimal to QQ.
text = str(text)
center = Fraction(text)
mantissa, exponent = (text.lower().split('e')+[0])[:2] if 'e' in text.lower() else (text,0)
places = len(mantissa.split('.')[1]) if '.' in mantissa else 0
ulp = Fraction(10)**(int(exponent)-places)
return QQ(center.numerator)/center.denominator, QQ(ulp.numerator)/ulp.denominator
def contains_ball(text, ball):
center, ulp = decimal_interval(text)
lo, hi = endpoints(ball)
assert center-ulp <= lo <= hi <= center+ulp, ('Written interval misses enclosure',text)
return max(abs(lo-center),abs(hi-center))/ulp
def run(stored=False):
controls = {}
for name,a,b,answer in [('unit',1,1,1),('scale',2,2,2)]:
v=agm_bracket(a,b)
assert v.is_finite()
lo,hi=endpoints(v)
assert lo <= QQ(answer) <= hi
assert hi-lo < QQ(1)/10**170
controls[name]={'known':answer,'ball':str(v)}
# Independent arithmetic and geometric mean check; no built-in AGM or K.
agm=narrow(agm_bracket(R(1),1/R(2).sqrt()))
elliptic=narrow(R.pi()/(2*agm))
gamma_two=narrow(4*elliptic**2/R.pi())
quarter_gamma=narrow(R(QQ(1)/4).gamma()**4/(4*R.pi()**2))
assert gamma_two.overlaps(quarter_gamma), 'Quarter-Gamma/AGM disagreement'
gen=UniformizationRadius()
coefficients=prepare_coefficients()
values={}
rows=[]
min_accuracy=100000
max_ulp=QQ(0)
previous=None
for params in gen.enumerate():
n=int(params['n'])
ball=narrow(gen.value(params,100))
independent,tail=zeta_radius(n,coefficients)
assert ball.overlaps(independent), ('Gamma/zeta disagreement',n)
if n==2: assert ball.overlaps(gamma_two), 'AGM special-case disagreement'
# The series has positive coefficients and decreases with n.
assert ball > 1
if previous is not None: assert previous > ball
previous=ball
text=to_text(ball,100)
assert len(text.replace('.','').lstrip('0'))==100
max_ulp=max(max_ulp,contains_ball(text,ball),contains_ball(text,independent))
min_accuracy=min(min_accuracy,int(ball.accuracy()))
values[str(n)]=text
lo,hi=endpoints(ball)
rows.append({'n':n,'decimal':text,'gamma_ball':str(ball),
'gamma_lower':str(lo),'gamma_upper':str(hi),
'accuracy_bits':int(ball.accuracy()),
'zeta_ball':str(independent),'log_series_tail_bound':str(tail)})
database={}
if stored:
doc=numberdb.table('T555')
numbers=doc['Numbers']
assert list(numbers)==list(values), 'Stored selection/order mismatch'
for n,entry in numbers.items():
text=entry['number'] if isinstance(entry,dict) else entry
independent,_=zeta_radius(int(n),coefficients)
contains_ball(text,independent)
if n=='2': contains_ball(text,gamma_two)
v=gen.verify(sample=None)
assert v.ok,str(v)
kdoc=numberdb.table('T25')
kentry=kdoc['Numbers']['1/2']
ktext=kentry['number'] if isinstance(kentry,dict) else kentry
contains_ball(ktext,elliptic)
database={'stored_rows_checked':len(numbers),'verify':str(v),
'stored_T25_lemniscatic_checked':True}
import importlib.metadata
try: package_version=importlib.metadata.version('numberdb')
except importlib.metadata.PackageNotFoundError: package_version='source checkout'
return {'table':'T555','skill_manifest':'agents/runs/20261027T175211Z-build-skills/manifest.json',
'skill_local_sha256':'e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c',
'skill_live_sha256':'e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c',
'sage_version':sage_version,'numberdb_version':package_version,
'count':len(rows),'working_bits':numberdb.bits(100,losing=128),
'minimum_gamma_accuracy_bits':min_accuracy,'check_bits':CHECK_BITS,
'zeta_terms':TERMS,'max_serialization_error_ulps':str(R(max_ulp)),
'max_written_length':max(map(len,values.values())),
'controls':controls,'agm_bracket':str(agm),'gamma_two_from_agm':str(gamma_two),
'gamma_two_from_quarter_gamma':str(quarter_gamma),
'all_gamma_zeta_overlaps':True,'all_written_intervals_contain_both_enclosures':True,
'strictly_decreasing_and_greater_than_one':True,'database':database,'rows':rows}
if __name__=='__main__':
key_stdin=os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1'
if key_stdin:numberdb.configure(api_key=sys.stdin.read().strip())
result=run(stored=('--stored' in sys.argv or key_stdin))
print(json.dumps(result))