back to table · edit · history · where entries came from · files · download
7739 bytes, as of the version from 2026-10-25 07:24 (current). Recorded here, not run.
"""Independent checks for numberdb.org/T477.
Run `sage -python checks.py` beside generate.py and square-packings-source.json.
Use `--stored` with NUMBERDB_API_KEY to check authenticated database readback.
The build runner can pipe the key with NUMBERDB_KEY_FROM_STDIN=1.
The geometric check ignores the source radius when recomputing the value:
it finds the least pairwise center distance D and the square bounding the
centers, of side L, then computes d=D/L and S=2+2L/D. Each printed coordinate
is allowed one unit (10^-12) of uncertainty. Interval extrema enclose every
choice in these coordinate boxes. This models printed-coordinate rounding;
it is not a proof of existence or global optimality of a packing.
"""
import json
import os
import sys
from fractions import Fraction
from pathlib import Path
import numberdb.sage as numberdb
from numberdb._write import to_text
from sage.rings.rational_field import QQ
from sage.rings.real_mpfi import RealIntervalField
from generate import SquarePackings, ROWS, GRID, FORMULAS, CERTIFIED, side_exact
FIELD = RealIntervalField(512)
def q(text):
f = Fraction(str(text))
return QQ(f.numerator) / QQ(f.denominator)
def interval(text):
"""The interval promised by a written NumberDB value."""
text = str(text)
if '/' in text or ('.' not in text and 'e' not in text.lower()):
return FIELD(q(text))
from decimal import Decimal
d = Decimal(text)
unit = QQ(10) ** d.as_tuple().exponent
return FIELD(q(text)-unit, q(text)+unit)
def minimum(values):
values = list(values)
return FIELD(min(x.lower() for x in values), min(x.upper() for x in values))
def maximum(values):
values = list(values)
return FIELD(max(x.lower() for x in values), max(x.upper() for x in values))
def geometry(points, error=QQ(0)):
pts = [(FIELD(q(x)-error, q(x)+error), FIELD(q(y)-error, q(y)+error))
for x,y in points]
span = maximum(maximum(p[k] for p in pts)-minimum(p[k] for p in pts)
for k in (0,1))
separation = minimum(((a[0]-b[0])**2+(a[1]-b[1])**2).sqrt()
for i,a in enumerate(pts) for b in pts[:i])
d = separation/span
return {'separation': d, 'container': 2+2/d, 'span': span}
def contains(outer, inner):
return outer.lower() <= inner.lower() and outer.upper() >= inner.upper()
def finite_tight(value, width):
assert not value.is_NaN() and value.absolute_diameter() < width, str(value)
def flatten(tree):
nums = tree['Numbers']
if isinstance(nums,list):
return {(int(e['params']['n']),e['params']['normalisation']):e['number'] for e in nums}
return {(int(n),norm):v['number'] if isinstance(v,dict) else v
for n,vs in nums.items() for norm,v in vs.items()}
def run(stored=False):
# Controls precede measurements: a square grid and two opposite corners.
c = geometry([('-0.25','-0.25'),('0.25','-0.25'),('-0.25','0.25'),('0.25','0.25')])
assert c['separation'] == 1 and c['container'] == 4
two = geometry([('0','0'),('1','1')])
assert two['separation'].overlaps(FIELD(2).sqrt())
assert two['container'].overlaps(2+FIELD(2).sqrt())
bad = geometry([('-0.25','-0.25'),('0.24','-0.25'),('-0.25','0.25'),('0.25','0.25')])
assert bad['separation'].upper()<1 and bad['container'].lower()>4
gen = SquarePackings()
written = {}
for params in gen.enumerate():
v = gen.value(params,gen.digits)
written[(int(params['n']),params['normalisation'])] = to_text(v['number'],v.get('digits',gen.digits))
if stored:
db = flatten(numberdb.table('T477'))
assert set(db) == set(written), (len(db),len(written))
written = db
rows=[]
retention = {d: [] for d in (10,11,12)}
previous=None
exact_widths=[]
for ns, source in ROWS.items():
n=int(ns)
assert len(source['coordinates'])==n
assert all(len(c)==3 and q(c[2])==q(source['radius']) for c in source['coordinates'])
geo=geometry([p[:2] for p in source['coordinates']],QQ(1)/10**12)
for norm in ('separation','container'):
finite_tight(geo[norm],QQ(1)/10**8)
assert geo[norm].overlaps(interval(source[norm])),(n,norm,'source/coordinate disagreement')
assert (1/geo['container']).overlaps(interval(source['radius'])), (n,'radius')
# Unit-square boundary and pair distances are also consistent with the
# printed radius, without assuming that rounding preserves tangencies.
assert geo['span'].overlaps(1-2*interval(source['radius'])),(n,'boundary')
d=interval(written[(n,'separation')]);side=interval(written[(n,'container')])
assert side.overlaps(2+2/d),(n,'stored conversion')
assert d.overlaps(2/(side-2)),(n,'stored inverse conversion')
if previous:
assert d.lower()<=previous[0].upper() and side.upper()>=previous[1].lower(),(n,'monotonicity')
previous=(d,side)
if n in GRID or n in FORMULAS:
for digits in (100,160):
s=side_exact(n,digits)
d_exact=QQ(2)/(s-2)
for norm,v in (('container',s),('separation',d_exact)):
vi=FIELD(v)
assert vi.overlaps(interval(source[norm])),(n,norm,'formula/source')
assert geo[norm].overlaps(vi),(n,norm,'formula/coordinates')
assert contains(interval(written[(n,norm)]),vi),(n,norm,'written exact value')
finite_tight(vi,QQ(1)/10**110)
if n not in GRID and digits==100:
exact_widths.append(str(vi.absolute_diameter()))
if n in GRID:
assert q(written[(n,'container')])==2*GRID[n]
assert q(written[(n,'separation')])==QQ(1)/(GRID[n]-1)
elif n in CERTIFIED:
lo,hi=CERTIFIED[n]
cert=FIELD(q(lo),q(hi))
assert contains(d,cert) and contains(side,2+2/cert),(n,'certified enclosure')
assert geo['separation'].overlaps(cert),(n,'certified/coordinates')
else:
from decimal import Decimal,localcontext
for digits in (10,11,12):
with localcontext() as context:
context.prec=digits
for norm in ('container','separation'):
out=interval(format(+Decimal(source[norm]),'f'))
if not contains(out,geo[norm]):
retention[digits].append('%d,%s'%(n,norm))
assert contains(d,geo['separation']) and contains(side,geo['container']), (n,'retained precision')
rows.append({'n':n,'coordinate_d':str(geo['separation']),
'coordinate_S':str(geo['container']),
'stored_d':written[(n,'separation')],
'stored_S':written[(n,'container')]})
report={'table':'T477','mode':'stored' if stored else 'local',
'passed':True,'configurations':len(rows),'entries':len(written),
'exact_formula_configurations':len(GRID)+len(FORMULAS),
'certified_interval_configurations':len(CERTIFIED),
'numerical_configurations':len(rows)-len(GRID)-len(FORMULAS)-len(CERTIFIED),
'precision_failure_counts':{str(k):len(v) for k,v in retention.items()},
'precision_failures':retention,'closed_form_interval_widths':exact_widths,'rows':rows}
print(json.dumps(report,indent=2))
return report
if __name__=='__main__':
if os.environ.get('NUMBERDB_KEY_FROM_STDIN') == '1':
numberdb.configure(api_key=sys.stdin.read().strip())
run(stored='--stored' in sys.argv or os.environ.get('NUMBERDB_CHECK_STORED') == '1')