back to table · edit · history · where entries came from · files · download
9477 bytes, as of the version from 2026-10-30 12:05. 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 '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():
if isinstance(value,dict): 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()