back to table · edit · history · where entries came from · files · download
3706 bytes, as of the version from 2026-11-11 07:57 (current). Recorded here, not run.
# Certified series method and independent checks
Policy: ../20261111T011141Z-build-skills/manifest.json; matching archived bundle d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab. This is build evidence, not the independent scientific verdict.
DLMF 4.36.1 gives sinh(z)/z = product_(j>=1)(1+z^2/(pi*j)^2). Expanding its logarithm, absolutely for |t|<2*pi, gives
B(t)=log(2sinh(t/2)/t)=sum_(j>=1) (-1)^(j+1) zeta(2j) (t/(2*pi))^(2j)/j.
The defining kernel is A(t)=log(t)+B(t). All three exact endpoints satisfy 0<x<2 and q=(x/(2*pi))^2<1/10 (checked as ball inequalities). For t=x*y, 0<=y<=1, let B_N be the first N terms and D(y^2)=log(x)+B_N(x*y).
Since 1<zeta(2j)<2,
|B(x*y)-B_N(x*y)| <= epsilon = 2*q^(N+1)/((N+1)*(1-q)).
Also |B| and |B_N| <= 2*q/(1-q)<1. With p=n-1-k and C=|log(x)|+1, the difference of pth powers is bounded by
p*epsilon*(C-log(y))^(p-1).
Integration against x^(k+1)*y^k therefore bounds the total error by
E=p*epsilon*x^(k+1)*sum_(h=0)^(p-1) binomial(p-1,h)*C^(p-1-h)*h!/(k+1)^(h+1).
This follows from factorizing a^p-b^p, not from a guessed precision margin. For p=0 the truncation error is zero.
The finite expression is integrated without quadrature: expand (log(y)+D(y^2))^p and use integral_0^1 y^(k+2j)*log(y)^h dy = (-1)^h*h!/(k+2j+1)^(h+1). Every coefficient and operation uses RealBallField, with exact Python integer combinatorics and division performed by Sage balls; no binary float enters any value. All polynomial powers are retained in full. Reconstructing x by radicals and logarithms in the same field propagates endpoint uncertainty. Add E using RealBall.add_error, which takes the upper magnitude of its ball argument. The error and rounding are thus included before the client encodes 100 significant digits.
At requested digits d, the implementation uses N=d+50 and bits(d+80) working bits. Each result must be finite and have more than bits(d+10) relative accuracy. Actual minimum accuracy, native return types, exact rational lower/upper bounds and timings are recorded in offline.log and offline-rows.json. The shared dry_run.py invokes check.py on all 98 values; its output is retained, including suspicious-decimal and size checks.
Independent method in checks.py: mpmath tanh-sinh quadrature after t=x*exp(-s), so the lower logarithmic singularity becomes an exponentially decaying integral on s>=0. It evaluates the original sinh/log kernel directly, without zeta coefficients, polynomial arithmetic, or the generator's tail argument. Endpoints are reconstructed separately using mpmath. This is a high-precision numerical check, not another certified enclosure. A second precision is used for selected difficult cases. Check all 98 stored intervals after upload, including both signs, maximal logarithmic degree, high k, and the endpoint beyond the kernel's sign change. Reject nonfinite/wide intervals and deliberately corrupted inputs. Known nonzero controls are the zero-logarithm integral and Lsh_3^(1)(2a)=zeta(3)/5.
Additional independent formulas: Lsh_2^(0)(x)=pi^2/6-Li_2(exp(-x))-x^2/4, obtained by differentiating Li_2(exp(-x)); at x=2a this is pi^2/10 using the dilogarithm identity in BS Example 11. For s>=3, at A(2a)=0 the inverse-binomial integral transform gives Lsh_s^(1)(2a)=(s-2)!*F_s(-1)/(-2)^(s-2). The checker sums F_s(-1) directly using exact integer binomial coefficients, independently of stored T698 values. Differentiating F_s(u) gives F_(s-1)(u)/u, and F_2(-4*sinh(x/2)^2)=-x^2/2; repeated integration in log(-u) establishes the transform, including signs and factorials. Numerical checks over the finite selection do not prove this universal identity; the derivation supplies the reason it is stated.