back to table · edit · history · where entries came from · files · download
2895 bytes, as of the version from 2026-11-09 23:44 (current). Recorded here, not run.
# Certified series for T699
Instruction provenance: `skill-manifest.json`, archived from
`agents/runs/20261109T231810Z-build-skills/manifest.json`; both skill hashes are
886390324dd1971e381a43cf3b46b822ab0bc67d62f31d8481e29ec79556746b.
Put a=pi*t, 0<t<=1/2, u=v/a, and w=u^2. Euler's sine and cosine products
(DLMF 4.22.1 and 4.22.2) give
log(2 sin(v/2)) = log(u) + log(a) - A(w),
log(2 cos(v/2)) = log(2) - B(w),
A(w) = sum_{j>=1} zeta(2j) (t/2)^(2j) w^j / j,
B(w) = sum_{j>=1} (4^j-1) zeta(2j) (t/2)^(2j) w^j / j.
All coefficients of A and B are positive. These series converge absolutely
at w=2 because (t/2)^2<=1/16 and t^2<=1/4. Since zeta(2j)<2,
A(2) <= -2 log(7/8) = Astar,
B(2) <= -2 log(1/2) = Bstar.
For p=m-1 and q=n-1, expand the integrand in powers log(u)^i. Its coefficient
series is binom(p,i) (log(a)-A(w))^(p-i) (log(2)-B(w))^q.
The sum of absolute coefficients weighted by 2^j is bounded by
binom(p,i) (abs(log(a))+Astar)^(p-i) (log(2)+Bstar)^q.
Truncating each polynomial product after degree N keeps exactly the first
N+1 Taylor coefficients; truncation at intermediate products cannot affect
those coefficients because all powers of w are nonnegative. For 0<=w<=1,
the entire omitted tail of the coefficient series is bounded by its weighted
absolute sum times 2^(-N-1). The endpoint log powers are integrable and
integral_0^1 u^(2j) log(u)^i du = (-1)^i i!/(2j+1)^(i+1).
Thus the absolute error of the negative integral is at most
a 2^(-N-1) (log(2)+Bstar)^q
* sum_{i=0}^p binom(p,i) i! (abs(log(a))+Astar)^(p-i).
This intentionally generous bound includes the full tail, including all
cross-products of omitted terms. It also justifies termwise integration
in the presence of the logarithmic singularity at zero.
The generator uses Sage RealBallField (Arb) for pi, logarithms, zeta values,
coefficients, polynomial products and all finite sums. Rational t is exact
before conversion to a ball, so argument rounding is included. It adds the
upward-rounded bound to the result radius. At 100 requested digits it uses
525 working bits and N=557; a runtime guard requires at least 415 accuracy
bits. The measured minimum is recorded in numerical-evidence.json.
For t=1, split at pi/2 and reflect the second integral: the result is the
sum of the (m,n) and (n,m) midpoint integrals. For 1/2<t<1, subtract the
(n,m) integral to pi*(1-t) from that complete integral. These exact identities
preserve enclosures under ball arithmetic. They avoid direct expansion at
the cosine singularity and cover the selected t=5/6 application case.
The 100-digit decimal is accepted only if its implicit interval of one unit
in the last place contains the complete output ball. Higher-precision
recomputation and independent quadrature and beta coefficients check the
implementation; they are not the basis of the certified error claim.