back to table · edit · history · where entries came from · files · download
9181 bytes, as of the version from 2026-10-27 04:54 (current). Recorded here, not run.
"""Independent checks for Distance Estrada indices -- numberdb.org/T538.
Run: sage -python checks.py
To check a saved database document: sage -python checks.py stored-document.json
All data files listed by generate.py must be beside these scripts.
The independent method decodes graph6 without Sage's Graph constructor, finds
shortest paths by Floyd-Warshall, and sums trace(D^k)/k! exactly using Python
integers and fractions. For R=max(row sum), the remaining tail after degree N
is at most n*R^(N+1)/(N+1)!/(1-R/(N+2)), for N+2>R. This follows from the
matrix infinity norm and a geometric bound on the exponential tail. All trace
terms are nonnegative. Thus [partial sum, partial sum+tail bound] encloses the
answer. This method uses no roots, characteristic polynomials, or Arb exp.
Controls run first: zero matrix, identity matrix, K2 and P3.
"""
from collections import Counter
from fractions import Fraction
import hashlib
import json
from pathlib import Path
import sys
import time
import numberdb.sage as numberdb
from sage.env import SAGE_VERSION
from sage.graphs.graph_generators import GraphGenerators
from sage.rings.integer_ring import ZZ
from sage.rings.rational_field import QQ
from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
from sage.rings.real_arb import RealBallField
from sage.rings.real_mpfi import RealIntervalField
from generate import DistanceEstrada, distance_data, selection, WORKING_GUARD
from check import exactness, measure, agrees_with, names_its_rings
ROOT=Path(__file__).resolve().parent
B=RealBallField(480)
I=RealIntervalField(480)
P=PolynomialRing(ZZ,'x')
def rational(q):
return QQ(q.numerator)/QQ(q.denominator)
def decode_distance(key):
n=ord(key[0])-63
assert 2<=n<=6
bits=[]
for ch in key[1:]:
bits.extend((ord(ch)-63 >> shift) & 1 for shift in range(5,-1,-1))
dist=[[0 if i==j else n+1 for j in range(n)] for i in range(n)]
t=0
for j in range(1,n):
for i in range(j):
if bits[t]: dist[i][j]=dist[j][i]=1
t+=1
for k in range(n):
for i in range(n):
for j in range(n):
dist[i][j]=min(dist[i][j],dist[i][k]+dist[k][j])
assert max(map(max,dist))<n
return dist
def trace_series(dist, digits=125):
n=len(dist)
norm=max(sum(abs(x) for x in row) for row in dist)
power=[[int(i==j) for j in range(n)] for i in range(n)]
total=Fraction(n)
factorial=1
norm_power=1
k=0
while True:
tail=Fraction(n*norm_power*norm,factorial*(k+1))
if k+2>norm:
tail /= 1-Fraction(norm,k+2)
if tail < Fraction(1,10**digits): break
k+=1
power=[[sum(power[i][t]*dist[t][j] for t in range(n))
for j in range(n)] for i in range(n)]
factorial*=k
norm_power*=norm
total+=Fraction(sum(power[i][i] for i in range(n)),factorial)
return B(I(rational(total),rational(total+tail))),k,tail
def narrow(v,digits=110):
assert v.is_finite()
assert B(v.rad()) < max(B(1),abs(v))*B(10)**(-digits)
def compare(a,b):
narrow(a); narrow(b)
assert a.overlaps(b)
def contains(outer, inner):
return outer.lower() <= inner.lower() and inner.upper() <= outer.upper()
def written_interval(text):
# NumberDB decimals denote plus/minus one unit in the last written place.
from decimal import Decimal
v=Decimal(text)
q=Fraction(v)
if '.' not in text and 'e' not in text.lower():
return I(rational(q))
ulp=Fraction(10)**v.as_tuple().exponent
return I(rational(q-ulp),rational(q+ulp))
def main(stored_path=None):
started=time.monotonic()
assert not names_its_rings(ROOT/'generate.py')
compare(trace_series([[0,0],[0,0]])[0],B(2))
compare(trace_series([[1,0],[0,1]])[0],2*B(1).exp())
compare(trace_series([[0,1],[1,0]])[0],B(1).exp()+B(-1).exp())
compare(trace_series([[0,1,2],[1,0,1],[2,1,0]])[0],
(1+B(3).sqrt()).exp()+(1-B(3).sqrt()).exp()+B(-2).exp())
print('CONTROLS PASS: zero, identity, K2, P3',flush=True)
rows=selection(); keys=[r['g'] for r in rows]
assert keys==sorted(keys,key=lambda k:(ord(k[0]),k)) and len(set(keys))==142
assert dict(Counter(r['order'] for r in rows))=={2:1,3:2,4:6,5:21,6:112}
snapshots=json.loads((ROOT/'comparison-tables.json').read_text())
for tid,doc in snapshots.items(): assert set(doc['Numbers'])==set(keys),tid
graphs=GraphGenerators()
census=[]
for n in range(2,7):
census.extend(g.canonical_label(algorithm='sage').graph6_string()
for g in graphs.nauty_geng('%s -c'%n))
assert sorted(census)==sorted(keys)
print('ENUMERATION PASS: nauty, canonicalization, four live-table snapshots',flush=True)
generator=DistanceEstrada()
values={}; independent={}; results=[]
counters=Counter()
stored=None
if stored_path:
stored=json.loads(Path(stored_path).read_text())['Numbers']
assert list(stored)==keys
for row in rows:
key=row['g']; graph,distance,poly,roots=distance_data(key)
n=graph.order()
assert n==row['order'] and graph.canonical_label(algorithm='sage').graph6_string()==key
dist=decode_distance(key)
assert dist==[[int(distance[i,j]) for j in range(n)] for i in range(n)]
p_stored=snapshots['T537']['Numbers'][key]
if isinstance(p_stored,dict): p_stored=p_stored['number']
assert poly==P(p_stored)
assert poly[n-1]==0
sum_squares=sum(x*x for row_d in dist for x in row_d)
assert -2*poly[n-2]==sum_squares
root_sum=sum((m*B(I(r)) for r,m in roots),B(0))
root_squares=sum((m*B(I(r))**2 for r,m in roots),B(0))
narrow(root_sum); narrow(root_squares)
assert root_sum.contains_zero() and (root_squares-sum_squares).contains_zero()
values[key]=generator.value({'g':key},100)
v=values[key]['number']; narrow(v)
independent[key],terms,tail=trace_series(dist)
compare(v,independent[key])
# Certified bounds using the largest distance eigenvalue.
rho=max(r for r,m in roots)
rhoval=snapshots['T536']['Numbers'][key]
if isinstance(rhoval,dict): rhoval=rhoval['number']
rho_interval=written_interval(rhoval)
if '.' not in rhoval and 'e' not in rhoval.lower():
assert rho==QQ(rhoval),('exact stored radius',key)
else:
assert contains(rho_interval,I(rho)),('stored radius interval',key)
exp_rho=B(I(rho)).exp()
assert v>n and v>exp_rho and v<n*exp_rho
# Closed forms, evaluated independently of the roots.
forms=[]
if graph.size()==n*(n-1)//2:
forms.append(B(n-1).exp()+(n-1)*B(-1).exp()); counters['complete']+=1
if graph.is_bipartite():
left,right=graph.bipartite_sets(); a,b=len(left),len(right)
if graph.size()==a*b:
s=B(a*a-a*b+b*b).sqrt()
forms.append(B(a+b-2+s).exp()+B(a+b-2-s).exp()+(a+b-2)*B(-2).exp())
counters['complete_bipartite']+=1
for f in forms:
compare(v,f)
if stored is not None:
raw=stored[key]; text=raw['number'] if isinstance(raw,dict) else raw
interval=written_interval(text)
assert contains(interval,I(independent[key])),('stored series',key)
assert contains(interval,I(v)),('stored generator',key)
for f in forms: assert contains(interval,I(f)),('stored formula',key)
if len(results)%25==0: print('Checked',len(results)+1,'of 142, graph',key,flush=True)
bits=int(-(v.rad()/abs(v.center())).log2())
results.append({'g':key,'order':n,'series_degree':terms,
'series_tail_bound':str(tail),'relative_accuracy_bits_floor':bits,
'root_multiplicities':[int(m) for r,m in roots]})
assert not exactness(values)
assert not agrees_with({k: [[int(x) for x in row] for row in distance_data(k)[1].rows()] for k in keys}, decode_distance)
assert counters=={'complete':5,'complete_bipartite':9}
summary={'table':'T538','entries':len(values),'controls':['zero','identity','K2','P3'],
'method':'exact rational trace series with a norm-geometric tail bound',
'skill_manifest':'agents/runs/20261027T044107Z-build-skills/manifest.json',
'skill_sha256':'e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c',
'sage':SAGE_VERSION,'numberdb':numberdb.__version__,'working_guard_bits':WORKING_GUARD,
'minimum_relative_accuracy_bits':min(r['relative_accuracy_bits_floor'] for r in results),
'series_max_degree':max(r['series_degree'] for r in results),
'formula_counts':dict(counters),'measurement':measure(values),
'stored_intervals_checked':len(values) if stored is not None else 0,
'seconds':round(time.monotonic()-started,2),'rows':results}
print('EVIDENCE_JSON '+json.dumps(summary,ensure_ascii=False),flush=True)
if __name__=='__main__':
main(sys.argv[1] if len(sys.argv)>1 else None)