check_values.py

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

9586 bytes, as of the version from 2026-10-30 12:10. Recorded here, not run.

"""Checks for Grassmann volumes -- numberdb.org/T625.

Run: sage -python check_values.py (local checks); add --stored to read the draft.
Set NUMBERDB_API_KEY for private-table reads, or pipe a key with
NUMBERDB_KEY_FROM_STDIN=1 under the campaign wrapper. Online mode is automatic
under that wrapper. Results are JSON on stdout; redirect to retain evidence.
This imports generate.py and the unmodified campaign check.py. The latter is
attached for reproducibility. No check changes or offers a table.

Independent calculations: sphere recurrence and full group quotient, direct
600-bit Gamma products, and recursively counted rectangular standard Young
tableaux for complex coefficients. Projective cases are compared to T27, T28,
T571 and T572. Source and metric derivations are in mathematical-checks.md.
"""
import os,sys,json
from functools import lru_cache
from fractions import Fraction
from decimal import Decimal
from math import factorial
import numberdb.sage as numberdb
from numberdb._write import to_text
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from generate import GrassmannVolumes, exact_form
from check import exactness, names_its_rings, measure

R = RealBallField(600)


def bounds(text):
    text=str(text).strip()
    if '.' not in text and 'e' not in text.lower():
        return QQ(text), QQ(text)
    d=Decimal(text)
    c=QQ(Fraction(d))
    u=QQ(10)**int(d.as_tuple().exponent)
    return c-u,c+u


def contains(text, value):
    assert value.is_finite() and value > 0
    assert value.accuracy() >= 350
    lo,hi=bounds(text)
    return bool(R(lo) < value and value < R(hi))


def written_ball(text):
    a,b=bounds(text)
    return R((a+b)/2).add_error(R((b-a)/2))


def overlap(a,b):
    assert a.is_finite() and b.is_finite() and a > 0 and b > 0
    assert min(a.accuracy(),b.accuracy()) >= 315
    return a.overlaps(b)


@lru_cache(None)
def sphere(d):
    if d==0: return R(2)
    if d==1: return 2*R.pi()
    return 2*R.pi()*sphere(d-2)/R(d-1)


def group(field,n):
    beta=1 if field=='real' else 2
    v=R(1)
    for j in range(1,n+1):
        v *= sphere(beta*j-1)
    return v*R(2)**(QQ(beta*n*(n-1))/4)


def group_quotient(field,n,k):
    beta=1 if field=='real' else 2
    return group(field,n)/group(field,k)/group(field,n-k)/R(2)**(QQ(beta*k*(n-k))/2)


def gamma_product(field,n,k):
    beta=1 if field=='real' else 2
    ans=R.pi()**(QQ(beta*k*(n-k))/2)
    for j in range(k):
        ans *= R(QQ(beta*(k-j))/2).gamma()/R(QQ(beta*(n-j))/2).gamma()
    return ans


@lru_cache(None)
def tableaux(shape):
    if not shape: return 1
    total=0
    for i,x in enumerate(shape):
        if i==len(shape)-1 or x>shape[i+1]:
            child=list(shape); child[i]-=1
            total += tableaux(tuple(y for y in child if y))
    return total


def records(doc):
    block=doc['Numbers']
    if isinstance(block,list): return block
    out=[]; names=list(doc['Parameters'])
    def walk(node,params):
        if len(params)==len(names) and not isinstance(node,dict):
            out.append({'params':params, 'number':str(node)}); return
        if 'number' in node:
            out.append(dict(node,params=params)); return
        if 'numbers' in node: node=node['numbers']
        name=names[len(params)]
        for key,value in node.items():
            walk(value,dict(params,**{name:str(key)}))
    walk(block,{})
    return out


def keyed(doc):
    names=list(doc['Parameters'])
    return {tuple(str(r['params'][n]) for n in names):r['number'] for r in records(doc)}


