back to table · edit · history · where entries came from · files · download
10762 bytes, as of the version from 2026-10-29 06:33 (current). Recorded here, not run.
"""Independent checks for T602; run sage -python checks.py.
Default checks generated values without network access. --stored additionally
reads the authenticated draft and reruns the identities on its written intervals.
Set NUMBERDB_API_KEY for draft reads, or NUMBERDB_KEY_FROM_STDIN=1.
The spectral tests use orthonormal Laplacian eigenfunctions, not the generator's
hyperbolic sums. Parseval bounds the omitted squared projection mass, and every
omitted eigenvalue is bounded below. This is a coarse independent enclosure,
not evidence of 100-digit accuracy. Certified output precision instead follows
from Arb and the generator's explicitly enclosed exponentially small tails.
A known exact square eigenfunction integral controls the projection formula.
The circle's exact polynomial solution controls the polynomial Poisson tests.
Archive policy: skill-manifest.json, local/live SHA-256
28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199.
"""
import os,sys,json,time,warnings
warnings.filterwarnings("ignore",message="Resolving lazy import Rings during startup")
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.rings.polynomial.polynomial_ring_constructor import PolynomialRing
from numberdb._write import to_text
from check import exactness,measure,names_its_rings
from flatten import to_records
from generate import TorsionalRigidity,DOMAINS,NORMALIZATIONS,RECTANGLES,ELLIPSES,compute,area,odd_sum
F=RealBallField(700)
pi=F.pi()
def decimal_rational(text):
text=text.rstrip('?')
if 'e' in text.lower():
text,exponent=text.lower().split('e');exponent=int(exponent)
else:
exponent=0
if '.' in text:
left,right=text.split('.');exponent-=len(right);text=left+right
return QQ(int(text))*QQ(10)**exponent
def written_ball(text):
text=text.rstrip('?')
exponent=int(text.lower().split('e')[1]) if 'e' in text.lower() else 0
base=text.lower().split('e')[0]
places=len(base.split('.')[1]) if '.' in base else 0
return F(decimal_rational(text),QQ(10)**(exponent-places))
def contains(outer,inner):
return outer.lower() <= inner.lower() and inner.upper() <= outer.upper()
def narrow(value,places=98):
assert value.is_finite() and value>0
assert F(value.rad()) < F(10)**(-places), str(value)
def agree(a,b,places=98):
narrow(a,places);narrow(b,places)
assert a.overlaps(b),(str(a),str(b))
def spectral_rectangle(r,n=256):
# phi_mn = 2/sqrt(r)*sin(m*pi*x/r)*sin(n*pi*y).
# Squared integral = 64*r/(pi^4*m^2*n^2), m,n odd.
total=F(0);mass=F(0)
for m in range(1,n+1,2):
for k in range(1,n+1,2):
b2=64*F(r)/(pi**4*m*m*k*k)
total+=b2/(pi**2*(F(m*m)/(r*r)+k*k))
mass+=b2
remainder=(F(r)-mass)/(pi**2*(n+1)**2/max(F(1),F(r*r)))
assert remainder>0
return total+F(remainder.upper()/2,remainder.upper()/2),remainder
def spectral_triangle(n=256):
# Antisymmetric normalized sine modes on 0<y<x<1.
# m odd, k even enumerate each unordered pair exactly once.
total=F(0);mass=F(0)
for m in range(1,n+1,2):
for k in range(2,n+1,2):
b2=64*F(k*k)/(pi**4*m*m*(m*m-k*k)**2)
total+=b2/(pi**2*(m*m+k*k));mass+=b2
remainder=(F(1)/2-mass)/(pi**2*(n+1)**2)
assert remainder>0
return total+F(remainder.upper()/2,remainder.upper()/2),remainder
def polynomial_checks(values):
ring=PolynomialRing(QQ,names=('x','z'));x,z=ring.gens()
u=(1-x*x-z*z)/4
assert -(u.derivative(x,2)+u.derivative(z,2))==1
# Radial integration of u gives pi/8.
agree(values['disk','unit-length'],pi/8)
triangle=QQ(3)/2*z*(x-z)*(1-x-z) # y=sqrt(3)*z
assert -(triangle.derivative(x,2)+triangle.derivative(z,2)/3)==1
assert triangle(z=0)==0 and triangle(x=z)==0 and triangle(x=1-z)==0
int_x=triangle.integral(x)
int_z=(int_x(x=1-z)-int_x(x=z)).integral(z)
integral=(int_z(z=QQ(1)/2)-int_z(z=0)).constant_coefficient()
assert integral==QQ(1)/320
agree(values['equilateral-triangle','unit-length'],F(3).sqrt()*integral)
for p,q in ((1,1),)+ELLIPSES:
r=QQ(p)/q
u=r*r/(2*(r*r+1))*(1-x*x/(r*r)-z*z)
assert -(u.derivative(x,2)+u.derivative(z,2))==1
assert u == -r*r/(2*(r*r+1))*(x*x/(r*r)+z*z-1)
# On the unit disk int(1-X^2-Y^2)=pi/2; Jacobian is r.
expected=F(r)*pi/2*F(r*r/(2*(r*r+1)))
domain='disk' if r==1 else 'ellipse-%d-%d'%(p,q)
agree(values[domain,'unit-length'],expected)
def sector_check(values):
# Sine separation in 0<theta<alpha gives
# T=2*alpha/pi^2 sum_{n odd} 1/[n^2*(n*pi/alpha+2)^2].
# Partial fractions telescope when alpha=pi or 2*pi.
# For s=2*alpha/pi, sum 1/[n^2(n+s)^2]
# = pi^2/(4*s^2) - sum_{odd n<s}1/n^2/s^2
# - 2*sum_{odd n<s}1/n/s^3.
for s,domain in [(2,'half-disk'),(4,'slit-disk')]:
finite1=sum((QQ(1)/k for k in range(1,s,2)),QQ(0))
finite2=sum((QQ(1)/(k*k) for k in range(1,s,2)),QQ(0))
series=pi*pi/(4*s*s)-F(finite2)/(s*s)-2*F(finite1)/(s**3)
alpha=F(s)*pi/2
expected=2*alpha**3/pi**4*series
agree(values[domain,'unit-length'],expected)
def identity_checks(values):
for domain in DOMAINS:
for norm in NORMALIZATIONS:
narrow(values[domain,norm])
a=area(domain,F)
agree(values[domain,'unit-area']*a*a,values[domain,'unit-length'],96)
if domain!='disk':
assert values[domain,'unit-area'] < 1/(8*pi)
agree(values['rectangle-1-1','unit-length'],values['rectangle-1-1','unit-area'])
polynomial_checks(values);sector_check(values)
# Rotating a rectangle and scaling its shorter side gives r^4*T(1/r).
for p,q in RECTANGLES:
r=F(QQ(p)/q)
inverse=1/r
exchanged=r**4*(inverse/12-16/pi**5*odd_sum(F,inverse,terms=520))
agree(values['rectangle-%d-%d'%(p,q),'unit-length'],exchanged)
def main(stored=False):
start=time.monotonic();gen=TorsionalRigidity()
raw={(p['domain'],p['normalization']):gen.value(p,100) for p in gen.enumerate()}
assert not exactness(raw) and not names_its_rings(Path(__file__).with_name('generate.py'))
assert len(raw)==38 and len(DOMAINS)==19
evidence={'table':'T602','skill_manifest':'agents/runs/20261029T055510Z-build-skills/manifest.json',
'skill_sha256':'28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199',
'numberdb_version':numberdb.__version__,'working_bits':501,'repeat_working_bits':665,'output_digits':100,
'entries':38,'minimum_relative_accuracy_bits':min(int((abs(F(v))/F(v.rad())).log(2).lower().floor()) for v in raw.values()),
'maximum_ball_radius':str(max(v.rad() for v in raw.values())),
'measure_raw':measure(raw),'spectral_checks':[]}
from sage.env import SAGE_VERSION
evidence['sage_version']=SAGE_VERSION
q=(-pi*161).exp()
evidence['maximum_correction_tail_bound']=str((q/(F(161)**5*(1-q)*(1-(-2*pi).exp()))).upper())
text={key:to_text(v,digits=100) for key,v in raw.items()}
values={key:written_ball(v) for key,v in text.items()}
evidence['measure_written']=measure(text)
for (domain,norm),v in raw.items():
hi=compute(domain,norm,665,120)
agree(F(v),hi)
assert contains(values[domain,norm],hi)
identity_checks(values)
# Control: squared integral of phi_11 on the unit square is 64/pi^4.
control=F(2)*(F(2)/pi)**2
agree(control**2,F(64)/pi**4)
for p,q in RECTANGLES:
domain='rectangle-%d-%d'%(p,q)
enclosure,tail=spectral_rectangle(QQ(p)/q)
assert enclosure.is_finite() and F(enclosure.rad())<F(1)/10**6
assert contains(enclosure,raw[domain,'unit-length'])
evidence['spectral_checks'].append({'domain':domain,'tail_upper':str(tail.upper()),'cutoff':256})
enclosure,tail=spectral_triangle()
assert enclosure.is_finite() and F(enclosure.rad())<F(1)/10**6
assert contains(enclosure,raw['right-isosceles-triangle','unit-length'])
evidence['spectral_checks'].append({'domain':'right-isosceles-triangle','tail_upper':str(tail.upper()),'cutoff':256})
evidence['oeis_checks']=[]
for seq,domain in [('180314','right-isosceles-triangle'),('180310','half-disk'),('180311','slit-disk')]:
rows=[]
for line in Path(__file__).with_name('oeis-A'+seq+'.txt').read_text().splitlines():
if line.strip() and not line.startswith('#'):
index,digit=line.split()[:2];rows.append((int(index),digit))
assert rows[0][0]==0
# The three source examples put every digit after the decimal point.
known='0.'+''.join(v for _,v in rows)
box=written_ball(known)
assert contains(box,4*F(raw[domain,'unit-length']))
evidence['oeis_checks'].append({'sequence':'A'+seq,'decimal_places':len(rows),'scale':'J=4T'})
if stored:
doc=numberdb.table('T602')
records=to_records(doc)
assert isinstance(records,list) and len(records)==38
actual={(r['params']['domain'],r['params']['normalization']):written_ball(r['number']) for r in records}
assert list(actual)==list(raw)
identity_checks(actual)
for key,v in raw.items():assert contains(actual[key],F(v))
for p,q in RECTANGLES:
key=('rectangle-%d-%d'%(p,q),'unit-length')
box,_=spectral_rectangle(QQ(p)/q)
assert contains(box,actual[key])
box,_=spectral_triangle();assert contains(box,actual['right-isosceles-triangle','unit-length'])
evidence['stored_readback']='all 38 intervals, identities and spectral checks passed'
evidence['elapsed_seconds']=round(time.monotonic()-start,3)
evidence['checks_passed']=['all finite and positive','150/200 working decimal-digit agreement',
'all written intervals contain higher-precision enclosures','all 19 scale conversions',
'Saint-Venant bound on all nondisk domains','square convention equality',
'exact Poisson polynomial and boundary checks','sector sine-series telescoping',
'all 10 rectangle axis exchanges','11 independent spectral enclosures','3 OEIS engineering constants']
evidence['values']=[{'params':{'domain':k[0],'normalization':k[1]},'number':v} for k,v in text.items()]
print(json.dumps(evidence,indent=2))
if __name__=='__main__':
if os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1':
key=sys.stdin.read().strip()
if '=' in key and key.split('=',1)[0].isidentifier():key=key.split('=',1)[1].strip().strip('\"\'')
numberdb.configure(api_key=key)
main('--stored' in sys.argv or os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1')