final_local_checks.py

back to table · edit · history · where entries came from · files · download

1401 bytes, as of the version from 2026-11-01 11:37 (current). Recorded here, not run.

import json,contextlib,io
from pathlib import Path
import numberdb.sage as numberdb
from sage.rings.real_arb import RealBallField
from checks import frac, recorded_ball
from generate import determinant, BroadhurstMellit
import dry_run
import mpmath as mp
root=Path(__file__).resolve().parent
assert dry_run.main([str(root/'generate.py')])==0
ns={}
with contextlib.redirect_stdout(io.StringIO()):
    exec((root/'program.py').read_text(),ns)
R=RealBallField(800)
for n in range(3,23):
    approx=ns['D'](n)
    real=determinant(n,180)
    # The program's rounded 100-digit output must enclose the proven ball.
    assert R(real) in recorded_ball(mp.nstr(approx,100),R),(n,'program')
print('Programs snippet: all 20 rounded outputs enclose higher-precision balls')
# I0(t)<=exp(t), K0(t)<=sqrt(pi/(2t))*exp(-t). For T>=1:
# t^r I0(t)^a K0(t)^b <= (pi/2)^(b/2) t^r exp(-(b-a)t).
# Integrate the right side exactly as an exponential times a finite sum.
for dps in (70,100):
 mp.mp.dps=dps
 T=3*(dps+40); worst=mp.mpf(0)
 for n in range(3,23):
  m=(n-1)//2
  for a in range(1,m+1):
   b=n-a;decay=b-a
   for j in range(1,m+1):
    r=2*j-1
    tail=(mp.pi/2)**(mp.mpf(b)/2)*mp.exp(-decay*T)*sum(mp.factorial(r)/mp.factorial(r-h)*mp.mpf(T)**(r-h)/mp.mpf(decay)**(h+1) for h in range(r+1))
    worst=max(worst,tail)
 print('Analytic majorant for every omitted moment tail at',dps,'digits:',mp.nstr(worst,10))