# Root location and index certificate for T589

Let c=exp(pi i/4), F(x)=I_0(cx)=u(x)+iv(x), with u=ber_0 and v=bei_0.
DLMF 10.61.1 gives the convention and 10.61.3 gives
F'' + F'/x - i F = 0. The Bessel derivative gives F'=c I_1(cx).

Define W=uv'-vu'. Direct differentiation gives
(xW)'=x(u^2+v^2). The origin series has F(0)=1, v(x)=x^2/4+O(x^6),
so xW tends to zero at the origin. Hence
xW(x)=integral_0^x t|F(t)|^2 dt > 0 for x>0.
If F vanished at a positive point then W would vanish there, a contradiction.
Consequently F never vanishes and its continuous phase theta, starting at zero,
satisfies theta'=W/|F|^2>0. Zeros of u are simple and occur at
successive phases (n-1/2)pi. This is also consistent with DLMF 10.71.8.

For 0<=x<=1, the entire series F=sum_k (i x^2/4)^k/(k!)^2 gives
|F-1| <= exp(1/4)-1 < 1. Thus u>0 there and no initial root is skipped.

On any [a,a+h] with a>=1, write Y=(F,F'). Its differential system has
matrix [[0,1],[i,-1/x]], whose induced infinity norm is at most M=1+1/a.
Gronwall's inequality implies ||Y(t)||_infinity <= N exp(Mh), where
N=|F(a)|+|F'(a)| is a convenient upper bound for ||Y(a)||_infinity.
Integration of F' therefore gives

    |F(t)/F(a)-1| <= h N exp(Mh)/|F(a)| = B.

The generator encloses B using Arb and requires B<1 on every consecutive
cell of width h=1/8, beginning at a=1. This proves that F(t)/F(a) stays
in the right half-plane; its continuous argument changes by less than pi/2.
Combined with strict phase monotonicity, a cell contains at most one zero
of u. Certified endpoint signs then prove exactly one zero when they differ,
and none when they agree. All endpoints have strictly certified signs.
The scan stops only when it has certified the twentieth sign-changing cell.
The number of cells and each cell's bound and signs are in checks-evidence.json.
This scan is a proof of ordinal indexing, not an assumption about grid spacing.

For each numbered cell mpmath supplies a candidate, used only for speed.
A rational interval of radius 10^(-digits-12) about that candidate must lie
strictly inside its counted cell and must have strictly opposite Arb signs.
Only then is it returned as a nonzero-width interval to the NumberDB writer.
The candidate's own accuracy is never a premise of the certificate.

Independent real-series check: let

    t_m = (-1)^m x^(4m)/(16^m ((2m)!)^2),  ber_0(x)=sum_m t_m.

After t_m the absolute term ratio is
q_m=x^4/[16 ((2m+1)(2m+2))^2]. These ratios decrease with m.
Once q_m<1, the absolute remainder is bounded by
|t_m| q_m/(1-q_m). The checker sums in ball arithmetic and adds this
explicit bound as an error. It evaluates the endpoints of every WRITTEN
100-significant-digit interval, proving opposite signs independently of
Arb's Bessel implementation. It also rejects an interval shifted by ten units
of the last written place. F(0)=1 and the first five printed roots on
Abramowitz-Stegun p. 381 are separate known-answer controls.

The I_0/J_0 identity and I_1/J_1 derivative identity are checked at all
root midpoints. The real series is also compared there, and all balls must
be finite with small absolute or relative radii. These consistency checks
supplement, rather than replace, the index and sign certificates.

Policy evidence: ../20261028T195045Z-build-skills/manifest.json.
Both archived instruction SHA-256 values are
 e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.
The separate critique actor must assess this argument independently.