back to table · edit · history · where entries came from · files · download
5411 bytes, as of the version from 2026-11-11 03:31 (current). Recorded here, not run.
# Computation and error bounds for T715
This is builder evidence. Independent scientific and argument-selection verdicts
must be written by a separate critic. The source bundle is identified by
skill-manifest.json (bundle SHA-256
d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab).
## Moment identity and conventions
Put c_n=binomial(2n,n). For integer p>=1,
U_p(v) = 1/(p-1)! integral_0^1 (-log x)^(p-1) / sqrt(1-4v x^2) dx.
Expand the binomial kernel and use integral_0^1 x^(2n)(-log x)^(p-1) dx
= (p-1)!/(2n+1)^p. The absolute series converges even at |v|=1/4,
since its terms are O(n^(-p-1/2)), justifying interchange. This derivation
is also the normalized content of CGLXZ Lemma 2.1 after v=+/-z^2 and an
order shift. The n=0 term remains 1. All square roots and logarithms in the
real integral are their positive/principal real values.
## Generator
The 100-digit evaluation uses target=bits(125)=432 and 944 working bits.
Every returned object must be a finite RealBall with radius below 10^-115.
Interior: sum n=0,...,N-1 using c_(n+1)v^(n+1)/(c_n v^n)
=2v(2n+1)/(n+1). With q=4|v|<1, c_n<=4^n gives an absolute tail at most
q^N / ((1-q)(2N+1)^p).
N is chosen by the exact rational inequality q^N/(1-q)<=2^-432.
Here N=217. All divisions in exact coefficients use QQ, and all approximate
arithmetic and the remainder are enclosed by Arb balls.
Negative endpoint: a_n=c_n/(4^n(2n+1)^p) is a Hausdorff moment sequence.
Indeed c_n/4^n is the nth moment of the probability density
1/(pi sqrt(t(1-t))) on [0,1]; (2n+1)^(-p) is the 2nth moment of the probability
density (-log x)^(p-1)/(p-1)! on [0,1]. Thus a_n is the nth moment of Y=t x^2
under the product measure. In particular 0<=Y<=1. For
D^k a_0=sum_{j=0}^k (-1)^j binomial(k,j)a_j = E[(1-Y)^k],
U_p(-1/4) = sum_{k>=0} D^k a_0 / 2^(k+1).
This is the geometric expansion of E[1/(1+Y)]. The omitted tail from k=N
is E[(1-Y)^N/(2^N(1+Y))], between zero and 2^-N. We use N=432 and add
2^-432 to the radius. Forward differences are computed in 944-bit balls;
the extra precision covers cancellation, and the final radius assertion
checks the resulting enclosure. No assertion of exactness comes from decimal
patterns or successful upload.
Positive endpoint: for |h|<1, summing the logarithmic moments gives
sum_{m>=0} U_(m+1)(1/4) h^m
= 1/2 B((1-h)/2,1/2)
= pi/2 exp(log(2)h + sum_{k>=2}(1-2^(1-k)) zeta(k) h^k/k).
The first equality follows by integrating x^(-h)/sqrt(1-x^2) and setting
t=x^2 (DLMF 5.12.1). Gamma duplication (5.5.5) rewrites the beta quotient as
(pi/2) 2^h Gamma(1-h)/Gamma(1-h/2)^2; the Taylor expansion of log Gamma
(5.7.3) gives the last expression. If its exponent is sum a_k h^k,
coefficients e_0=1 and e_m=(1/m)sum_{k=1}^m k a_k e_(m-k) suffice.
Only coefficients through m=p-1 are used; there is no truncation error from
higher formal coefficients. Arb encloses pi, log(2), zeta(k), and arithmetic.
## Independent integral enclosure
checks.py imports no generator. Let a=2sqrt(|v|), theta=asin(a) for v>0
and theta=asinh(a) for v<0; let f=sin or sinh respectively. Substitution
x=f(s)/a in the moment integral, followed by s=theta exp(-t), gives
U_p(v) = theta/(a(p-1)!) integral_0^infinity
exp(-t) log(a/f(theta exp(-t)))^(p-1) dt.
All inputs are computed afresh from exact rationals. This is a smooth integral
on the nonnegative real axis. The logarithm is real and nonnegative there;
analytic continuation is permitted only where Arb's log(analytic=True)
certifies it. Complex-ball quadrature on [0,420] uses 450 bits and absolute
and relative tolerances 10^-120. The imaginary enclosure must contain zero.
For 0<=s<=theta<=pi/2, sin(s)>=2s/pi and sin(theta)<=theta. Thus in the
positive case log(a/sin(theta exp(-t))) <= t+log(pi/2) < t+1.
In the negative case sinh(s)>=s and theta<=asinh(1)<1, so
sinh(theta)/theta <= sinh(1) < exp(1), giving the same bound. Also theta/a<2
in both cases. The positive tail after L therefore is bounded by
2 exp(-L) sum_{k=0}^{p-1} (L+1)^k/k!.
This follows by integrating the integer incomplete-gamma polynomial exactly.
We add that bound to the quadrature radius and require radius <10^-110.
Every decimal is interpreted as its full last-place uncertainty interval;
the whole independent enclosure, not only its midpoint, must lie inside it.
Both methods share Arb arithmetic and the mathematical moment identity, but
they use different algorithms and no shared numerical implementation.
Known controls: all four p=1 arcsin/asinh evaluations, plus
U_2(1/4)=pi log(2)/2. Negative controls omit the initial term, reverse the sign,
perturb by five stored last-place units, use a radius of 100, and use NaN.
Every negative control must be rejected. Full results are in check-results.json
and, after upload, stored-check-results.json. No sibling table is used as the
independent numerical oracle.
## Related identities
CGLXZ Lemma 2.1 implies U_p(1/16)=(-1)^p Ls_p(pi/3)/(p-1)! and
U_p(-1/16)=(-1)^p Lsh_p(2log(phi))/(p-1)!, phi=(1+sqrt(5))/2.
These also follow directly by the above substitution because 2sin(theta)=1
or 2sinh(theta)=1. This proves the normalization for every p, rather than
inferring it from finite numerical agreement. T697 and T713 contain the
corresponding logarithmic moments; cross-table comparisons check link
conventions only and are not independent verification of this table.