checks.py

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

7443 bytes, as of the version from 2026-10-29 03:43. Recorded here, not run.

"""Checks for Ray–Singer torsion of lens spaces -- numberdb.org/T599.

Run: sage -python checks.py
This is build evidence, not the campaign's independent critique. It checks
all 286 default entries using mpmath log-gamma (not sine), controls of known
value, exact cyclotomic arithmetic, character symmetries, product identities,
and decimal enclosure containment. --stored checks a downloaded document as
well. Set NUMBERDB_KEY_FROM_STDIN=1 to read a draft key from stdin.
"""
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.integer_ring import ZZ
from sage.rings.real_arb import RealBallField
from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
from numberdb._write import to_text
from fractions import Fraction
from functools import lru_cache
import mpmath as mp
import json
import sys
import os
from math import gcd
from generate import LensTorsion, torsion_ball

mp.mp.dps = 175
RB = RealBallField(600)


def rational(text):
    a = Fraction(str(text))
    return QQ(a.numerator)/a.denominator


def interval(text):
    text = str(text)
    if '.' not in text and 'e' not in text.lower():
        x = rational(text)
        return x, x
    # The generator intentionally emits only ordinary fixed-point decimals.
    assert 'e' not in text.lower() and '+/-' not in text and '[' not in text
    unit = QQ(1)/ZZ(10)**len(text.split('.')[1])
    x = rational(text)
    return x-unit, x+unit


@lru_cache(None)
def log_gamma_pair(a, p):
    x = mp.mpf(a)/p
    return mp.loggamma(x)+mp.loggamma(1-x)


def independent(p, q, u):
    # Inverse found by exhaustive search, independent of pow(q,-1,p).
    r = next(k for k in range(1, p) if (k*q) % p == 1)
    v = (u*r) % p
    return mp.exp(2*mp.log(2*mp.pi)-log_gamma_pair(u,p)-log_gamma_pair(v,p))


def known_controls():
    for p,expected in [(2,4),(3,3),(4,2),(6,1)]:
        assert abs(independent(p,1,1)-expected) < mp.mpf('1e-165')
        assert LensTorsion().value({'p':p,'q':1,'u':1},100) == expected
    assert abs(independent(5,2,1)-mp.sqrt(5)) < mp.mpf('1e-165')
    # A sign/inverse-sensitive presentation: replacing q^{-1} by q fails.
    a=independent(7,2,1)
    wrong=4*mp.sin(mp.pi/7)*mp.sin(2*mp.pi/7)
    assert abs(a-wrong)>mp.mpf('0.1')


