import mpmath as mp
mp.mp.dps = 130
n = 1
seed = mp.sqrt(2) * (n - mp.mpf(1)/8) * mp.pi
root = mp.findroot(lambda x: mp.kei(0, x), (seed-mp.mpf('0.25'), seed+mp.mpf('0.25')))
print(mp.nstr(root, 100))
The attached generator uses Arb complex-ball evaluations of $K_0$ at 753 bits. Each root lies in a rational bracket of radius $10^{-108}$ with certified opposite endpoint signs; the returned ball contains that bracket, and the written decimal denotes uncertainty of one unit in its last place.
The ordinal indices are certified as well. An analytic series bound excludes roots in $(0,1/4]$. On each of 353 consecutive cells of width $1/4$ ending at $88.5$, a 384-bit calculation proves that the image of $G(x)=K_0(xe^{\pi i/4})$ lies in a disk excluding zero. The derivative bound $|G'(x)|\leq K_1(x/\sqrt2)$ follows from [4]. The disk condition and strict phase monotonicity give at most one zero per cell, so endpoint signs count exactly twenty. The largest certified disk-radius-to-center-modulus ratio is less than $0.513$. The attached root-counting.md supplies the proof.
An independent implementation of the real logarithmic and harmonic-number series [2], with explicit geometric tail bounds at 1024 bits, certifies opposite signs at both endpoints of every written 100-significant-digit interval. All endpoint balls are finite with radii below $10^{-200}$. Controls include the nonzero identity $K_{1/2}(1)=\sqrt{\pi/2}/e$, the origin series, and rejection of intervals displaced by ten last-place units. The first five roots agree with the printed values [6] within $10^{-5}$; this is a low-precision control, not the basis of the hundred-digit bounds. The Programs snippet illustrates numerical approximation; the attached generator supplies the certificates.