back to table · edit · history · where entries came from · files · download
7062 bytes, as of the version from 2026-11-11 08:15 (current). Recorded here, not run.
"""Independent build checks for T714, with resumable numerical evidence.
python checks.py offline-rows.json check-results.json
python checks.py stored-rows.json stored-check-results.json --reference check-results.json
Requires mpmath. No generator import; sources CGLXZ (2.5), definition 2.1.
The reference option reuses unchanged quadrature values by source hash and
parameter identity, then tests actual stored intervals and identities afresh.
This is builder evidence, never an independent critic's verdict.
"""
import argparse,hashlib,json,math,pathlib
import mpmath as mp
def rational(text):
if '/' in text:
a,b=text.split('/');return mp.mpf(a)/mp.mpf(b)
return mp.mpf(text)
def endpoint(key):
a=mp.log((1+mp.sqrt(5))/2)
return {'logphi':a,'2logphi':2*a}[key]
def integral(m,n,key,dps=140):
with mp.workdps(dps):
x=endpoint(key)
def f(v):
t=x*mp.exp(-v)
return -t*mp.log(2*mp.sinh(t/2))**(m-1)*mp.log(2*mp.cosh(t/2))**(n-1)
return +mp.quad(f,[0,1,4,16,64,256,mp.inf])
def compare(lo,hi,v,stored=False):
if not all(mp.isfinite(z) for z in [lo,hi,v]) or lo>hi:return False
scale=abs(v) or mp.mpf(1)
if hi-lo>scale*mp.mpf('1e-98'):return False
return lo<=v<=hi if stored else abs((lo+hi)/2-v)<scale*mp.mpf('1e-125')
def main():
ap=argparse.ArgumentParser();ap.add_argument('input');ap.add_argument('output');ap.add_argument('--reference');args=ap.parse_args()
mp.mp.dps=180; raw=pathlib.Path(args.input).read_bytes();rows=json.loads(raw)
codehash=hashlib.sha256(pathlib.Path(__file__).read_bytes()).hexdigest(); fp=hashlib.sha256(raw+codehash.encode()).hexdigest()
out=pathlib.Path(args.output);refs={}
if args.reference:
ref=json.loads(pathlib.Path(args.reference).read_text());assert ref['program_sha256']==codehash
assert not ref['failures'] and ref['checked_entries']==44
refs={(c['params']['m'],c['params']['n'],c['params']['x']):c for c in ref['checks']}
data={'fingerprint':fp,'program_sha256':codehash,'input_sha256':hashlib.sha256(raw).hexdigest(),'skill_bundle_sha256':'d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab','checked_entries':0,'total_entries':len(rows),'failures':[],'known_answer_control':False,'negative_control_rejected':False,'mpmath_version':mp.__version__,'quadrature_dps':140,'second_precision_dps':175,'checks':[],'reference_file':args.reference}
if out.exists():
old=json.loads(out.read_text())
if old.get('fingerprint')==fp:data=old
def save():out.write_text(json.dumps(data,indent=2))
x=endpoint('2logphi');v=integral(1,2,'2logphi');exact=-x*x/4-mp.polylog(2,-mp.exp(-x))-mp.pi**2/12
data['known_answer_control']=bool(abs(v-exact)<mp.mpf('1e-130') and abs(integral(1,1,'logphi')+endpoint('logphi'))<mp.mpf('1e-130'))
tiny=mp.mpf('1e-100')
tests={'wrong_sign':not compare(-v-tiny,-v+tiny,v,True),'shifted':not compare(v+10*tiny,v+12*tiny,v,True),'nan':not compare(mp.nan,mp.nan,v,True),'unbounded':not compare(mp.ninf,mp.inf,v,True),'vacuous':not compare(v-1,v+1,v,True)}
data['negative_controls']=tests;data['negative_control_rejected']=all(tests.values())
data['known_control_details']={'H_1_2_2a_relative_error':mp.nstr(abs(v-exact)/abs(v),12),'H_1_1_a':'-log(phi)'}
done={(c['params']['m'],c['params']['n'],c['params']['x']) for c in data['checks']}
for row in rows:
p=row['params'];m,n,key=int(p['m']),int(p['n']),p['x'];ident=(m,n,key)
if ident in done:continue
lo,hi=rational(row['lower']),rational(row['upper']);v=mp.mpf(refs[ident]['value']) if ident in refs else integral(m,n,key)
ok=compare(lo,hi,v,row.get('stored',False))
item={'params':{'m':m,'n':n,'x':key},'value':mp.nstr(v,145),'relative_midpoint_error':mp.nstr(abs((lo+hi)/2-v)/abs(v),12),'relative_width':mp.nstr((hi-lo)/abs(v),12),'pass':bool(ok)}
if ident in [(1,9,'logphi'),(5,5,'logphi'),(8,2,'logphi'),(8,2,'2logphi')]:
e=mp.mpf(refs[ident]['second_precision_relative_difference']) if ident in refs else abs(v-integral(m,n,key,175))/abs(v)
item['second_precision_relative_difference']=mp.nstr(e,12);ok=ok and e<mp.mpf('1e-130')
if (m,n)==(1,2):
xx=endpoint(key);expect=-xx*xx/4-mp.polylog(2,-mp.exp(-xx))-mp.pi**2/12
item['dilog_control']=bool(abs(v-expect)<mp.mpf('1e-130'));ok=ok and item['dilog_control']
item['pass']=bool(ok)
if not ok:data['failures'].append(p)
data['checks'].append(item);data['checked_entries']=len(data['checks']);save()
print(data['checked_entries'],p,'PASS' if ok else 'FAIL',flush=True)
values={(int(r['params']['m']),int(r['params']['n']),r['params']['x']):((rational(r['lower'])+rational(r['upper']))/2,(rational(r['upper'])-rational(r['lower']))/2) for r in rows}
identities=[]
# CGLXZ (2.5), z=1/4. Direct central-binomial/harmonic series, 400 terms.
terms=[];h=mp.mpf(0)
for j in range(1,401):
h+=mp.mpf(1)/(2*j-1)+mp.mpf(1)/(2*j)
terms.append(mp.mpf(math.comb(2*j,j))*(-1)**j*h/mp.mpf(4)**(2*j+1))
for p in range(1,9):
lhs=mp.fsum(t/(2*j+1)**p for j,t in enumerate(terms,1))
mid,rad=values[(p,2,'2logphi')];rhs=mid/2;err=rad/2
for l in range(1,p+1):
mid,rad=values[(l,p-l+2,'logphi')];c=math.comb(p-1,l-1);rhs-=c*mid;err+=c*rad
rhs*=mp.mpf((-1)**(p-1))/math.factorial(p-1);err/=math.factorial(p-1)
residual=abs(lhs-rhs);ok=residual<err+mp.mpf('1e-125')
identities.append({'name':'harmonic_binomial','p':p,'residual':mp.nstr(residual,12),'propagated_interval_radius':mp.nstr(err,12),'pass':bool(ok)})
# Duplication with independently recomputed pure log-sinh boundaries.
for r in range(1,9):
lhs=integral(r+1,1,'2logphi');rhs=integral(r+1,1,'logphi');err=mp.mpf(0)
for j in range(r):
mid,rad=values[(j+1,r-j+1,'logphi')];c=math.comb(r,j);rhs+=c*mid;err+=c*rad
residual=abs(lhs-2*rhs);ok=residual<2*err+mp.mpf('1e-125')
identities.append({'name':'duplication','r':r,'residual':mp.nstr(residual,12),'propagated_interval_radius':mp.nstr(2*err,12),'pass':bool(ok)})
# Incomplete-beta generating function: independent integration and betainc.
xx=endpoint('logphi');alpha=mp.mpf(1)/3;beta=mp.mpf(2)/5;u=mp.tanh(xx/2)**2
direct=mp.quad(lambda t:(2*mp.sinh(t/2))**alpha*(2*mp.cosh(t/2))**beta,[0,xx])
via_beta=2**(alpha+beta)*mp.betainc((alpha+1)/2,-(alpha+beta)/2,0,u)
identities.append({'name':'beta_generating_function','alpha':'1/3','beta':'2/5','x':'logphi','residual':mp.nstr(abs(direct-via_beta),12),'pass':bool(abs(direct-via_beta)<mp.mpf('1e-130'))})
data['identities']=identities
data['failures'] += [i for i in identities if not i['pass']];save()
assert data['known_answer_control'] and data['negative_control_rejected'] and not data['failures'] and data['checked_entries']==len(rows)
print('All entries and identities passed',flush=True)
if __name__=='__main__':main()