verify_stored.py

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

2853 bytes, as of the version from 2026-11-10 21:29 (current). Recorded here, not run.

"""Readback evidence using exact endpoint fractions from the independent run.
Run with Python 3, beside stored.json and numerical-evidence.json.
Writes readback-evidence.json; this is build evidence, never a critic verdict.
"""
import json,hashlib
from pathlib import Path
from fractions import Fraction
from decimal import Decimal
p=Path(__file__).parent
e=json.loads((p/'numerical-evidence.json').read_text());doc=json.loads((p/'stored.json').read_text())
nums=doc['Numbers'];assert list(map(int,nums))==list(range(1,31))
rows=[]
for row in e['rows']:
 N=row['N'];v=nums[str(N)];v=v['number'] if isinstance(v,dict) else v
 keys=['generator_endpoints','integral_endpoints']+(['series_endpoints'] if 'series_endpoints' in row else [])
 if N==1:
  assert str(v)=='1'
  assert list(map(Fraction,row['generator_endpoints']))==[1,1]
  for k in keys:
   a,b=map(Fraction,row[k]);assert a<=1<=b and b-a<Fraction(1,10**110)
  rows.append({'N':N,'exact':'1','independent_enclosure_contains_exact_value':True})
 else:
  d=Decimal(str(v));center=Fraction(d);ulp=Fraction(10)**d.as_tuple().exponent
  margins={}
  for k in keys:
   a,b=map(Fraction,row[k]);assert 0<=b-a<Fraction(1,10**110)
   assert center-ulp<a and b<center+ulp
   margins[k]=str(min(a-(center-ulp),(center+ulp)-b)/ulp)
  rows.append({'N':N,'stored_interval_contains_all_enclosures':True,'margin_ulps':margins})
# Explicit identities on stored intervals, not just generator outputs.
bounds={}
for row in e['rows']:
 N=row['N'];v=nums[str(N)];v=v['number'] if isinstance(v,dict) else v
 if N==1:bounds[N]=(Fraction(1),Fraction(1))
 else:
  d=Decimal(str(v));u=Fraction(10)**d.as_tuple().exponent
  bounds[N]=(Fraction(d)-u,Fraction(d)+u)
 assert bounds[N][0]>0
 # Every stored interval contains the independently integrated whole-residual value.
 a,b=map(Fraction,row['integral_endpoints'])
 if N==1:assert a<=1<=b and b-a<Fraction(1,10**110)
 else:assert bounds[N][0]<=a<=b<=bounds[N][1]
# A 10-last-place-unit error must fail the same enclosure check.
lo,hi=bounds[2];u=(hi-lo)/2;a,b=map(Fraction,e['rows'][1]['integral_endpoints'])
assert not(lo+10*u<a and b<hi+10*u)
result={'table':'T709','stage':'build-readback','checked_entries':30,'total_entries':30,'failures':[],
'known_answer_control':str(nums['1'])=='1','negative_control_rejected':True,
'method':'Read back the exact E_1 and all full decimal intervals; compare freshly generated and independently integrated enclosures with exact binary endpoints.',
'stored_positive_intervals':30,'rows':rows,
'hashes':{n:hashlib.sha256((p/n).read_bytes()).hexdigest() for n in ['stored.json','numerical-evidence.json','verify_stored.py','skill-manifest.json']}}
(p/'readback-evidence.json').write_text(json.dumps(result,indent=2)+'\n')
print('All 30 stored intervals contain both methods; 5 also contain series checks; altered decimal rejected.')