back to table · edit · history · where entries came from · files · download
6595 bytes, as of the version from 2026-11-10 21:29 (current). Recorded here, not run.
"""Executable T709 build evidence, not an independent actor verdict.
sage -python checks.py > numerical-evidence.log 2> residual-checkpoints.jsonl
Keep generate.py, integral_kernel.py and skill-manifest.json beside this file.
The entire residual is integrated on its constant intervals in t=1/(N*x).
The periodic tail uses digamma differences, independently of Gram entries,
cotangent sums and target inner products. A separate explicit series remainder
also checks N=1,2,3,4,30. Exact binary endpoints make every result resumable.
"""
import json,sys,platform,hashlib
from pathlib import Path
from functools import lru_cache
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):
s=1;p=2
while p*p<=n:
if n%p==0:
n//=p;s=-s
if n%p==0:return 0
p+=1
return -s if n>1 else s
def independent_weights(n):
# Group mu(m) by floor(n/m); this differs from Mertens differences.
w=[0]*n
for m in range(1,n+1):w[n//m-1]+=mu_by_trial(m)
w[0]-=1
assert sum((k*w[k-1] for k in range(1,n+1)),0)==0
return w
def endpoints(x):return [str(y.exact_rational()) for y 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 residual_parts(n,w):
assert sum(k*w[k-1] for k in range(1,n+1))==0
cuts=sorted({QQ(k)/j for j in range(1,n+1) for k in range(j+1)})
parts=[]
for l,r in zip(cuts,cuts[1:]):
mid=(l+r)/2
c=1-sum(w[j-1]*(j*mid).floor() for j in range(1,n+1))
# Merge adjacent pieces with identical squared residual.
if parts and parts[-1][4]==c*c:
old=parts[-1];parts[-1]=(old[0],r,QQ(0),QQ(0),QQ(c*c))
else:parts.append((l,r,QQ(0),QQ(0),QQ(c*c)))
return parts
@lru_cache(None)
def psi(q):return R(q).psi()
def direct_residual(n):
w=independent_weights(n);parts=residual_parts(n,w)
finite=R(0);tail=R(0)
for l,r,_,_,c in parts:
left=max(l,QQ(1)/n)
if r>left:finite+=R(c)*(1/R(left)-1/R(r))
tail+=R(c)*(psi(1+r)-psi(1+l))
return (finite+tail)/n,parts,finite
def series_tail(parts):
total=sum((ik.integral_rational_kernel(parts,m) for m in range(1,ik.K)),R(0))
powers=[(l,r,c,l,r) for l,r,_,_,c in parts]
for m in range(ik.M+1):
moment=QQ(0)
for i,(l,r,c,lp,rp) in enumerate(powers):
moment+=c*(rp-lp)/(m+1)
powers[i]=(l,r,c,lp*l,rp*r)
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)
bound=max(c for l,r,_,_,c in parts)
return total.add_error(R(bound*error))
def main():
assert [mu_by_trial(n) for n in range(1,11)]==[1,-1,-1,0,-1,1,-1,0,0,1]
compare(psi(QQ(1)),-R.euler_constant())
compare(psi(QQ(1)/2),-R.euler_constant()-2*R(2).log())
control=ik.integral_rational_kernel([(QQ(0),QQ(1),QQ(1),QQ(0),QQ(0))],1)
compare(control,R(3)/2-2*R(2).log())
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(control,bad)
except AssertionError:rejected.append(name)
assert len(rejected)==3
wrong=independent_weights(3);wrong[0]+=1
try:residual_parts(3,wrong)
except AssertionError:rejected.append('omitted subtractive rho_N')
assert len(rejected)==4
field,G,values=generate.computation(30,100)
assert type(values[0]).__name__=='Integer'
assert [int(p['N']) for p in generate.DualErrors().enumerate()]==list(range(1,31))
known={1:R(1),2:1-R(2).log(),3:1-R.pi()/(3*R(3).sqrt()),4:1-R.pi()/4}
rows=[];series=[]
for n in range(1,31):
w=independent_weights(n)
assert w==generate.coefficients(n)
assert all(type(a).__name__=='Integer' for a in generate.coefficients(n))
vi,parts,finite=direct_residual(n)
compare(vi,R(values[n-1]));assert vi>0
if n in known:compare(vi,known[n])
row={'N':n,'weights':w,'generator':str(values[n-1]),'generator_endpoints':endpoints(R(values[n-1])),
'integral':str(vi),'integral_endpoints':endpoints(vi),'constant_pieces':len(parts),'exterior_tail_exact':'0'}
if n in [1,2,3,4,30]:
vseries=(finite+series_tail(parts))/n
compare(vi,vseries)
row.update(series=str(vseries),series_endpoints=endpoints(vseries));series.append(n)
rows.append(row)
print(json.dumps(row),file=sys.stderr,flush=True)
# Deliberately omit dual Gram scaling: must disagree on a nontrivial case.
n=3;w=independent_weights(n)
bi=[R(QQ(k)/n)*(R(QQ(n)/k).log()+1-R.euler_constant()) for k in range(1,n+1)]
wrong=1+2*sum(w[k-1]*bi[k-1] for k in range(1,n+1))+sum(w[j-1]*w[k-1]*G[j-1][k-1] for j in range(1,n+1) for k in range(1,n+1))
assert not R(wrong).overlaps(known[3]);rejected.append('omitted dual Gram scaling')
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':'T709','stage':'build','checked_entries':30,'total_entries':30,'failures':[],
'known_answer_control':True,'negative_control_rejected':True,'rejected_controls':rejected,
'direct_whole_residual_checked':list(range(1,31)),'additional_series_checks':series,
'coefficient_and_exterior_cancellation_checked':30,'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,'checkpoint_file':'residual-checkpoints.jsonl',
'limitations':'Build evidence, not an independent actor verdict; shared Arb arithmetic, distinct formulas and weight implementations. No universal asymptotic conclusion.'}
print('FINAL_EVIDENCE_BEGIN',flush=True);print(json.dumps(result,indent=2),flush=True)
if __name__=='__main__':main()