back to table · edit · history · where entries came from · files · download
2944 bytes, as of the version from 2026-10-28 18:59 (current). Recorded here, not run.
# Root-counting and enclosure certificate for T587
Set a = exp(i pi/4), G(x) = K_0(a x) = u(x) + i v(x). All branches are
principal, x > 0. DLMF 10.61.3 gives G'' + G'/x - i G = 0. Thus for
W = u v' - v u', (x W)' = x (u^2 + v^2). The exponential decay of G and G'
(DLMF 10.67.1, 10.67.2, 10.67.5, 10.67.6) gives x W -> 0 at infinity, so
x W(x) = - integral_x^infinity t |G(t)|^2 dt < 0.
The integral is strictly positive since G is a nontrivial analytic solution.
In particular G never vanishes on the positive ray, and its continuous phase
has strictly negative derivative W/|G|^2. Consecutive zeros of v differ in
phase by pi. Every zero of v is simple: v=0 implies u != 0 and u v'=W<0.
There are no zeros in (0, 1/4]. To see this directly, put t=x^2/4 and use
DLMF 10.65.2 and 10.65.5 in the equivalent harmonic-number expansion
G = -(log(x/2) + gamma + i pi/4) I
+ sum_{k>=1} H_k (i t)^k/(k!)^2,
I = sum_{k>=0} (i t)^k/(k!)^2.
Here H_k = sum_{j=1}^k 1/j. For 0<x<=1/4, t<=1/64, H_k<=k,
|I-1|<=t/(1-t), and the harmonic sum is at most t/(1-t)^2 in modulus.
The function x^2 log(2/x) is increasing on this range. Since log(8)<3,
0<gamma<1, and 3/4<pi/4<1, these bounds give
|v + pi/4| <= 5/63 + 64/3969 < 3/4 < pi/4.
Hence v is strictly negative on that interval. This also fixes the count's
starting point without a numerical assumption about the limiting phase.
For every subsequent mesh cell [l,r] of width 1/4, the code checks
h K_1(l/sqrt(2)) < |G(m)|, m=(l+r)/2, h=(r-l)/2.
DLMF 10.32.9, differentiated under its absolutely convergent integral, gives
|G'(x)| <= K_1(x/sqrt(2)) <= K_1(l/sqrt(2)) on the whole cell. Therefore
|G(x)-G(m)| <= h K_1(l/sqrt(2)). The cell image lies in a disk excluding the
origin, and its phase spans strictly less than pi. Combined with strict phase
monotonicity, each cell contains at most one zero of v. Certified endpoint
signs now give a complete count: opposite signs imply exactly one simple
zero, equal signs imply none. No mesh endpoint is accepted with uncertain or
zero sign. Scanning stops only after counting the requested number of roots.
Newton steps locate candidates inside the counted cells; no accuracy claim
rests on Newton convergence. Each result is an explicit rational bracket
whose endpoints have opposite signs under complex-ball Bessel K evaluation,
and whose endpoints stay inside the counted cell. The returned RealBall
contains that bracket. The separately implemented checks.py evaluates the
real logarithmic/harmonic series with a rigorous absolute tail bound at both
ends of the final 100-significant-digit decimal interval. It also checks the
stored numbers read from the website after filling.
The arithmetic guard and tail bounds, controls, widths, and per-root outcomes
are recorded in numerical evidence. There is no numerical integration in this
certificate. The analytic identities, not a sampled plot, provide monotonicity.