back to table · edit · history · where entries came from · files · download
5362 bytes, as of the version from 2026-11-11 03:31 (current). Recorded here, not run.
"""Independent integral checks for T715; no generator code is imported.
Usage: sage -python checks.py [rows.json] [results.json]
Input is {"rows":[{"params":{"p":1,"v":"1/4"},"number":"..."},...]}
with NumberDB decimal interval encodings. The default is offline-rows.json.
The integral is a different implementation from the series / Euler transform /
beta coefficients used to generate entries. Both use Arb arithmetic, and both
rely on the same series-to-moment identity; this is not a separate library check.
Analytic quadrature and an explicit positive tail yield a second enclosure.
"""
import json
import math
import pathlib
import sys
import time
from fractions import Fraction
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from sage.rings.complex_arb import ComplexBallField
from sage.rings.real_mpfi import RealIntervalField
R = RealBallField(450)
C = ComplexBallField(450)
I = RealIntervalField(600)
def rational(text):
f = Fraction(str(text))
return QQ(f.numerator)/f.denominator
def decimal_bounds(text):
text = str(text).lower()
mantissa, _, exponent = text.partition('e')
places = len(mantissa.split('.')[1]) if '.' in mantissa else 0
ulp = QQ(10)**(int(exponent or 0)-places)
center = rational(text)
return center-ulp, center+ulp, ulp
def narrow(y):
return bool(y.is_finite() and R(y.rad()) < R(10)**-110)
def contained(text, y):
if not narrow(y):
return False
lo, hi, _ = decimal_bounds(text)
interval = I(y)
return bool(interval.lower() >= lo and interval.upper() <= hi)
def integral(p, v):
"""U_p(v) via the logarithmic moment after theta=theta_end exp(-t)."""
v = rational(v)
a = 2*R(abs(v)).sqrt()
theta = a.arcsin() if v > 0 else a.arcsinh()
norm = C(theta/a)/math.factorial(p-1)
A, th = C(a), C(theta)
def integrand(t, analytic):
z = th*(-t).exp()
kernel = z.sin() if v > 0 else z.sinh()
return norm*(-t).exp()*(A/kernel).log(analytic=analytic)**(p-1)
L = 420
y = C.integral(integrand, 0, L, abs_tol=R(10)**-120, rel_tol=R(10)**-120)
# log(a/kernel(theta exp(-t))) <= t+1, theta/a < 2.
tail = 2*R(-L).exp()*sum(R(L+1)**k/math.factorial(k) for k in range(p))
assert y.real().is_finite() and y.imag().is_finite() and y.imag().contains_zero()
return y.real().add_error(tail)
def main(input_path, output_path):
data = json.loads(pathlib.Path(input_path).read_text())
records = data['rows']
comparisons, failures = [], []
controls = []
start = time.time()
for row in records:
p = int(row['params']['p']); v = row['params']['v']
y = integral(p,v)
ok = contained(row['number'],y)
center = R(rational(row['number'])); ulp = decimal_bounds(row['number'])[2]
comparisons.append({'params':row['params'],'integral_ball':str(y),
'radius':str(y.rad()),'stored_contains_integral':ok,
'residual_in_stored_ulps':str((center-y)/R(ulp))})
if not ok: failures.append({'params':row['params'],'reason':'stored interval does not contain the narrow integral enclosure'})
if p==1:
a=2*R(abs(rational(v))).sqrt()
known=(a.arcsin() if rational(v)>0 else a.arcsinh())/a
controls.append(bool(narrow(known) and narrow(y) and y.overlaps(known)))
if p==2 and rational(v)==QQ(1)/4:
controls.append(bool(y.overlaps(R.pi()*R(2).log()/2)))
print('ROW_JSON='+json.dumps(comparisons[-1]),flush=True)
reference=records[0]; y=integral(int(reference['params']['p']),reference['params']['v'])
_,_,ulp=decimal_bounds(reference['number'])
negative_controls={
'missing_initial_term':not contained(reference['number'],y-1),
'wrong_sign':not contained(reference['number'],-y),
'five_last_place_units':not contained(reference['number'],y+5*R(ulp)),
'vacuous_radius':not contained(reference['number'],y.add_error(100)),
'nan':not contained(reference['number'],R('nan')),
}
result={'table':'T715','checked_entries':len(records),'total_entries':len(records),
'failures':failures,'known_answer_control':all(controls) and len(controls)==5,
'negative_control_rejected':all(negative_controls.values()),
'negative_controls':negative_controls,'known_answer_controls':controls,
'comparisons':comparisons,'seconds':time.time()-start,
'method':'450-bit Arb analytic quadrature on [0,420] plus explicit exponential tail',
'skill_manifest':'skill-manifest.json',
'skill_bundle_sha256':'d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab',
'limitations':'Independent formula and implementation; shared Arb arithmetic and series-to-moment identity. This is builder evidence, not a critic verdict.'}
pathlib.Path(output_path).write_text(json.dumps(result,indent=2))
assert not failures and result['known_answer_control'] and result['negative_control_rejected']
return result
if __name__=='__main__':
here=pathlib.Path(__file__).parent
inp=sys.argv[1] if len(sys.argv)>1 else here/'offline-rows.json'
out=sys.argv[2] if len(sys.argv)>2 else here/'check-results.json'
main(inp,out)