back to table · edit · history · where entries came from · files · download
9101 bytes, as of the version from 2026-10-30 12:33 (current). Recorded here, not run.
"""Independent checks for Stiefel volumes -- numberdb.org/T624.
sage -python check_values.py [--stored]
Download generate.py and check.py alongside this file. Private draft reads
need NUMBERDB_API_KEY (or NUMBERDB_KEY_FROM_STDIN=1 with the key on stdin).
Output is JSON evidence; redirect it to preserve a local check record.
"""
import json
import sys
from decimal import Decimal
from math import factorial, prod
import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.real_arb import RealBallField
from numberdb._write import to_text
from generate import StiefelVolumes, configure_key_from_stdin
from check import exactness, measure, names_its_rings, agrees_with
from pathlib import Path
R = RealBallField(600)
MANIFEST = 'agents/runs/20261030T111206Z-build-skills/manifest.json'
DIGEST = '28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199'
def unwrap(value):
return value['number'] if isinstance(value, dict) else value
def rational_decimal(text):
a, b = Decimal(str(text)).as_integer_ratio()
return QQ(a)/QQ(b)
def endpoints(text):
text = str(text)
center = rational_decimal(text)
if '.' not in text and 'e' not in text.lower():
return center, center
ulp = QQ(10)**Decimal(text).as_tuple().exponent
return center-ulp, center+ulp
def enclosure(text):
lo, hi = endpoints(text)
# Arb endpoint union is outward rounded.
return R(lo).union(R(hi))
def finite_precise(x, bits=330):
x = R(x)
assert x.is_finite() and x > 0, 'nonpositive or nonfinite value'
assert x.is_exact() or x.accuracy() >= bits, 'wide comparison ball'
return x
def contains(text, ball):
ball = finite_precise(ball)
lo, hi = endpoints(text)
return lo <= QQ(ball.lower()) and QQ(ball.upper()) <= hi
def same(a, b, bits=320):
return finite_precise(a, bits).overlaps(finite_precise(b, bits))
def gaussian_qr(field, n, k):
if (field,n,k)==('real',1,1):
return QQ(2) # Gamma(1/2)=sqrt(pi): the two-point counting volume.
beta = 1 if field == 'real' else 2
integral = R.pi()**(QQ(beta*k*(k-1))/4)
for i in range(1,k+1):
integral *= R(QQ(beta*(n-i+1))/2).gamma()/R(2)
return R(2)**(QQ(beta*k*(k-1))/4)*R.pi()**(QQ(beta*n*k)/2)/integral
def closed_complex(n,k):
return R(QQ(2)**(k*(k+1)//2)/QQ(prod(factorial(n-i) for i in range(1,k+1))))*R.pi()**(n*k-k*(k-1)//2)
def sphere(d):
if d==0:
return QQ(2)
return R(2)*R.pi()**(QQ(d+1)/2)/R(QQ(d+1)/2).gamma()
def tangent_determinant(field,n,k):
beta = 1 if field == 'real' else 2
vectors=[]
for i in range(k):
if beta==2:
vectors.append({(i,i,1):1})
for j in range(i):
vectors.append({(i,j,0):1,(j,i,0):-1})
if beta==2:
vectors.append({(i,j,1):1,(j,i,1):1})
for i in range(k,n):
for j in range(k):
for part in range(beta):
vectors.append({(i,j,part):1})
expected_dim=n*k-k*(k+1)//2 if beta==1 else 2*n*k-k*k
assert len(vectors)==expected_dim
determinant=QQ(1)
for i,v in enumerate(vectors):
determinant *= sum(x*x for x in v.values())
for w in vectors[:i]:
assert sum(x*w.get(key,0) for key,x in v.items())==0
assert determinant==QQ(2)**(beta*k*(k-1)//2)
return determinant
def flatten(document):
# This table has exactly the declared three nested parameters; also accept
# the flat API representation without depending on the Django application.
numbers=document['Numbers']
if isinstance(numbers,list):
return {(x['params']['field'],int(x['params']['n']),int(x['params']['k'])):str(x['number']) for x in numbers}
return {(f,int(n),int(k)):str(unwrap(v)) for f,ns in numbers.items() for n,ks in ns.items() for k,v in ks.items() if isinstance(ks,dict) and k not in ('param-latex','comment')}
def main():
configure_key_from_stdin()
# Known-answer and deliberate-failure controls run before the full checks.
assert same(gaussian_qr('real',1,1),2)
assert same(gaussian_qr('complex',1,1),2*R.pi())
assert same(gaussian_qr('real',2,2),4*R(2).sqrt()*R.pi())
assert same(gaussian_qr('real',3,3),32*R(2).sqrt()*R.pi()**2)
assert same(gaussian_qr('complex',2,2),8*R.pi()**3)
assert not same(gaussian_qr('real',2,2),4*R.pi())
assert not contains('3.141592653589793238462643383279502884197169399375105820974944592307816406286208998628034825342117068', R.pi()+R('1e-90'))
assert contains('2',R(2)) and not contains('2',R(3))
for bad in [R('nan'),R(0).add_error(1)]:
try: finite_precise(bad)
except AssertionError: pass
else: raise AssertionError('invalid enclosure accepted')
generator=StiefelVolumes()
assert not names_its_rings(str(Path(__file__).with_name('generate.py')))
values={}
raw={}
for params in generator.enumerate():
key=(params['field'],params['n'],params['k'])
raw[key]=generator.value(params,100)
values[key]=unwrap(raw[key])
assert len(values)==272
assert not exactness(values)
written={key:to_text(v, digits=100) for key,v in values.items()}
records=[{'params':dict(zip(generator.parameters,key)), 'number':text} for key,text in written.items()]
if '--stored' in sys.argv:
doc=numberdb.table('T624')
written=flatten(doc)
assert list(written)==list(values), 'stored selection/order differs'
report=generator.verify(sample=None)
assert report.ok, str(report)
precisions=[]
metric_checks=0
for (field,n,k),v in values.items():
finite_precise(v)
if hasattr(v,'accuracy'):
precisions.append(int(v.accuracy()))
assert contains(written[field,n,k],R(v)), ('generator containment',field,n,k)
independent=gaussian_qr(field,n,k)
assert contains(written[field,n,k],independent), ('QR containment',field,n,k)
tangent_determinant(field,n,k);metric_checks+=1
if field=='complex':
assert contains(written[field,n,k],closed_complex(n,k))
if k==1:
assert contains(written[field,n,k],sphere(n-1 if field=='real' else 2*n-1))
# Use the shared exact-comparison helper for exact rational controls.
assert not agrees_with({'real,1,1':values['real',1,1]},lambda _:QQ(2))
balls={key:enclosure(text) for key,text in written.items()}
recurrence=0; complement=0
for (field,n,k),v in balls.items():
beta=1 if field=='real' else 2
if k>=2:
rhs=balls[field,n,k-1]*R(2)**(QQ(beta*(k-1))/2)*sphere(beta*(n-k+1)-1)
assert same(v,rhs),('recurrence',field,n,k)
recurrence+=1
if k<n:
quotient=v/balls[field,k,k]
other=balls[field,n,n-k]/balls[field,n-k,n-k]
assert same(quotient,other),('complement',field,n,k)
complement+=1
# Existing tables provide controls outside the generated frame family.
sphere_doc=numberdb.table('T28')['Numbers']
hs_doc=numberdb.table('T571')['Numbers']
bures_doc=numberdb.table('T572')['Numbers']
sphere_checks=0; pure_checks=0; external_bits=[]
for field in ['real','complex']:
for n in range(1,17):
d=n-1 if field=='real' else 2*n-1
external=enclosure(unwrap(sphere_doc[str(d)]))
assert same(balls[field,n,1],external,bits=300)
if not external.is_exact(): external_bits.append(int(external.accuracy()))
sphere_checks+=1
if n>=2:
quotient=balls[field,n,1]/balls[field,1,1]
assert same(quotient,enclosure(unwrap(bures_doc[field][str(n)]['1'])))
beta=1 if field=='real' else 2
scaled=quotient*R(2)**(QQ(beta*(n-1))/2)
assert same(scaled,enclosure(unwrap(hs_doc[field][str(n)]['1'])))
pure_checks+=2
import sage.version
import yaml
summary={'table':'T624','mode':'stored' if '--stored' in sys.argv else 'local',
'skill_manifest':MANIFEST,'skill_sha256':{'local':DIGEST,'live':DIGEST},
'entries':len(values),'exact_rational_cases':['real,1,1=2'],
'working_bits':int(next(v.parent().precision() for v in values.values() if hasattr(v,'accuracy'))),
'minimum_relative_accuracy_bits':min(precisions),
'independent_working_bits':600,'serialized_containment_checks':2*len(values),
'metric_gram_determinants':metric_checks,'complex_factorial_checks':136,
'recurrences':recurrence,'complementary_quotient_checks':complement,
'minimum_live_sphere_accuracy_bits':min(external_bits),'live_sphere_checks':sphere_checks,'live_pure_state_checks':pure_checks,
'known_answer_controls':5,'deliberate_failure_controls':5,
'serialized_measure':measure(written),
'flat_entry_block_bytes':len(yaml.safe_dump(records).encode()),
'sage_version':sage.version.version,'numberdb_version':numberdb.__version__,
'all_checks_passed':True}
print(json.dumps(summary,indent=2))
if __name__=='__main__':main()