postfill.py

back to table · edit · history · where entries came from · files · download

2636 bytes, as of the version from 2026-10-29 00:39. Recorded here, not run.

"""Read back T595 and verify its actual written intervals.

Run: sage -python postfill.py < key-file
The key is used only for NumberDB API reads. Keep generate.py and
numerical-evidence.json alongside this file. No writes are performed.
"""
import json
import sys
from decimal import Decimal
from fractions import Fraction
from pathlib import Path
import numberdb.sage as numberdb
from numberdb._generate import _stored_entries
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from generate import SphereDeterminants, logdet


def rational(s):
    f=Fraction(s)
    return QQ(f.numerator)/f.denominator


def stored_interval(s, R):
    center=rational(s)
    exponent=int(Decimal(s).as_tuple().exponent)
    ulp=QQ(10)**exponent
    return R(center).add_error(R(ulp))


def check_stored(client):
    g=SphereDeterminants()
    verification=g.verify(sample=None,client=client)
    assert verification.ok
    document=numberdb.table('T595',client=client)
    entries=_stored_entries(document)
    expected=[','.join(p.values()) for p in g.enumerate()]
    assert list(entries)==expected
    evidence=json.loads(Path(__file__).with_name('numerical-evidence.json').read_text())
    R=RealBallField(800)
    written={key:stored_interval(value,R) for key,value in entries.items()}
    rejected=0
    for row in evidence['rows']:
        d=row['d']
        reference=R(rational(row['independent_logdet'])).add_error(R(QQ(1)/10**130))
        determinant=reference.exp()
        actualL=written[f'{d},logdet']; actualD=written[f'{d},det']
        for actual,reference_value,generated in (
            (actualL,reference,logdet(d,200)),
            (actualD,determinant,logdet(d,200).exp())):
            assert actual.is_finite() and reference_value.is_finite()
            assert actual.contains(reference_value)
            assert actual.contains(R(generated))
            assert not actual.contains(reference_value+R(QQ(1)/10**90))
            rejected+=1
        assert actualD.log().overlaps(actualL)
        assert actualL.exp().overlaps(actualD)
    return {'table':'T595','verification':str(verification),
            'entries_checked':len(entries),'independent_interval_containments':40,
            'production_ball_containments':40,'convention_pairs_checked':20,
            'perturbed_controls_rejected':rejected,
            'ordered_enumeration_matches':True,
            'longest_stored_value_characters':max(map(len,entries.values()))}


if __name__=='__main__':
    client=numberdb.Client(api_key=sys.stdin.read().strip(),as_sage=True)
    print(json.dumps(check_stored(client),indent=2))