back to table · edit · history · where entries came from · files · download
3591 bytes, as of the version from 2026-10-28 20:48 (current). Recorded here, not run.
# Root location and index certificate for T590
Set c=exp(pi i/4), F(x)=I_0(cx)=u(x)+iv(x), u=ber_0, v=bei_0.
DLMF 10.61.1 and 10.61.3 give the normalization and
F''+F'/x-iF=0. The derivative is F'=c I_1(cx).
With W=uv'-vu', differentiation gives (xW)'=x|F|^2. The origin
series F(0)=1, v(x)=x^2/4+O(x^6) implies xW tends to zero.
Thus xW(x)=integral_0^x t|F(t)|^2 dt>0 for every x>0.
If F vanished at x>0, W would vanish there, a contradiction.
The continuous phase theta starts at zero and has theta'=W/|F|^2>0.
The positive zeros of v are simple and occur at theta=n*pi, n>=1.
The origin is a double zero of v and is excluded.
DLMF 10.71.8 also gives the integral underlying the Wronskian identity.
For 0<x<=1, write
v(x)=sum_m (-1)^m x^(4m+2)/(4*16^m*((2m+1)!)^2).
Successive absolute term ratios are
q_m=x^4/[16*((2m+2)*(2m+3))^2], decreasing with m.
On this interval q_0<=1/576, so the sum of all terms after x^2/4
has magnitude at most (x^2/4)/575. Therefore v(x)>0 throughout
(0,1], and no positive root precedes the certified scan.
On each [a,a+h], a>=1, Y=(F,F') satisfies a first-order linear
system with matrix [[0,1],[i,-1/x]]. Its induced infinity norm
is at most M=1+1/a. Set N=|F(a)|+|F'(a)|, which bounds ||Y(a)||.
Gronwall's inequality implies ||Y(t)||<=N exp(Mh). Integration gives
|F(t)/F(a)-1| <= h*N*exp(Mh)/|F(a)| = B.
Arb encloses B on every consecutive cell of width h=1/8. The generator
requires B<1. Therefore F(t)/F(a) stays in the right half-plane and its
continuous argument changes by less than pi/2. Since theta increases,
each cell contains at most one zero of v. Strict endpoint signs decide
whether it contains one or none. Every cell through the twentieth root is
checked; no claim about spacing is assumed. The count certificate is
adapted from the attached regular-Kelvin method on T589, with the component
and the proof on the initial interval changed for bei_0.
For each numbered cell, mpmath supplies only a candidate. A rational bracket
of radius 10^(-digits-12) must lie strictly inside the cell and have opposite
Arb signs of Im I_0(cx). The returned MPFI interval encloses those rational
endpoints with outward rounding. Its width must be nonzero. No accuracy
assumption about the candidate finder enters the certificate.
The independent checker sums the displayed real series at 900 bits. After
term t_m, once q_m<1, the absolute remainder is at most
|t_m| q_m/(1-q_m). It adds this error bound to the ball sum. This check uses
no Bessel-function evaluator. It checks opposite signs at the endpoints of
all written 100-digit intervals (decimal center plus or minus one unit in
the last place), and rejects all intervals displaced by ten such units.
Controls precede the root checks: v(0)=0 and
575/2304<v(1)<575/2304+1/14745600, from alternating terms at x=1.
The second is a nonzero control, so a function that returns zero cannot pass.
Other checks compare the I_0 and J_0 rotations, their first derivatives,
the differential equation, and W>0 at every midpoint. Independent mpmath
0F3 root computations at 160 and 210 decimal places provide agreement checks.
The first five roots are compared with the five-decimal values visually
read on Abramowitz-Stegun p. 381. The Programs snippet is executed for all
20 roots. These checks supplement the rigorous index and endpoint certificates.
Policy: ../20261028T202403Z-build-skills/manifest.json. Both archived skills
have SHA-256 e37efb7e2ededf6c1d7134c673f152f648f26e0267c556aebdf3ec65765d8b4c.
The build makes no independent critique decision; that is the next actor's task.