back to table · edit · history · where entries came from · files · download
3363 bytes, as of the version from 2026-11-09 23:51 (current). Recorded here, not run.
# Certified evaluation of T697
Instruction provenance is the attached skill-manifest.json, originally
`agents/runs/20261109T220207Z-build-skills/manifest.json`. Both archived skill
SHA-256 values are 886390324dd1971e381a43cf3b46b822ab0bc67d62f31d8481e29ec79556746b.
Put theta=pi*t, p=n-1-k, A=log(theta), q=(t/2)^2, and v=theta*x.
For 0<x<=1 and 0<t<=1, Euler's sine product (DLMF 4.22.1) gives
log(2 sin(v/2)) = A + log(x) + H(x),
H(x) = -sum_{m>=1} zeta(2m)/m * q^m * x^(2m).
For j=0,...,p the generator computes exactly the first N+1 coefficients of
H(x)^j in y=x^2, with every coefficient enclosed by Arb. Repeated polynomial
multiplication followed by truncation is valid because H has zero constant
coefficient; omitted coefficients can never contribute to a lower degree.
The constant power H^0=1 is retained exactly.
The integrals of each retained term are evaluated analytically:
J_d(r) = integral_0^1 x^(r-1) (A+log(x))^d dx,
J_0(r)=1/r, J_d(r)=(A^d-d*J_(d-1)(r))/r.
Here r=k+2m+1>0. This recurrence is integration by parts; its boundary at
zero vanishes even when the logarithm is singular. Thus the retained answer is
-theta^(k+1) times sum_j binomial(p,j) sum_m [H^j]_m J_(p-j)(k+2m+1).
There is no numerical endpoint cutoff.
For the remainder, let b_m=zeta(2m)/m>0 and B(z)=sum b_m*z^m.
Since zeta(2m)<2, B(1/2)<2 log(2)=C. All coefficients c_(j,m) of B(z)^j
are nonnegative. For 0<q<=1/4,
sum_{m>N} c_(j,m) q^m
<= (2q)^(N+1) sum_{m>N} c_(j,m) (1/2)^m
<= (2q)^(N+1) C^j.
This bounds the absolute tail of H(x)^j uniformly for x in [0,1], including
all omitted products, not just the tail of H. The remaining logarithm has
an integrable majorant:
integral_0^1 x^k |A+log(x)|^d dx
<= sum_{l=0}^d binomial(d,l) |A|^(d-l) l!/(k+1)^(l+1) = M_d.
Consequently the absolute error is at most
E=theta^(k+1) sum_{j=1}^p binomial(p,j) C^j (2q)^(N+1) M_(p-j).
The generator computes E in real ball arithmetic and adds its upper endpoint
to the answer's radius. Arithmetic error, the rational input t, pi, logarithms,
zeta coefficients, polynomial operations and integrals are all enclosed as
well. At 100 requested digits it uses numberdb.bits(100, losing=192) working
bits and N=numberdb.bits(160, losing=0). These fixed guards are checked by
measuring the minimum returned accuracy over the entire selection and by
recomputing at 140 requested digits. Every nonzero answer must retain at least
numberdb.bits(digits+20, losing=0) accurate bits. numerical-evidence.json gives
the actual counts and worst case.
The single exact zero is Ls_2(pi). The identity
Gamma(1+s)/Gamma(1+s/2)^2 = -(1/pi) sum_{m>=0} Ls_(m+1)(pi) s^m/m!
(Borwein–Straub equation (8)) has zero linear coefficient, proving that value
is exactly zero. The script also computes the series enclosure without this
shortcut and checks that it contains zero with a small absolute radius.
Independent checks use direct mpmath tanh-sinh quadrature at 130 and 170 decimal
digits, Gamma-ratio coefficients, and finite polylogarithm expressions for every
one-logarithm moment. These checks are not used to create the radii. Controls
with known nonzero integrals run before the comparisons. The stored decimal's
one-last-place interval is required to contain the full higher-precision Arb
ball; agreement of midpoints alone is insufficient.