back to table · edit · history · where entries came from · files · download
8152 bytes, as of the version from 2026-11-01 16:17 (current). Recorded here, not run.
"""Checks for T654, including independent computation from weighted degree laws.
sage -python checks.py
sage -python checks.py --stored # also check the values read from T654
Requires generate.py, check.py, companion-hilbert.json and skill-manifest.json
beside this file. The companion snapshot is data read from T653, not the
source code that generated it. This is build evidence, not the independent
campaign critique. JSON evidence is printed to stdout.
"""
import os
import sys
import json
import hashlib
from decimal import Decimal
from fractions import Fraction
from pathlib import Path
import numberdb.sage as numberdb
from numberdb._write import to_text
from sage.rings.integer_ring import ZZ
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from sage.env import SAGE_VERSION
import mpmath as mp
from generate import GrowthConstants, hilbert, enclose, R, t, selected_groups
from check import exactness, measure, names_its_rings, agrees_with
HERE = Path(__file__).resolve().parent
def independent(identity, digits=180):
"""Separate factor-moment bisection, with no polynomial/root code shared."""
with mp.workdps(digits):
family, size, p = identity.split('-')
size, p = int(size), int(p)
if family == 'UT':
weights = [j-i for i in range(size) for j in range(i+1,size)]
else:
weights = [1]*(2*size)+[2]
degree = (p-1)*sum(weights)
def statistics(x):
total, mean = mp.mpf(1), mp.mpf(0)
for weight in weights:
terms = [x**(weight*a) for a in range(p)]
z = sum(terms)
total *= z
mean += sum(weight*a*terms[a] for a in range(p))/z
return total, mean
a, b = mp.mpf(0), mp.mpf(1)
target = mp.mpf(degree)/3
for _ in range(560):
mid = (a+b)/2
if statistics(mid)[1] < target:
a = mid
else:
b = mid
x = (a+b)/2
h, mean = statistics(x)
c = h/mp.power(x,target)
assert abs(mean-target) < mp.mpf('1e-160')
return +x, +c, weights
def decimal_bounds(text):
"""The stored plain decimal claims +/- one unit in its final place."""
dec = Decimal(text)
mid = Fraction(dec)
ulp = Fraction(10)**dec.as_tuple().exponent
return QQ((mid-ulp).numerator)/ZZ((mid-ulp).denominator), QQ((mid+ulp).numerator)/ZZ((mid+ulp).denominator)
def mpq(q):
return mp.mpf(int(q.numerator()))/int(q.denominator())
def accuracy_bits(ball):
lo, hi = ball.lower().exact_rational(), ball.upper().exact_rational()
assert 0 < lo < hi
return int((lo/(hi-lo)).floor().nbits()-1)
def main():
if os.environ.get('NUMBERDB_KEY_FROM_STDIN') == '1':
numberdb.configure(api_key=sys.stdin.read().strip())
mp.mp.dps = 180
# Known-answer controls precede any measurement.
control, bracket, _ = enclose(1+t, 100)
assert bracket == (QQ(1)/2,QQ(1)/2)
assert QQ(27)/4 in control**3
control2, _, _ = enclose((1+t)**3,100)
assert QQ(27)/4 in control2
assert accuracy_bits(control2) >= 380
control_x, control_c, _ = independent("UT-2-2")
assert abs(control_x-mp.mpf(1)/2) < mp.mpf("1e-160")
assert abs(control_c-3/mp.power(2,mp.mpf(2)/3)) < mp.mpf("1e-160")
expected = []
for p, sizes in [(2,[3,4,5,6]), (3,[3,4,5,6]), (5,[3,4,5]), (7,[3,4])]:
expected += ['UT-%d-%d' % (n,p) for n in sizes]
expected += ['Heis-%d-%d' % (r,p) for r in [2,3,4]]
assert list(selected_groups()) == expected
companion = json.loads((HERE/'companion-hilbert.json').read_text())
assert list(companion['Numbers']) == expected
polynomials = {g:hilbert(g) for g in expected}
assert not exactness(polynomials)
assert not agrees_with(polynomials, lambda g:R(companion['Numbers'][g]['number']))
assert not names_its_rings(str(HERE/'generate.py'))
stored = None
if '--stored' in sys.argv or os.environ.get('CHECK_STORED') == '1':
stored = numberdb.table('T654')['Numbers']
assert list(stored) == expected
values, rows = {}, []
for identity in expected:
h = polynomials[identity]
d = h.degree()
family, size, prime = identity.split('-')
size, p = int(size), int(prime)
dimension = size*(size-1)//2 if family=='UT' else 2*size+1
expected_degree = (p-1)*size*(size*size-1)//6 if family=='UT' else (p-1)*(2*size+2)
assert d == expected_degree
assert h(0)==1 and h[d]==1 and h(1)==p**dimension
assert list(h) == list(reversed(list(h)))
assert 2*h.derivative()(1)==d*h(1)
c, (a,b), root = enclose(h,100)
precise, _, _ = enclose(h,140)
assert c.is_finite() and precise.is_finite()
assert c.overlaps(precise)
assert accuracy_bits(c) >= 380
assert accuracy_bits(precise) >= 510
x, independent_c, weights = independent(identity)
assert mpq(a)<=x<=mpq(b)
low, high = c.lower().exact_rational(),c.upper().exact_rational()
assert mpq(low) <= independent_c <= mpq(high)
coeffs = list(h)
normalizer = sum(mp.mpf(int(v))*x**j for j,v in enumerate(coeffs))
entropy = mp.mpf(0)
for j, v in enumerate(coeffs):
if v:
q = mp.mpf(int(v))*x**j/normalizer
entropy -= q*mp.log(q/int(v))
assert abs(mp.exp(entropy)/independent_c-1) < mp.mpf('1e-158')
text = to_text(c,digits=100)
lo,hi = decimal_bounds(text)
# The entire certified enclosure must fit in the written interval.
assert lo <= low and high <= hi
if stored is not None:
text = stored[identity]['number']
lo,hi = decimal_bounds(text)
assert lo <= precise.lower().exact_rational()
assert precise.upper().exact_rational() <= hi
assert mpq(lo) <= independent_c <= mpq(hi)
assert 1<lo and hi<h(1)
# Direct bounded-composition DP, independent of polynomial powers.
counts = [1]
finite_counts = []
for k in range(1,5):
for weight in weights:
new = [0]*(len(counts)+(p-1)*weight)
for j,v in enumerate(counts):
for digit in range(p):
new[j+digit*weight] += v
counts = new
power = h**k
assert counts == list(power)
L = sum(counts[:k*d//3+1])
assert RealBallField(600)(L) < precise**k
finite_counts.append(str(L))
if k in (2,3):
power_c, power_bracket, _ = enclose(power,100)
assert power_bracket == (a,b)
assert power_c.overlaps(c**k)
values[identity] = c
rows.append({'G':identity,'C_100':text,'optimizer':mp.nstr(x,140),
'root_bracket':[str(a),str(b)],'relative_accuracy_bits':int(accuracy_bits(c)),
'high_precision_accuracy_bits':int(accuracy_bits(precise)),
'independent_C_150':mp.nstr(independent_c,150),
'L_at_k_1_to_4':finite_counts})
assert not exactness(values)
evidence={'table':'T654','stage':'build','all_passed':True,'stored_checked':stored is not None,
'skill_manifest':'agents/runs/20261101T154704Z-build-skills/manifest.json',
'skill_versions':json.loads((HERE/'skill-manifest.json').read_text())['versions'],
'versions':{'sage':SAGE_VERSION,'mpmath':mp.__version__,'numberdb':getattr(numberdb,'__version__','unknown')},
'companion_sha256':hashlib.sha256((HERE/'companion-hilbert.json').read_bytes()).hexdigest(),
'controls':['H=1+t: optimizer 1/2, C^3=27/4','H=(1+t)^3: C=27/4','independent factor optimizer on C_2: t=1/2, C=3/2^(2/3)'],
'measure':measure(values),'min_relative_accuracy_bits':min(r['relative_accuracy_bits'] for r in rows),
'rows':rows}
print(json.dumps(evidence,indent=2))
if __name__ == '__main__':
main()