def selection_check(params):
    expected=[]
    for p in range(2,21):
        unused={q for q in range(1,p) if gcd(p,q)==1}
        while unused:
            q=min(unused)
            inverse=next(r for r in range(1,p) if q*r%p==1)
            unused -= {q,p-q,inverse,p-inverse}
            for u in range(1,p//2+1): expected.append((p,q,u))
    assert params==expected and len(params)==len(set(params))


def check_numbers(records):
    generator=LensTorsion()
    known_controls()
    params=[tuple(int(row['params'][k]) for k in ('p','q','u')) for row in records]
    selection_check(params)
    exact=[];bits=[];errors=[];balls={};texts={};types=set()
    for row,(p,q,u) in zip(records,params):
        text=str(row['number']); lo,hi=interval(text)
        balls[p,q,u]=RB(lo).union(RB(hi));texts[p,q,u]=text;types.add((p,q))
        b=torsion_ball(p,q,u)
        v=generator.value(dict(p=p,q=q,u=u),100)
        if lo==hi:
            assert v in QQ and QQ(v)==lo
            assert lo in b
            exact.append({'p':p,'q':q,'u':u,'value':str(lo)})
        else:
            assert b >= RB(lo) and b <= RB(hi)
            bits.append(int(b.accuracy()))
            assert len(text.replace('.','').lstrip('0')) == 100
        alternative=independent(p,q,u)
        error=abs(alternative-mp.mpf(str(b.mid())))/alternative
        assert error < mp.mpf('1e-145')
        errors.append(error)
        assert b.overlaps(torsion_ball(p,q,p-u))
        assert b.overlaps(torsion_ball(p,p-q,u))
        r=next(k for k in range(1,p) if k*q%p==1)
        assert b.overlaps(torsion_ball(p,r,u*r%p))
        # Read-back interval also contains independent evaluations of each symmetry.
        for qq,uu in [(q,p-u),(p-q,u),(r,u*r%p)]:
            w=independent(p,qq,uu)
            if lo!=hi:
                assert mp.mpf(str(lo.numerator()))/int(lo.denominator()) < w
                assert w < mp.mpf(str(hi.numerator()))/int(hi.denominator())
            else:
                assert abs(w-mp.mpf(str(lo))) < mp.mpf('1e-165')
    for p,q in types:
        product=RB(1)
        for u in range(1,p): product *= balls[p,q,min(u,p-u)]
        assert p*p in product
        assert RB(product.rad()) < RB('1e-90')
    # Independent exact algebraic evaluations in Q[z]/Phi_p using a separately
    # constructed root of unity, checking rational classification on every row.
    R=PolynomialRing(QQ,'z');z=R.gen()
    for row,(p,q,u) in zip(records,params):
        K=R.quotient(R.cyclotomic_polynomial(p),'w');w=K.gen()
        r=next(k for k in range(1,p) if k*q%p==1)
        a=1-w**u;c=1-w**(u*r)
        square=(a*(1-w**((-u)%p))*c*(1-w**((-u*r)%p))).lift()
        lo,hi=interval(row['number'])
        is_rational=square.degree()==0 and square[0].is_square()
        assert (lo==hi)==is_rational
        if is_rational: assert lo>0 and lo**2==square[0]
    return {'entries':len(records),'lens_space_types':len(types),'rational_entries':len(exact),
            'nonrational_entries':len(bits),'minimum_ball_accuracy_bits':min(bits),
            'maximum_relative_gamma_discrepancy':mp.nstr(max(errors),10),
            'working_bits':500,'stored_significant_digits':100,
            'exact_values':exact,'all_decimal_intervals_contain_computed_balls':True,
            'all_symmetries_checked':True,'all_character_products_contain_p_squared':True,
            'rational_classification_checked_by_exact_cyclotomic_arithmetic':True,
            'gamma_check_dps':175,'gamma_relative_agreement_threshold':'1e-145',
            'gamma_controls':'T(2,1,1)=4; T(3,1,1)=3; T(4,1,1)=2; T(6,1,1)=1; T(5,2,1)=sqrt(5)',
            'inverse_negative_control':'T(7,2,1) differs from the erroneous q-instead-of-inverse result by >0.1',
            'longest_written_value':max(len(str(r['number'])) for r in records),
            'skill_manifest':'agents/runs/20261029T032928Z-build-skills/manifest.json',
            'skill_sha256':'28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199',
            'versions':{'mpmath':mp.__version__,'numberdb':getattr(numberdb,'__version__','see package metadata')}}


def run(stored=False,client=None):
    if stored:
        document=numberdb.table('T599',client=client)
        records=document['Numbers']
        if isinstance(records,dict):
            records = [{'params': {'p': p, 'q': q, 'u': u}, 'number': v}
                       for p, qs in records.items() for q, us in qs.items()
                       for u, v in us.items()]
        if not isinstance(records,list):
            raise ValueError('Expected flat or p/q/u-grouped stored records')
    else:
        g=LensTorsion()
        records=[{'params':p,'number':to_text(g.value(p,100),100)} for p in g.enumerate()]
    result=check_numbers(records)
    result['checked_stored_document']=stored
    print(json.dumps(result,indent=2))


if __name__=='__main__':
    client=None
    if os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1':
        key=sys.stdin.read().strip()
        if '=' in key and key.split('=',1)[0].isupper(): key=key.split('=',1)[1].strip().strip('\"\'')
        client=numberdb.Client(api_key=key)
    run('--stored' in sys.argv,client)