generate.py

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

4494 bytes, as of the version from 2026-10-29 02:42 (current). Recorded here, not run.

"""External solid angles of regular simplices -- numberdb.org/T597.

Run with SageMath (or a compatible passagemath installation):
    sage -pip install numberdb
    sage -python generate.py                  # verify every stored entry
    sage -python generate.py --fill           # fill the existing draft
The latter needs NUMBERDB_API_KEY. It writes entries, not publication status.

The default enumeration is all 2 <= d <= 12 and 0 <= k < d, in that order.
See argument-selection.md for the choice of extent. The sphere has measure 1.
Kabluchko and Zaporozhets (2020), Proposition 1.2(a), gives
    gamma[d,k] = E[Phi(Z/sqrt(k+1))**(d-k)], Z standard normal.
Exact values: gamma[d,0] = 1/(d+1), gamma[d,d-1] = 1/2.

Arb encloses the entire integrand on [-T,T]. Because 0 <= Phi <= 1,
the sum of both omitted tails is at most 2*phi(T)/T (Mills' bound).
This positive bound is added as a symmetric ball radius. T is an integer
chosen from the requested decimal digits, not a rounded integration limit.
The integrand is entire, so the analytic callback flag needs no restriction.
80 guard bits and an integration goal of digits+15 decimal places were
measured on the full default enumeration; checks.py rejects any returned
relative radius >= 10**(-digits-10). Ball widths, not the goal, certify output.

This run uses the matched archived skill copies recorded in skill-evidence.json;
the controlling manifest is agents/runs/20261029T020934Z-build-skills/manifest.json.
"""
import os
import sys
from math import isqrt
from pathlib import Path

import numberdb.sage as numberdb
from sage.rings.rational_field import QQ
from sage.rings.complex_arb import ComplexBallField
from sage.rings.real_arb import RealBallField

WORKING_GUARD = 80


def quadrature(d, k, digits=100):
    """Certified quadrature, including for the exact-value controls."""
    d, k = int(d), int(k)
    if not (d >= 2 and 0 <= k < d):
        raise ValueError('require d >= 2 and 0 <= k < d')
    precision = numberdb.bits(digits, losing=WORKING_GUARD)
    C = ComplexBallField(precision)
    R = RealBallField(precision)
    m = d-k
    scale = C(2*(k+1)).sqrt()
    normalizer = (2*C.pi()).sqrt()
    T = isqrt(5*(digits+20))+1
    tolerance = R(10)**(-digits-15)

    def integrand(z, analytic):
        return (-z*z/2).exp()*((1+(z/scale).erf())/2)**m/normalizer

    integral = C.integral(integrand, -T, T,
                          abs_tol=tolerance, rel_tol=tolerance)
    if (not integral.real().is_finite() or not integral.imag().is_finite()) or not integral.imag().contains_zero():
        raise ArithmeticError('nonfinite or nonreal integral')
    tail = 2*(-R(T)**2/2).exp()/(R(T)*(2*R.pi()).sqrt())
    result = integral.real()+R(0, tail.upper())
    if not result.is_finite() or not 0 < result < 1:
        raise ArithmeticError('invalid probability enclosure')
    if not R(result.rad()) < abs(R(result.center()))*R(10)**(-digits-10):
        raise ArithmeticError('not enough certified precision')
    return result


class ExternalSimplexAngles(numberdb.Generator):
    table = 'T597'
    parameters = ('d', 'k')
    type = 'R'
    digits = 100
    rigour = 'proven'
    files = ('generate.py', 'checks.py', 'argument-selection.md',
             'numerical-evidence.md', 'skill-evidence.json')

    def enumerate(self, max_dimension=12):
        for d in range(2, max_dimension+1):
            for k in range(d):
                yield {'d': d, 'k': k}

    def value(self, params, digits):
        d, k = int(params['d']), int(params['k'])
        if not (d >= 2 and 0 <= k < d):
            raise ValueError('require d >= 2 and 0 <= k < d')
        if k == 0:
            return QQ(1)/(d+1)
        if k == d-1:
            return QQ(1)/2
        return quadrature(d, k, digits)


if __name__ == '__main__':
    if os.environ.get('NUMBERDB_KEY_FROM_STDIN') == '1':
        key = sys.stdin.read().strip()
        if '=' in key and key.split('=', 1)[0].replace('_','').isalnum():
            key = key.split('=', 1)[1].strip().strip('\"\'')
        numberdb.configure(api_key=key)
    generator = ExternalSimplexAngles()
    if '--fill' in sys.argv or os.environ.get('NUMBERDB_PUBLISH') == '1':
        print(generator.publish(message='Fill 77 simplex face angles with certified values',
                                assisted_by=os.environ.get('NUMBERDB_ASSISTED_BY','codex-cli')))
    else:
        report = generator.verify(sample=None)
        print(report)
        sys.exit(0 if report.ok else 1)