back to table · edit · history · where entries came from · files · download
3216 bytes, as of the version from 2026-10-28 19:40 (current). Recorded here, not run.
# Root counting and independent series bounds for T588
Let s = exp(pi i/4), G(x) = K_0(s x) = u(x)+i v(x). All arguments x are
strictly positive and K is principal. The ODE (DLMF 10.61.3) is
G'' + G'/x - i G = 0. Thus for W = u v' - v u',
(x W)' = x |G|^2. The exponential decay of G and G' on this ray
(DLMF 10.67.1, 10.67.2, 10.67.5, 10.67.6) gives x W -> 0 at infinity.
Consequently
x W(x) = -integral_x^infinity t |G(t)|^2 dt < 0.
Strictness follows because G is a nontrivial analytic solution. In particular
G cannot vanish at any positive x, since that would give W(x)=0. Its
continuous phase has derivative W/|G|^2 < 0. A zero of u therefore occurs
at a phase congruent to pi/2 modulo pi and is simple: at u=0, v is nonzero
and W=-v u' is nonzero.
## Excluding the origin interval
Set t=x^2/4, L=-log(x/2)-gamma. From DLMF 10.65.2 and 10.65.5,
G = (L-i pi/4) sum_{k>=0} (i t)^k/(k!)^2
+ sum_{k>=1} H_k (i t)^k/(k!)^2.
Here H_k=sum_{j=1}^k 1/j and H_0=0.
For 0<x<=1/4, t<=1/64 and L>=log(8)-gamma>0.
Put A=t/(1-t), B=t/(1-t)^2. By k!>=1 and H_k<=k,
|sum (i t)^k/(k!)^2 - 1| <= A and
|sum H_k (i t)^k/(k!)^2| <= B.
It follows that u >= L(1-A) - pi A/4 - B. This is bounded below by
(log(8)-gamma)(1-A0) - pi A0/4 - B0 at t0=1/64.
The code checks that explicit lower bound is positive in ball arithmetic.
There is no ker zero in (0,1/4].
## At most one zero per certified scan cell
DLMF 10.29.3 gives G'(x)=-s K_1(s x). The integral DLMF 10.32.9 gives
|K_1(s x)| <= K_1(x/sqrt(2)), a positive decreasing function of x.
For a cell [a,b] with midpoint m and half-width h,
|G(x)-G(m)| <= h K_1(a/sqrt(2)).
If this radius is less than |G(m)|, the image lies in an open disk excluding
zero. Its continuous phase lies in a wedge of angular width strictly less
than pi. Combined with strict phase monotonicity, there is at most one zero
of u in the cell. Opposite nonzero endpoint signs give exactly one; equal
nonzero signs give none. This proves the ordinal labels, not only existence.
All consecutive cells starting at 1/4 are certified, and counting stops only
after the cell containing the requested last root. An unsuccessful cell is
subdivided. Narrow root brackets remain inside their counted cells.
## Independent endpoint computation
checks.py implements the real and imaginary parts of the two series directly,
without calling Bessel or Kelvin functions. After terms k=0,...,N, put
A_next = t^(N+1)/((N+1)!)^2 and r=t/(N+2)^2 < 1. Later term ratios are at
most r, so the plain tail is bounded by A_next/(1-r). Also
H_(N+1+j) <= H_(N+1)+j/(N+2), so the harmonic tail is bounded by
A_next [ H_(N+1)/(1-r) + r/((N+2)(1-r)^2) ].
The error bound for either component of G is at most the plain bound times
(|L|+pi/4), plus the harmonic bound. Outward ball arithmetic accounts for
rounding and cancellation. These bounds are used at both endpoints of the
interval denoted by each stored decimal. A displaced interval must fail the
sign-change test. The certificate does not infer a root from a small residual.
The archived skill manifest is
agents/runs/20261028T190129Z-build-skills/manifest.json;
local and live SHA-256 both equal
e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.