back to table · edit · history · where entries came from · files · download
5177 bytes, as of the version from 2026-11-10 22:53 (current). Recorded here, not run.
"""Read-only T710 precision-scope regression.
Run with SageMath and numberdb installed:
sage -python repair_check.py
Place live-document.json, polynomials.json and generate.py beside this script.
Prints REPAIR_CHECK_JSON for capture. No API or writes. Exact coefficient
checkpoints are reused; minimal polynomials are not rebuilt. Direct 512-bit
Arb reproduces the original check order; 640-bit MPFI sin/cos independently
checks enclosures. The two paths share Sage and the defining finite sum.
"""
import json,hashlib,sys,platform
from pathlib import Path
import numberdb.sage as numberdb
from sage.rings.integer_ring import ZZ
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from sage.rings.real_mpfi import RealIntervalField
from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
from sage.env import SAGE_VERSION
import generate
ROOT=Path(__file__).parent
R=RealBallField(512); I=RealIntervalField(640); ZX=PolynomialRing(ZZ,'x')
def arb(k,h):
return -sum(R(QQ(m)/k)*(R.pi()*QQ(m*h)/k).cot() for m in range(1,k))
def mpfi(k,h):
total=I(0)
for m in range(1,k):
angle=I.pi()*I(QQ(m*h)/k)
total-=I(QQ(m)/k)*angle.cos()/angle.sin()
return total
def finite_narrow(v):
return bool(v.is_finite() and v.rad_as_ball()<R(10)**-140)
def check(k,h,p):
v=arb(k,h); u=mpfi(k,h)
assert finite_narrow(v) and v.accuracy()>340
assert not u.is_NaN() and I(u.absolute_diameter())<I(10)**-180
mid=v.mid().exact_rational(); rad=v.rad().exact_rational()
enclosure=I(mid-rad,mid+rad)
assert (enclosure.lower() <= u.lower() and u.upper() <= enclosure.upper()), (k,h,'MPFI not contained')
L=int(ZZ(k).lcm(4)); a=next(a for a in range(h,L,k) if ZZ(a).gcd(L)==1)
sign=(-1)**((a-1)//2)
q=p if sign==1 else ZX([c*(-1)**(j+p.degree()) for j,c in enumerate(p.list())])
assert q(v).contains_zero() and (0 in q(u))
assert not (0 in (q+1)(u))
eps=I(QQ(1)/ZZ(2)**400)
assert q(u-eps)*q(u+eps)<0
bracket=I(u.lower()-eps.upper(),u.upper()+eps.upper())
assert not (0 in q.derivative()(bracket))
return {'k':k,'h':h,'radius':str(v.rad()),'radius_exact':str(rad),
'accuracy_bits':int(v.accuracy()),'ball':str(v),
'mpfi_width':str(u.absolute_diameter()),'mpfi_contained':True,
'signed_polynomial_root_isolated':True,'wrong_constant_rejected':True}
def main():
doc=json.loads((ROOT/'live-document.json').read_text())
values=json.loads((ROOT/'polynomials.json').read_text())
assert values=={str(k):r['number'] for k,r in doc['Numbers'].items()}
assert list(generate.BettinConreyMinimalPolynomials().enumerate())==[{'k':k} for k in range(3,25)]
assert set(values)=={str(k) for k in range(3,25)}
# Known nonzero values and deliberately invalid interval/sign/scale controls.
known={3:1/(3*I(3).sqrt()),4:I(QQ(1)/2),6:7/(3*I(3).sqrt()),8:1+I(2).sqrt()}
for k,u in known.items():
v=mpfi(k,1); assert v.overlaps(u) and I(v.absolute_diameter())<I(10)**-180
assert not finite_narrow(R('nan'))
assert not finite_narrow(R(0).add_error(R(1)))
for wrong in [ZX('2*x+1'),ZX('x-1'),ZX('4*x-1')]:assert not (0 in wrong(mpfi(4,1)))
rows=[]
for k in range(3,25):
p=ZX(values[str(k)])
for h in range(1,k):
if ZZ(h).gcd(k)==1:rows.append(check(k,h,p))
print('CHECKPOINT',k,json.dumps([r for r in rows if r['k']==k]),flush=True)
h1=[r for r in rows if r['h']==1]
def summary(group):
low=min(group,key=lambda r:r['accuracy_bits']); high=max(group,key=lambda r:QQ(r['radius_exact']))
return {'count':len(group),'minimum_accuracy_bits':low['accuracy_bits'],'min_at':[low['k'],low['h']],
'maximum_radius':high['radius'],'max_at':[high['k'],high['h']],
'below_505_bits':sum(r['accuracy_bits']<505 for r in group),
'over_original_radius':sum(QQ(r['radius_exact'])>=QQ(750)/ZZ(10)**154 for r in group)}
assert all(r['accuracy_bits']>=505 and QQ(r['radius_exact'])<QQ(750)/ZZ(10)**154 for r in h1)
result={'table':'T710','checked_entries':22,'total_entries':22,'checked_numerator_branches':len(rows),
'failures':[],'known_answer_control':True,'negative_control_rejected':True,
'h1':summary(h1),'all_reduced_numerators':summary(rows),'rows':rows,
'versions':{'sage':SAGE_VERSION,'numberdb':numberdb.__version__,'python':platform.python_version()},
'skill_manifest':'../20261110T224713Z-repair-skills/manifest.json',
'skill_bundle_sha256':'d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab',
'dependencies':{n:hashlib.sha256((ROOT/n).read_bytes()).hexdigest() for n in ['generate.py','polynomials.json','live-document.json','repair_check.py']},
'limitations':'Focused repair checks, not a fresh independent scientific verdict. Original exact coefficient checkpoints retained; no minpoly recomputation. MPFI and Arb share the finite sum definition and Sage infrastructure.'}
print('REPAIR_CHECK_JSON='+json.dumps(result),flush=True)
if __name__=='__main__':main()