back to table · edit · history · where entries came from · files · download
7379 bytes, as of the version from 2026-10-30 10:45 (current). Recorded here, not run.
"""Independent checks for numberdb.org/T623.
sage -python checks.py checks generated values. With --stored, reads T623
and T622 afresh, verifies every stored entry, and checks the eta difference.
The private drafts require NUMBERDB_API_KEY. The stdin key option is supported.
Checks use no source attachment from T622. check.py is the campaign's unchanged
common exactness/measurement helper. No computations are sent to the website.
"""
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from math import gcd
from pathlib import Path
import json
import os
import sys
from generate import LensSpaceRho, rho
from check import exactness, measure, agrees_with, names_its_rings
BITS = 512
R = RealBallField(BITS)
def lattice_rho(key):
"""Count geometric lattice points directly, without sawtooth code."""
p, q, u = key
if u == 0:
return QQ(0)
# Brute-force character conversion independently of modular inversion.
k = next(k for k in range(1, p) if (q*k-u) % p == 0)
four_count = 0
for x in range(k+1):
for y in range((k*q)//p+1):
if (x == 0 and y == 0) or p*y > q*x:
continue
if x == k and (y == 0 or p*y == q*k):
four_count += 1
elif x == k or y == 0 or p*y == q*x:
four_count += 2
else:
four_count += 4
four_area = QQ(2*q*k*k)/QQ(p)
return QQ(four_count)-four_area
def trig_rho(p, q, u):
"""Finite APS cotangent sum for a complex line, using Arb throughout."""
answer = R(0)
for j in range(1, p):
a = R.pi()*R(QQ(j)/QQ(p))
b = R.pi()*R(QQ(q*j)/QQ(p))
c = R.pi()*R(QQ(u*j)/QQ(p))
answer += (a.cos()/a.sin())*(b.cos()/b.sin())*c.sin()**2
return 2*answer/R(p)
def eta_sum(p, q, u):
"""An exact convolution, independent of the prefix sum in generate.py."""
total = QQ(0)
for j in range(1, p):
b = (q*j+u) % p
if b:
total += QQ((2*j-p)*(2*b-p))/QQ(p*p)
return -total
def records(doc):
block = doc['Numbers']
if isinstance(block, list):
assert all('params' in row for row in block)
return {(int(row['params']['p']), int(row['params']['q']),
int(row['params']['u'])): QQ(row['number']) for row in block}
return {(int(p),int(q),int(u)): QQ(value['number'] if isinstance(value,dict) else value)
for p, qs in block.items() for q, us in qs.items()
for u, value in us.items()}
def main(stored=False):
gen = LensSpaceRho()
# Controls first, with a nonzero, its negative, and a genuine zero.
controls = {(2,1,1): QQ(0), (3,1,1): QQ(1)/3,
(3,2,1): -QQ(1)/3, (5,1,2): QQ(7)/5}
for key, known in controls.items():
assert rho(*key) == known and lattice_rho(key) == known
ball = trig_rho(*key)
assert ball.is_finite() and R(ball.rad()) < R(10)**-140
assert known in ball
enumeration = [tuple(int(params[n]) for n in gen.parameters) for params in gen.enumerate()]
assert len(enumeration) == len(set(enumeration)) == 550
assert len({key[:2] for key in enumeration}) == 87
assert enumeration == sorted(enumeration)
values = {key: rho(*key) for key in enumeration}
report = {'table':'T623', 'mode':'stored' if stored else 'local',
'skill_manifest':'agents/runs/20261030T101710Z-build-skills/manifest.json',
'skill_sha256':'28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199',
'environment':gen.environment(), 'controls':{','.join(map(str,k)):str(v) for k,v in controls.items()}}
if stored:
doc = numberdb.table('T623')
values = records(doc)
assert list(values) == enumeration
verify = gen.verify(sample=None)
assert verify.ok
report['verify'] = str(verify)
eta = records(numberdb.table('T622'))
assert all(values[p,q,u] == eta[p,q,u]-eta[p,q,0] for p,q,u in values)
report['live_eta_difference_checks'] = len(values)
import contextlib, io
namespace = {}
with contextlib.redirect_stdout(io.StringIO()):
exec(doc['Programs']['Sage']['code'], namespace)
assert all(namespace['rho'](*key) == value for key,value in values.items())
report['program_checks'] = len(values)
assert not exactness(values)
assert not names_its_rings(str(Path(__file__).with_name('generate.py')))
assert not agrees_with(values, lattice_rho)
max_radius = R(0)
minimum_accuracy = BITS
balls = []
for (p,q,u), value in values.items():
assert value == eta_sum(p,q,u)-eta_sum(p,q,0)
ball = trig_rho(p,q,u)
assert ball.is_finite() and R(ball.rad()) < R(10)**-140
assert value in ball
max_radius = max(max_radius, R(ball.rad()))
if value:
minimum_accuracy = min(minimum_accuracy, int(ball.accuracy()))
balls.append({'p':p,'q':q,'u':u,'rational':str(value),'ball':str(ball),
'radius':str(ball.rad()),'relative_accuracy_bits':int(ball.accuracy()) if value else None})
# Full domain, including omitted orientations/presentations/conjugates.
full = {(p,q,u):rho(p,q,u) for p in range(2,21)
for q in range(1,p) if gcd(p,q)==1 for u in range(p)}
for (p,q,u), value in full.items():
r = pow(q,-1,p)
assert value == full[p,q,(-u)%p]
assert value == full[p,r,(u*r)%p]
assert value == -full[p,p-q,u]
assert value == eta_sum(p,q,u)-eta_sum(p,q,0)
assert value == lattice_rho((p,q,u))
if u == 0:
assert value == 0
else:
# Recover every raw label from the actual selected stored rows.
qq, uu = (q,u) if q <= r else (r,(u*r)%p)
uu = min(uu,p-uu)
assert values[p,qq,uu] == value
if q == 1:
assert value == (QQ(0) if u == 0 else QQ(2*u*(p-u))/QQ(p)-1)
for p,q in {key[:2] for key in full}:
eta_ball = -sum(((R.pi()*R(QQ(j)/QQ(p))).cot() *
(R.pi()*R(QQ(q*j)/QQ(p))).cot()
for j in range(1,p)), R(0))/R(p)
assert eta_ball.is_finite() and R(eta_ball.rad()) < R(10)**-140
assert eta_sum(p,q,0) in eta_ball
assert sum((full[p,q,u] for u in range(p)), QQ(0)) == -p*eta_sum(p,q,0)
report.update(entries=len(values),presentations=87,measurement=measure(values),
lattice_checks=len(values),eta_convolution_checks=len(values),
ball_checks=len(values),ball_precision_bits=BITS,
max_ball_radius=str(max_radius),minimum_nonzero_relative_bits=minimum_accuracy,
full_domain_labels=len(full),full_domain_identities='conjugation, orientation, exchange, homogeneous, eta difference, lattice counts, reconstruction from selected rows, full character sum',
zero_entries=sum(v==0 for v in values.values()),unique_values=len(set(values.values())),
enclosures=balls)
print(json.dumps(report,indent=2))
return report
if __name__ == '__main__':
if os.environ.get('NUMBERDB_KEY_FROM_STDIN') == '1':
os.environ['NUMBERDB_API_KEY'] = sys.stdin.read().strip()
main(stored='--stored' in sys.argv)