back to table · edit · history · where entries came from · files · download
4059 bytes, as of the version from 2026-10-29 11:13 (current). Recorded here, not run.
"""Check T607's repaired one-value example without website writes.
Run: sage -python repair-checks.py
Keep document-proposed.json, generate.py and skill-evidence.json in this directory.
The existing stored values are compared with the unchanged generator; this is
consistency checking, not a replacement for the independent critique. The new
example is also checked against a direct sum with a rigorous tail bound.
"""
import contextlib, hashlib, importlib.metadata, io, json, platform
from pathlib import Path
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.integer_ring import ZZ
from sage.env import SAGE_VERSION
from sage.rings.real_arb import RealBallField
from generate import WittenZeta
here=Path(__file__).resolve().parent
doc=json.loads((here/'document-proposed.json').read_text())
skill=json.loads((here/'skill-evidence.json').read_text())
g=WittenZeta()
selected=[{'algebra':a,'m':m} for a,rows in doc['Numbers'].items() for m in rows]
assert list(g.enumerate())==selected
checks=[]
for params in selected:
decimal=doc['Numbers'][params['algebra']][params['m']]
assert '.' in decimal and 'e' not in decimal.lower()
whole,fraction=decimal.split('.')
unit=QQ(1)/ZZ(10)**len(fraction)
midpoint=QQ(ZZ(whole+fraction))*unit
ball=g.value(params,100)
assert ball.is_finite() and ball.accuracy()>=numberdb.bits(100)
lo,hi=ball.endpoints()
assert lo>midpoint-unit and hi<midpoint+unit
checks.append({'params':params,'accuracy_bits':int(ball.accuracy()),'stored_interval_contains_ball':True})
# Execute the exact proposed visible snippet.
namespace={}
captured=io.StringIO()
with contextlib.redirect_stdout(captured):
exec(compile(doc['Programs']['Sage']['code'],'Programs/Sage','exec'),namespace)
params={'algebra':'G2','m':'5'}
x=namespace['g'].value(params,100)
high=g.value(params,170)
assert x.is_finite() and high.is_finite()
assert x.accuracy()>=numberdb.bits(100) and high.accuracy()>=numberdb.bits(170)
assert x.overlaps(high)
# Independent normalization check from positive representation dimensions.
# P(a,b)=ab(a+b)(a+2b)(a+3b)(2a+3b) >=2*a**5*b and >=18*a*b**5.
# Union bounding a>L or b>L and using integrals for the positive tails gives
# T <=120**s*(2**(-s)+18**(-s))*(1+1/(s-1))*L**(1-5*s)/(5*s-1).
# All arguments here are exact integers/rationals, enclosed before evaluation.
field=RealBallField(700)
def dimension(a,b):
return QQ(a*b*(a+b)*(a+2*b)*(a+3*b)*(2*a+3*b))/120
assert [dimension(1,1),dimension(2,1),dimension(1,2)]==[1,7,14]
assert (field(2).zeta()-field.pi()**2/6).contains_zero()
L=32; s=10
partial=sum((field(dimension(a,b))**(-s) for a in range(1,L+1) for b in range(1,L+1)),field(0))
tail=QQ(120)**s*(QQ(2)**(-s)+QQ(18)**(-s))*(1+QQ(1)/(s-1))*QQ(L)**(1-5*s)/(5*s-1)
assert partial.is_finite() and partial.rad()<QQ(1)/ZZ(10)**190
lo=partial.lower(); hi=(partial+field(tail)).upper()
assert x.lower()>lo and x.upper()<hi
assert not (x+field('1e-40')).overlaps(field(lo).union(field(hi)))
report={
'table':'T607','skill_manifest':skill['manifest'],'skill_sha256':{v['source']:v['sha256'] for v in skill['versions']},
'generator_sha256':hashlib.sha256((here/'generate.py').read_bytes()).hexdigest(),
'versions':{'sage':SAGE_VERSION,'python':platform.python_version(),'numberdb':importlib.metadata.version('numberdb')},
'stored_values':checks,'enumeration_unchanged':True,
'example':{'params':params,'printed_output':captured.getvalue().strip(),'accuracy_bits':int(x.accuracy()),'higher_precision_accuracy_bits':int(high.accuracy()),'higher_precision_overlaps':True,'direct_sum_bound':str(field(tail)),'direct_sum_encloses_example':True,'negative_control_rejected':True,'argument_uncertainty':'Integer m=5 and symbolic G2 are exact; rational coefficients and pi are enclosed by Arb.','limitation':'The independent direct sum confirms normalization within its stated bound; the 100-digit ball uses the original generator, with higher-precision consistency checking.'},
'new_stored_values':0,
}
print(json.dumps(report,indent=2))