back to table · edit · history · where entries came from · files · download
8294 bytes, as of the version from 2026-11-10 20:59 (current). Recorded here, not run.
"""Executable build checks for T708. This is not an independent actor verdict.
sage -python checks.py > numerical-evidence.json
Keep generate.py and integral_kernel.py beside this file. The kernel is checked
by a period integral with an exact analytic remainder, not by cotangent sums.
All 465 symmetric Gram entries and every one of 30 corrected norms are checked. Small
whole-residual controls also avoid the generating target-inner-product formula.
If stored.json is present, check all its last-place intervals. Evidence includes
exact rational endpoints so it can be reused to validate an upload without
repeating the integral calculation. Kernel checkpoints are printed on stderr.
"""
import json
import sys
import platform
import hashlib
from pathlib import Path
from math import gcd, lcm
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
import generate
import integral_kernel as ik
R=ik.R
def mu_by_trial(n):
"""Separate trial-division implementation; no Sage moebius call."""
result=1
p=2
while p*p<=n:
if n%p==0:
n//=p; result=-result
if n%p==0:return 0
p+=1
return -result if n>1 else result
def endpoints(x):
return [str(v.exact_rational()) for v in x.endpoints()]
def finite_narrow(x):
return bool(x.is_finite() and x.rad_as_ball()<R(10)**(-110))
def compare(a,b):
assert finite_narrow(a) and finite_narrow(b)
assert a.overlaps(b), (str(a),str(b))
def integrate_tail(parts, bound):
total=sum((ik.integral_rational_kernel(parts,n) for n in range(1,ik.K)),R(0))
for m in range(ik.M+1):
moment=QQ(0)
for left,right,a,b,c in parts:
moment+=a*(right**(m+3)-left**(m+3))/(m+3)
moment+=b*(right**(m+2)-left**(m+2))/(m+2)
moment+=c*(right**(m+1)-left**(m+1))/(m+1)
total+=(-1)**m*(m+1)*ik.zeta_tail(m)*R(moment)
error=QQ(ik.M+2)/QQ(ik.K)**(ik.M+3)+QQ(1)/QQ(ik.K)**(ik.M+2)
return total.add_error(R(bound*error))
def independent_weights(n):
# Eliminate mu(1) algebraically from the fixed-endpoint correction.
rest=[QQ(mu_by_trial(j)) for j in range(2,n+1)]
first=-sum((rest[j-2]/QQ(j) for j in range(2,n+1)),QQ(0))
w=[first]+rest
assert sum((w[j-1]/QQ(j) for j in range(1,n+1)),QQ(0))==0
return w
def direct_residual(n):
"""Whole residual integral, avoiding both Gram entries and b_n."""
L=lcm(*range(1,n+1));w=independent_weights(n)
cuts=sorted({QQ(k*j)/L for j in range(1,n+1) for k in range(L//j+1)})
parts=[]; finite=R(0)
for left,right in zip(cuts,cuts[1:]):
mid=(left+right)/2
const=1-sum(w[j-1]*(L*mid/j).floor() for j in range(1,n+1))
piece=(left,right,QQ(0),QQ(0),QQ(const*const))
parts.append(piece)
if left>=QQ(1)/L:
finite+=ik.integral_rational_kernel([piece],0)/L
bound=(1+sum(abs(x) for x in w))**2
return finite+integrate_tail(parts,bound)/L
def main():
# Known-answer controls and failure controls validate this comparison code.
assert [mu_by_trial(n) for n in range(1,11)]==[1,-1,-1,0,-1,1,-1,0,0,1]
pieces=[(QQ(0),QQ(1),QQ(1),QQ(0),QQ(0))]
compare(ik.integral_rational_kernel(pieces,0),R(1))
compare(ik.integral_rational_kernel(pieces,1),R(3)/2-2*R(2).log())
C=(2*R.pi()).log()-R.euler_constant();control=ik.integral_A(1,1)
compare(control,C)
rejected=[]
for name,bad in [('wrong value',control+R(QQ(1)/10**80)),
('wide ball',control.add_error(R(1))),('NaN',R('nan'))]:
try:compare(bad,C)
except AssertionError:rejected.append(name)
assert len(rejected)==3
known1=R(1)
known2=1-QQ(3)/4*R(2).log()
compare(direct_residual(1),known1);compare(direct_residual(2),known2)
field,G,b,values=generate.computation(30,100)
assert type(values[0]).__name__=='Integer'
weights=generate.coefficients(30)
assert all(type(w).__name__=='Rational' for w in weights)
assert weights==independent_weights(30)
assert [int(p['N']) for p in generate.VasyuninErrors().enumerate()]==list(range(1,31))
GI=[[R(0) for j in range(30)] for i in range(30)]
kernels=[]
for j in range(1,31):
for k in range(1,j+1):
common=gcd(j,k);v=ik.integral_A(j//common,k//common)/j
GI[j-1][k-1]=GI[k-1][j-1]=v
compare(v,G[j-1][k-1])
kernels.append({'j':j,'k':k,'endpoints':endpoints(v)})
print(json.dumps({'checkpoint_gram_row':j,'kernels':kernels[-j:]}),file=sys.stderr,flush=True)
bi=[(R(n).log()+1-R.euler_constant())/n for n in range(1,31)]
rows=[];direct={};repeats=[]
for n in range(1,31):
w=independent_weights(n)
assert w==generate.coefficients(n)
vi=1+2*sum((w[i]*bi[i] for i in range(n)),R(0))
vi+=sum((w[i]*w[j]*GI[i][j] for i in range(n) for j in range(n)),R(0))
compare(vi,R(values[n-1]));assert vi>0
if n in [1,2,3,4,6]:
direct[n]=direct_residual(n);compare(vi,direct[n])
minimum,x=ik.gauss_distance(GI,bi,n)
assert vi>minimum and finite_narrow(minimum)
g=sum((QQ(w[i])/QQ(i+1) for i in range(n)),QQ(0))
assert g==0
assert vi>g*g
if n>1 and mu_by_trial(n)==0:
compare(vi,R(values[n-2]));repeats.append(n)
# Expansion of the fixed-endpoint correction against the untapered sum.
mu=[QQ(mu_by_trial(j)) for j in range(1,n+1)]
gn=sum((mu[j-1]/QQ(j) for j in range(1,n+1)),QQ(0))
untapered=1+2*sum((mu[i]*bi[i] for i in range(n)),R(0))
untapered+=sum((mu[i]*mu[j]*GI[i][j] for i in range(n) for j in range(n)),R(0))
correction=untapered-2*gn*(bi[0]+sum((mu[i]*GI[0][i] for i in range(n)),R(0)))+gn*gn*GI[0][0]
compare(vi,correction)
rows.append({'N':n,'generator':str(values[n-1]),'generator_endpoints':endpoints(R(values[n-1])),
'integral':str(vi),'integral_endpoints':endpoints(vi),
'minimum':str(minimum),'minimum_endpoints':endpoints(minimum),
'exterior_tail_exact':str(g*g)})
compare(R(values[0]),known1);compare(values[1],known2)
stored_count=0;sp=Path(__file__).with_name('stored.json')
if sp.exists():
data=json.loads(sp.read_text())['Numbers'];assert list(map(int,data))==list(range(1,31))
for row in rows:
value=data[str(row['N'])];value=value['number'] if isinstance(value,dict) else value
lo,hi=(QQ(1),QQ(1)) if row['N']==1 else ik.decimal_interval(value)
for key in ['generator_endpoints','integral_endpoints']:
a,z=map(QQ,row[key])
if row['N']==1:
assert str(value)=='1' and a<=1<=z and z-a<QQ(1)/10**110
else:
assert lo<a and z<hi
stored_count+=1
hashes={name:hashlib.sha256(Path(__file__).with_name(name).read_bytes()).hexdigest()
for name in ['generate.py','integral_kernel.py','checks.py','skill-manifest.json']}
result={'table':'T708','stage':'build','checked_entries':30,'total_entries':30,'failures':[],
'known_answer_control':True,'negative_control_rejected':True,'rejected_controls':rejected,
'gram_entries_checked':465,'direct_whole_residual_checks':{str(k):str(v) for k,v in direct.items()},
'endpoint_cancellation_checked':30,'nonsquarefree_repetitions':repeats,'correction_identity_checked':30,'stored_intervals_checked':stored_count,
'generator_bits':int(field.precision()),'minimum_generator_accuracy_bits':min(int(v.accuracy()) for v in values[1:]),
'maximum_generator_radius':str(max(v.rad() for v in values[1:])),
'maximum_integral_radius':str(max(R(row['integral']).rad() for row in rows)),
'independent_bits':ik.PRECISION,'tail_start':ik.K,'last_power':ik.M,
'versions':{'sage':SAGE_VERSION,'numberdb':numberdb.__version__,'python':platform.python_version()},
'hashes':hashes,'rows':rows,'kernel_checkpoints':'kernel-checkpoints.jsonl'}
print('FINAL_EVIDENCE_BEGIN',flush=True)
print(json.dumps(result,indent=2),flush=True)
if __name__=='__main__':main()