back to table · edit · history · where entries came from · files · download
2567 bytes, as of the version from 2026-10-24 21:16 (current). Recorded here, not run.
"""Precision checks for T467's prose repair.
Run: sage -python repair_checks.py
Requires the table's generate.py, checks.py, check.py, and the repair snapshot
T467-document.json in the same directory. This is read-only and uses no key.
The independent quadratures are numerical corroboration; only Arb closed-form
balls certify containment. Every one of the nine stored entries is checked.
"""
import json
from pathlib import Path
from decimal import Decimal
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.real_mpfr import RealField
import mpmath as mp
from generate import closed_form, REGIONS
from checks import independent, check_text
def rational(text):
f = Fraction(text)
return QQ(f.numerator)/f.denominator
def main():
document=json.loads(Path(__file__).with_name('T467-document.json').read_text())
assert document['Data properties']['digits']=='100'
entries=document['Numbers']
assert tuple(entries)==REGIONS
quadratures=independent(130)
R=RealBallField(600)
exact={'unit-interval':QQ(1)/3,'unit-ball-3':QQ(36)/35,'unit-sphere-2':QQ(4)/3}
radii=[]
ulps=[]
for region,entry in entries.items():
text=entry['number']
v=closed_form(region,100)
check_text(text,quadratures[region])
if region in exact:
assert rational(text)==v==exact[region]
print(region,'exact rational and quadrature PASS',flush=True)
continue
assert len(Decimal(text).as_tuple().digits)==100
center=rational(text)
ulp=QQ(10)**Decimal(text).as_tuple().exponent
assert v.is_finite() and v.rad()>0
assert R(v)>R(center-ulp) and R(v)<R(center+ulp)
higher=closed_form(region,160)
assert higher.is_finite() and higher.rad()<QQ(1)/10**175
assert R(higher)>R(center-ulp) and R(higher)<R(center+ulp)
assert v.overlaps(higher)
radii.append(v.rad())
error=abs(quadratures[region]-mp.mpf(text))/(mp.mpf(10)**Decimal(text).as_tuple().exponent)
ulps.append(error)
print(region,'100 significant digits; Arb containment PASS; quadrature ulps',mp.nstr(error,12),flush=True)
assert max(radii)<QQ(3)/10**124
print('maximum guard-80 Arb radius',RealField(50)(max(radii)),flush=True)
print('maximum quadrature midpoint error in ulps',mp.nstr(max(ulps),16),flush=True)
print('ALL_NINE_STORED_VALUES_PASS',flush=True)
if __name__=='__main__':
main()