def metric_checks():
    # Sparse real coordinates for complex entries: (row, col, real_or_imag).
    # Their Frobenius inner product is the ordinary dot product on these slots.
    def dot(a,b): return sum(QQ(v)*b.get(i,0) for i,v in a.items())
    coordinate_tests=0
    for beta in (1,2):
        for n in range(2,17):
            for k in range(1,n//2+1):
                tangent=[]
                for a in range(n-k):
                    for b in range(k):
                        for component in range(beta):
                            t={(k+a,b,component):1,(b,k+a,component):(-1 if component else 1)}
                            tangent.append(t)
                for i,t in enumerate(tangent):
                    assert dot(t,t)/2==1
                    for s in tangent[:i]: assert dot(t,s)==0
                assert len(tangent)==beta*k*(n-k)
                coordinate_tests += len(tangent)
                # Real Stiefel: skew frame rotations double their squared norms.
                if beta==1:
                    determinant=QQ(1)
                    for a in range(k):
                        for b in range(a):
                            A={(a,b,0):1,(b,a,0):-1}
                            ratio=dot(A,A)/(dot(A,A)/2)
                            determinant *= ratio
                    assert determinant==2**(k*(k-1)//2)
    return coordinate_tests


def main():
    online='--stored' in sys.argv or os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1'
    if os.environ.get('NUMBERDB_KEY_FROM_STDIN')=='1':
        key=sys.stdin.read().strip()
        if key.startswith('NUMBERDB_'): key=key.split('=',1)[1].strip().strip('\"\'')
        numberdb.configure(api_key=key)
    # Known answers first; the parser and numerical comparisons must reject errors.
    assert bounds('3.14')==(QQ(313)/100,QQ(315)/100)
    assert bounds('1.25e-4')==(QQ(124)/10**6,QQ(126)/10**6)
    assert tableaux((2,2))==2 and tableaux((3,3))==5
    assert overlap(sphere(2),4*R.pi()) and overlap(sphere(3),2*R.pi()**2)
    assert overlap(group_quotient('real',4,2),2*R.pi()**2)
    assert overlap(group_quotient('complex',4,2),R.pi()**4/12)
    assert contains(to_text(R.pi(),100),R.pi())
    assert not contains(to_text(R.pi(),100),R.pi()+R(QQ(1)/10**97))
    assert not overlap(R.pi(),2*R.pi())
    g=GrassmannVolumes(); params=list(g.enumerate())
    assert len(params)==128
    values={tuple(str(p[name]) for name in g.parameters):g.value(p,100) for p in params}
    assert not exactness(values)
    assert not names_its_rings(os.path.join(os.path.dirname(__file__),'generate.py'))
    texts={k:to_text(v,100) for k,v in values.items()}
    if online:
        stored=keyed(numberdb.table('T625'))
        assert list(stored)==list(texts)
        texts=stored
    least=1000
    coeffs={}; counters={'gamma':0,'group_quotient':0,'complement':0,'tableaux':0,'recurrence':0}
    for key,value in values.items():
        field,n,k=key; n=int(n);k=int(k)
        least=min(least,int(value.accuracy()))
        assert contains(texts[key],value),('generator enclosure',key)
        assert contains(texts[key],gamma_product(field,n,k)),('gamma',key)
        counters['gamma']+=1
        assert contains(texts[key],group_quotient(field,n,k)),('group',key)
        counters['group_quotient']+=1
        c,e=exact_form(field,n,k)
        assert c>0 and e>=1  # No rational cases in this selected domain.
        coeffs[','.join(key)]={'coefficient':str(c),'pi_power':e}
        assert (c,e)==exact_form(field,n,n-k)
        assert contains(texts[key],group_quotient(field,n,n-k))
        counters['complement']+=1
        if field=='complex':
            assert e==k*(n-k)
            assert c*factorial(e)==tableaux((n-k,)*k)
            assert contains(texts[key],R(tableaux((n-k,)*k))*R.pi()**e/R(factorial(e)))
            counters['tableaux']+=1
        beta=1 if field=='real' else 2
        previous=(field,str(n-1),str(k))
        if previous in texts:
            ratio=R.pi()**(QQ(beta*k)/2)*R(QQ(beta*(n-k))/2).gamma()/R(QQ(beta*n)/2).gamma()
            assert overlap(written_ball(texts[key]),written_ball(texts[previous])*ratio)
            counters['recurrence']+=1
    if online:
        companions={tid:keyed(numberdb.table(tid)) for tid in ['T624','T27','T28','T571','T572']}
        quotient_count=pure_count=0
        for key,text in texts.items():
            field,n,k=key
            a=written_ball(companions['T624'][key]); b=written_ball(companions['T624'][(field,k,k)])
            assert overlap(written_ball(text),a/b),('stored Stiefel quotient',key)
            quotient_count+=1
            if k=='1':
                N=int(n); beta=1 if field=='real' else 2
                assert overlap(written_ball(text),written_ball(companions['T572'][(field,n,'1')]))
                scale=R(2)**(QQ(beta*(N-1))/2)
                assert overlap(written_ball(text)*scale,written_ball(companions['T571'][(field,n,'1')]))
                if field=='real': control=written_ball(companions['T28'][(str(N-1),)])/2
                else: control=written_ball(companions['T27'][(str(2*(N-1)),)])
                assert overlap(written_ball(text),control)
                pure_count+=3
        counters.update(stored_stiefel=quotient_count,stored_projective_controls=pure_count)
    out={'table':'T625','mode':'stored' if online else 'local','entries':128,
         'skill_manifest':'agents/runs/20261030T115517Z-build-skills/manifest.json',
         'skill_sha256':'28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199',
         'working_bits':numberdb.bits(100,losing=64),'least_relative_accuracy_bits':least,
         'measurement':measure(texts),'metric_coordinates_checked':metric_checks(),
         'checks':counters,'controls':'passed, including intentional corrupted value',
         'exact_forms':coeffs,'values':{','.join(k):v for k,v in texts.items()},
         'versions':{'numberdb':numberdb.__version__,'python':sys.version}}
    print(json.dumps(out,indent=2))

if __name__=='__main__': main()