back to table · edit · history · where entries came from · files · download
5034 bytes, as of the version from 2026-11-11 07:57 (current). Recorded here, not run.
"""Independent numerical checks for T713. Run with Python and mpmath:
python checks.py offline-rows.json check-results.json
python checks.py stored-rows.json stored-check-results.json
The result JSON is resumable and bound to both input bytes and this program.
This is build evidence, not an independent critic's verdict.
"""
import argparse,hashlib,json,math,pathlib,time
import mpmath as mp
def rational(text):
if '/' in text:
a,b=text.split('/'); return mp.mpf(a)/mp.mpf(b)
return mp.mpf(text)
def endpoints():
phi=(1+mp.sqrt(5))/2
return {'logphi':mp.log(phi),'2logphi':2*mp.log(phi),
'2logsilver':2*mp.asinh(1)}
def integral(n,k,key,dps=140):
with mp.workdps(dps):
x=endpoints()[key]; p=n-1-k
def f(s):
t=x*mp.exp(-s)
return -x**(k+1)*mp.exp(-(k+1)*s)*mp.log(2*mp.sinh(t/2))**p
return +mp.quad(f,[0,1,4,16,64,256,mp.inf])
def compare(lo,hi,v,stored=False):
if not all(mp.isfinite(x) for x in [lo,hi,v]) or lo>hi: return False
scale=abs(v)
if scale==0: scale=mp.mpf(1)
if hi-lo>scale*mp.mpf('1e-98'): return False
if stored: return lo<=v<=hi
return abs((lo+hi)/2-v) < scale*mp.mpf('1e-115')
def main():
ap=argparse.ArgumentParser(); ap.add_argument('input');ap.add_argument('output'); ap.add_argument('--reference')
args=ap.parse_args(); mp.mp.dps=170
raw=pathlib.Path(args.input).read_bytes(); rows=json.loads(raw)
fp=hashlib.sha256(raw+pathlib.Path(__file__).read_bytes()).hexdigest()
out=pathlib.Path(args.output)
references={}
if args.reference:
reference=json.loads(pathlib.Path(args.reference).read_text())
assert reference['program_sha256']==hashlib.sha256(pathlib.Path(__file__).read_bytes()).hexdigest()
assert not reference['failures'] and reference['checked_entries']==reference['total_entries']
references={tuple(c['params'].values()):c for c in reference['checks']}
data={'fingerprint':fp,'checked_entries':0,'total_entries':len(rows),'failures':[],
'known_answer_control':False,'negative_control_rejected':False,'checks':[],
'program_sha256':hashlib.sha256(pathlib.Path(__file__).read_bytes()).hexdigest(),
'reference_file':args.reference,'mpmath_version':mp.__version__,'quadrature_dps':140,'second_precision_dps':175}
if out.exists():
old=json.loads(out.read_text())
if old.get('fingerprint')==fp: data=old
def save(): out.write_text(json.dumps(data,indent=2))
x=endpoints()['2logphi']; simple=integral(3,2,'2logphi')
control=integral(3,1,'2logphi')
data['known_answer_control']=bool(abs(simple+x**3/3)<mp.mpf('1e-125') and abs(control-mp.zeta(3)/5)<mp.mpf('1e-125'))
data['negative_control_rejected']=bool(not compare(mp.mpf('0.2'),mp.mpf('0.3'),control) and not compare(control+1,control+2,control) and not compare(mp.nan,mp.nan,control) and not compare(-control-mp.mpf('1e-120'),-control+mp.mpf('1e-120'),control))
data['control_inputs']={'simple_n':3,'simple_k':2,'x':'2logphi','wrong_sign':True,'wide_interval':[0.2,0.3],'shifted_interval':True,'nan':True}
done={tuple(c['params'].values()) for c in data['checks']}
for row in rows:
p=row['params']; ident=tuple(p.values())
if ident in done: continue
n,k,key=int(p['n']),int(p['k']),p['x']
lo,hi=rational(row['lower']),rational(row['upper'])
v=mp.mpf(references[ident]['value']) if ident in references else integral(n,k,key)
ok=compare(lo,hi,v,row.get('stored',False))
err=abs((lo+hi)/2-v)/abs(v)
item={'params':p,'value':mp.nstr(v,145),'relative_midpoint_error':mp.nstr(err,12),'relative_width':mp.nstr((hi-lo)/abs(v),12),'pass':bool(ok)}
if (n,k,key) in [(10,0,'2logsilver'),(10,8,'2logsilver'),(9,0,'logphi'),(10,0,'2logphi')]:
e2=mp.mpf(references[ident]['second_precision_relative_difference']) if ident in references else abs(v-integral(n,k,key,175))/abs(v)
item['second_precision_relative_difference']=mp.nstr(e2,12)
ok=ok and e2<mp.mpf('1e-125'); item['pass']=bool(ok)
if n==2:
xx=endpoints()[key]; expected=mp.pi**2/6-mp.polylog(2,mp.exp(-xx))-xx**2/4
ok=ok and abs(v-expected)<mp.mpf('1e-125'); item['dilog_control']=bool(ok)
if k==1 and key=='2logphi':
F=mp.fsum(mp.mpf((-1)**j)/(j**n*math.comb(2*j,j)) for j in range(1,550))
expected=mp.factorial(n-2)/(-2)**(n-2)*F
ok=ok and abs(v-expected)<abs(v)*mp.mpf('1e-125'); item['inverse_binomial_control']=bool(ok)
if not ok: data['failures'].append(p)
data['checks'].append(item); data['checked_entries']=len(data['checks']); save()
print(data['checked_entries'],p,'PASS' if ok else 'FAIL',flush=True)
assert data['known_answer_control'] and data['negative_control_rejected']
assert not data['failures'] and data['checked_entries']==len(rows)
print('All checks passed',flush=True)
if __name__=='__main__': main()