back to table · edit · history · where entries came from · files · download
4749 bytes, as of the version from 2026-10-28 21:23. Recorded here, not run.
"""Independent checks on T591's downloaded database values.
Run: sage -python stored_checks.py
Keep readback.json, checks.py, check.py and generate.py in the same directory.
The numerical inputs are the strings read from the website, not generated
values. The defining polynomial is recomputed by the independent edge-parity
expansion in checks.py. The polynomial is freshly isolated at 600 bits.
"""
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.complex_interval_field import ComplexIntervalField
from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
from sage.rings.polynomial.complex_roots import complex_roots
from checks import even_subgraphs, from_even
from pathlib import Path
from fractions import Fraction
from decimal import Decimal
import json
def rational(f):
f = Fraction(f)
return QQ(f.numerator) / QQ(f.denominator)
def parse_part(s):
s=s.strip()
if s.startswith('['):
lo,hi=s[1:-1].split(',')
return rational(lo),rational(hi)
center = rational(s)
if '.' not in s and 'e' not in s.lower():
return center, center
ulp=QQ(10)**int(Decimal(s).as_tuple().exponent)
return center-ulp,center+ulp
def parsed(text):
parts=text.split(' + i * ')
if len(parts)==1:
parts.append('0')
assert len(parts)==2
return tuple(parse_part(s) for s in parts)
def main():
doc=json.loads(Path(__file__).with_name('readback.json').read_text())
field=ComplexIntervalField(650)
R=PolynomialRing(field,'t'); t=R.gen()
records=doc['Numbers']
assert len(records)==310
grouped={}
for record in records:
m,n,j=(int(record['params'][k]) for k in ('m','n','j'))
grouped.setdefault((m,n),[]).append((j,record))
result=[]
for (m,n),rows in grouped.items():
p=from_even(m,n,even_subgraphs(m,n))
isolated=complex_roots(p,min_prec=600,retval='interval')
boxes=[]; multiplicities=[]; used=set(); algebraic=[]
for j,record in rows:
ends=parsed(record['number'])
box=field(field.real_field()(*ends[0]),field.real_field()(*ends[1]))
matches=[k for k,(z,e) in enumerate(isolated) if box.overlaps(z)]
assert len(matches)==1, (m,n,j,'isolation matching')
k=matches[0]
assert k not in used
used.add(k)
z,e=isolated[k]
for (lo,hi),part in zip(ends,(z.real(),z.imag())):
lower,upper=(v.exact_rational() for v in part.endpoints())
if lo != hi:
assert lo <= lower and upper <= hi, (m,n,j,'written enclosure')
from sage.rings.qqbar import QQbar
a=QQbar.polynomial_root(p,z)
if ends[0][0]==ends[0][1]:
q=ends[0][0]
assert a+a.conjugate()==2*q
if ends[1][0]==ends[1][1]:
q=ends[1][0]
assert a-a.conjugate()==2*QQbar.gen()*q
algebraic.append(a)
assert record['comment']=='Multiplicity %s.' % e
assert p(box).contains_zero()
boxes.append(box);multiplicities.append(e)
for j in range(1,len(algebraic)):
a,c=algebraic[j-1],algebraic[j]
if boxes[j-1].real() < boxes[j].real():
continue
if a.conjugate()==c or (a==-a.conjugate() and c==-c.conjugate()):
assert boxes[j-1].imag() < boxes[j].imag()
else:
assert a.real() < c.real() or (a.real()==c.real() and a.imag()<c.imag())
assert [j for j,record in rows]==list(range(1,len(rows)+1))
assert len(used)==len(isolated)
assert sum(multiplicities)==p.degree()
assert all(sum(v.conjugate().overlaps(w) for w in boxes)==1 for v in boxes)
assert all(sum((1/v).overlaps(w) for w in boxes)==1 for v in boxes)
product=R(p.leading_coefficient())
for box,e in zip(boxes,multiplicities):
product *= (t-box)**e
assert all(p[k] in product[k] for k in range(p.degree()+1))
assert all(QQ(c.real().diameter()) < QQ(1)/10**60 and
QQ(c.imag().diameter()) < QQ(1)/10**60 for c in product)
row={'m':m,'n':n,'stored_roots':len(rows),'multiplicity_sum':int(sum(multiplicities)),
'every_written_enclosure_contains_certified_root':True,
'all_coefficients_reconstructed':True}
result.append(row)
print('PASS',json.dumps(row),flush=True)
print('STORED_EVIDENCE '+json.dumps({'table':'T591','entries':len(records),'shapes':result,
'skill_manifest':'agents/runs/20261028T210416Z-build-skills/manifest.json'}))
if __name__=='__main__':
main()