back to table · edit · history · where entries came from · files · download
3849 bytes, as of the version from 2026-10-25 09:13 (current). Recorded here, not run.
"""Elementary spherical covering checks -- numberdb.org/T480.
Run with SageMath, beside generate.py and source.json:
sage -python repair-checks.py
Independent checks use exact vector geometry, rational squaring of decimal
endpoints, and MPFI trigonometry. The general lower-bound proof is in README.txt.
This script writes no table and reads no credentials.
"""
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_mpfi import RealIntervalField
from numberdb._write import to_text
from decimal import Decimal
import json
from generate import SphericalCoverings
def rational(text):
d = Decimal(text)
sign, digits, exponent = d.as_tuple()
value = QQ(int(''.join(map(str, digits)))) * QQ(10)**exponent
return -value if sign else value
def run():
def dot(a, b):
return sum(x*y for x, y in zip(a, b))
def squared_distance(a, b):
return sum((x-y)**2 for x, y in zip(a, b))
north = [QQ(0), QQ(0), QQ(1)]
south = [-x for x in north]
east = [QQ(1), QQ(0), QQ(0)]
boundary = [QQ(0), QQ(1), QQ(0)]
assert squared_distance(north, south) == 4
for centres in ([north, south], [north, south, east]):
assert all(dot(x, boundary) == 0 for x in centres)
assert min(squared_distance(x, boundary) for x in centres) == 2
assert dot(boundary, boundary) == 1
# The coordinate axes have full rank. Their opposite octant supplies
# the vector required by the other branch of the general proof.
centres = [east, boundary, north]
y = [QQ(-1), QQ(-1), QQ(-1)]
assert all(dot(x, y) == -1 for x in centres)
generator = SphericalCoverings()
I = RealIntervalField(768)
rows = {}
evidence = {'table': 'T480', 'numberdb_version': numberdb.__version__,
'geometry_controls': 'passed', 'entries': {},
'exact_entries': 0, 'irrational_entries': 0}
for n in range(1, 4):
rows[str(n)] = {}
rho = 180 if n == 1 else 90
for form in ('angle', 'chord'):
params = {'n': n, 'normalisation': form}
item = generator.value(params, 100)
value = item['number']
text = to_text(value, 100)
record = {'number': text, 'comment': item['comment']}
rows[str(n)][form] = record
info = {'number': text}
if form == 'angle' or n == 1:
expected = rho if form == 'angle' else 2
assert type(value) is int and value == expected
assert text == str(expected)
evidence['exact_entries'] += 1
else:
high = generator.value(params, 160)['number']
assert value.is_finite() and high.is_finite()
assert value.overlaps(high)
assert value.rad() < QQ(1)/10**120
q = rational(text)
ulp = QQ(10)**Decimal(text).as_tuple().exponent
lo, hi = q-ulp, q+ulp
assert lo > 0 and lo**2 < 2 < hi**2
independent = 2*(I(rho)*I.pi()/360).sin()
assert I(lo) < independent < I(hi)
assert I(lo) < I(high) < I(hi)
info.update({'rational_square_bracket': True,
'independent_interval_conversion': True,
'precision_agreement': [100, 160],
'ball_radius': str(value.rad())})
evidence['irrational_entries'] += 1
evidence['entries'][str(n)+','+form] = info
assert evidence['exact_entries'] == 4
assert evidence['irrational_entries'] == 2
assert len(list(generator.enumerate())) == 260
print('NEW_ROWS_JSON', json.dumps(rows))
print('REPAIR_EVIDENCE_JSON', json.dumps(evidence))
if __name__ == '__main__':
run()