back to table · edit · history · where entries came from · files · download
3281 bytes, as of the version from 2026-11-09 09:52 (current). Recorded here, not run.
# Certification of the values in T685
The skill manifest is `agents/runs/20261109T080742Z-build-skills/manifest.json`,
attached as `skill-manifest.json`; both archived versions have SHA-256
`886390324dd1971e381a43cf3b46b822ab0bc67d62f31d8481e29ec79556746b`.
The numerical results and measured precision are in `numerical-evidence.json`.
For n=3, Jensen's formula gives
M_(3,k) = (2/3) integral_0^1 log(2 cos(pi t/3))^k dt.
The logarithm's argument ranges from 2 to 1. The generator passes Arb's
analytic flag through to the complex logarithm so the adaptive integrator
cannot use a region crossing its branch cut. Arb encloses pi, the integrand
and the integral. The imaginary enclosure must contain zero and the real
answer must be finite and meet the relative-accuracy requirement.
For n=4, BS Theorem 3.3 gives M_(4,k) = integral_0^1 g(t)^k dt with
g(t) = t log(2 sin(pi t/2)) + Cl_2(pi t)/pi, g(0)=0.
Differentiation, using Cl_2'(theta)=-log(2 sin(theta/2)), gives
g'(t) = (pi t/2) cot(pi t/2).
The partial fraction expansion of cotangent (DLMF 4.22.3,
https://dlmf.nist.gov/4.22.E3), expanded as geometric series,
therefore yields, throughout 0 <= t <= 1,
g(t) = t [1 - 2 sum_(m>=1) zeta(2m) (t/2)^(2m)/(2m+1)].
Let h_N(u)=1-2 sum_(m=1)^N zeta(2m) u^m / ((2m+1)4^m), and p_N(t)=t h_N(t^2).
Every omitted coefficient has negative sign. Since zeta(2m) < 2, uniformly
0 <= p_N(t)-g(t)
<= 4 sum_(m=N+1)^infinity 4^(-m)/(2m+1)
<= 16/[3(2N+3)4^(N+1)] = E.
Also g increases from 0 to log(2)<1, because its derivative is nonnegative
on [0,1]. Thus 0<=g<=1 and 0<=p_N<=1+E, giving
|p_N(t)^k-g(t)^k| <= k(1+E)^(k-1) E.
If h_N(u)^k = sum_j a_j u^j, then the polynomial integral is exactly
sum_j a_j/(k+2j+1). Arb ball coefficients enclose every zeta value and all
arithmetic; adding the displayed uniform power-error bound encloses the
infinite-series integral. There is no numerical quadrature or unbounded
series truncation in the four-term generator.
The 100-digit calculation uses 445 bits (112 extra working bits) and N=235.
The bound and all divisors are built with exact Sage integers/rationals.
Each output is rejected unless its ball is finite and retains at least
numberdb.bits(digits)+24 accurate bits. The attached measured evidence records
actual radii and minimum accuracy. Computation at 140 requested digits checks
all 24 enclosures again. The 100-digit written intervals are explicitly tested
to contain these higher-precision enclosures.
Independent checks use mpmath at 75 and 125 decimal working digits. The n=3
integral uses the log-sine form on [pi/3,pi], and the n=4 integral evaluates
the Clausen formula directly through polylogarithms. These computations share
neither the polynomial series nor Arb's integration routine with the generator.
They are numerical agreement checks, not the rigorous error-bound argument.
The checks run known integral controls before trusting the quadrature, and
compare five low-order formulas from BS Examples 3.1 and 3.4. Those formulas
involve pi, zeta(3), Clausen values and Li_4(1/2); they also connect to existing
NumberDB tables. Positivity, the log(2) upper bound between successive moments,
and strict log-convexity are checked across every applicable stored order.