back to table · edit · history · where entries came from · files · download
5438 bytes, as of the version from 2026-10-29 02:59 (current). Recorded here, not run.
# Certified computation and independent checks for T598
## Convention and primary source
Use Kabluchko and Zaporozhets, *Absorption probabilities for Gaussian polytopes
and regular spherical simplices*, Advances in Applied Probability 52 (2020),
588–616, DOI 10.1017/apr.2020.7, arXiv:1704.04968v3, Proposition 1.2(b),
equations (1.4), (1.5), (1.19), and Section 2.5. In their indexing n=d+1 and
the face has k+1 vertices. Put m=d-k and N=d+1. Then
beta[d,k] = g_m(-1/N)
= 1/sqrt(2*pi) integral_0^infinity exp(-x^2/2)
* (Phi(i*x/sqrt(N))^m + Phi(-i*x/sqrt(N))^m) dx.
Here Phi(z)=(1+erf(z/sqrt(2)))/2, with the usual error function. In particular
Phi(0)=1/2. The sentence converting Phi to erf immediately after equation
(1.6) in the source omits the factor 1/2 multiplying erf. The Gaussian integral
definition (1.6), the probability definition and the source's stated special
values resolve this typographical error. The generator uses those definitions.
The symmetry sum is entire; taking `real()` inside a complex quadrature
callback would not be an analytic function on complex neighborhoods.
The covariance is I_m-J_m/N, not a matrix with off-diagonal correlation -1/N.
The correlation is -1/d. An exact rational computation of the actual projected
rays checks their Gram matrix and its inverse at every stored pair.
## Infinite-tail bound
For y>=0, let A(y)=integral_0^y exp(t^2/2) dt. Then
|exp(-y^2/2) Phi(i*y)|^2
= exp(-y^2)/4 + exp(-y^2)*A(y)^2/(2*pi).
For 0<=y<=1, A(y)<=y*exp(y^2/2), so this expression is at most
1/4+1/(2*pi)<1. For y>=1, t^2<=y*t on [0,y], hence
A(y)<=2*(exp(y^2/2)-1)/y. The expression is therefore at most
1/4+2/(pi*y^2)<=1/4+2/pi<1. Thus |Phi(i*y)|<=exp(y^2/2) for all y>=0.
With a=1-m/N=(k+1)/(d+1)>0, the absolute omitted integral beyond T is at most
sqrt(2/pi) integral_T^infinity exp(-a*x^2/2) dx
<= sqrt(2/pi) exp(-a*T^2/2)/(a*T).
The last inequality follows from 1<=x/T for x>=T and integration of
x*exp(-a*x^2/2). The generator evaluates this bound in Arb and adds its outward
upper endpoint to the radius of the finite-interval enclosure. The integer
cutoff T is chosen so a*T^2/2>=3*(digits+30). No numerical agreement is used as
an error bound.
At 100 requested digits, arithmetic uses 500 bits (167 guard bits), with
absolute and relative quadrature targets 2^-430 (97 guard bits). Every returned
ball is required to have positive finite bounds and relative radius below
10^-110. The complete run records the actual worst radius. The facet cone is
a half-space, giving 1/2 exactly. The equilateral-triangle vertex is exactly
one sixth of the full circle. These are geometric facts, not rational guesses
from decimal digits.
## Independent algorithm
The independent checker uses 630-bit Arb quadrature for external angles,
with a real, nonnegative Gaussian integrand, integrated on [-34,34] through its
even half. Its two omitted tails are bounded by
2*exp(-34^2/2)/(34*sqrt(2*pi)), since 0<=Phi(x)^m<=1 on the real axis.
Its absolute and relative targets are 2^-560; every such result must have
relative radius below 10^-150. Known controls g_0(1)=1, g_1(1)=1/2,
g_2(1)=1/3 and g_3(1)=1/4 are computed by quadrature before any family check.
The internal quadrature also computes 1/6 and 1/2 as nonzero controls.
For the pointed tangent cone C_m(1/(k+1)), Proposition 1.3 and Remark 1.1 of
the same primary paper give
v_j = binomial(m,j) beta[k+j,k] gamma[d,k+j],
sum over j congruent to m modulo 2 of v_j = 1/2.
The boundary conventions beta[k,k]=gamma[d,d]=1 and beta[k+1,k]=1/2 are
used only inside this checking recurrence. Thus
beta[d,k] = 1/2 - sum_{0<=j<m, j congruent m mod 2}
binomial(m,j) beta[k+j,k] gamma[d,k+j].
This recovers all internal angles from the independently computed external
angles, in increasing dimension, without evaluating Phi on the imaginary
axis. Its recovered enclosures must have relative radius below 10^-140 before
comparison with the generator. In addition, every generator value is recomputed
at 140 requested digits. Agreement is required between narrow enclosures.
The checker also verifies every projected Gram matrix exactly; all 11 facet,
11 codimension-two and 10 codimension-three identities; the triangle and
tetrahedron controls; and Gram's alternating angle-sum relation for each of
the 11 simplex dimensions. The conic parity identity is evaluated on all 77
produced values, then repeated on every interval read back from the website.
Stored decimal values are interpreted with one unit of uncertainty in the last
place, not as exact point values. All finite-width comparisons enforce a
precision threshold first.
`check.py` is the unchanged campaign helper used for exactness, measurement,
named-import checks and comparison. Its `stored()` helper requires Django and
a database, so `checks.py` reads the authoritative document with the client and
uses its existing decimal-interval parser on this build machine.
## Instruction provenance
The governing manifest is
`agents/runs/20261029T024405Z-build-skills/manifest.json`.
The archived local and live skills, and this snapshot's canonical skill, all
have SHA-256
`28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199`.
The manifest and source copies are preserved in this run's artifacts.
This document explains build evidence; independent critique is a later session.