# Certification of T487

The stored value is the kth positive zero of

\[
F_\nu(x;\lambda)=J_\nu(x)Y_\nu(\lambda x)-Y_\nu(x)J_\nu(\lambda x),
\qquad \nu\geq0,\quad\lambda>1.
\]

The table uses integer orders 0 through 5, the exact radius ratios 5/4, 3/2,
2, 5/2, 3, 4, 5 and 10, and positive indices 1 through 10. These are the
plain cross-product roots, not roots of derivative or mixed cross-products.
The inner radius is 1; no domain has been rescaled to unit area. At a general
inner radius a, the radial wavenumber is kappa/a and the Laplacian eigenvalue
is kappa squared/a squared.

## Root enclosures

SciPy scans supply candidates only. Each candidate is recomputed using
mpmath at 130 and 160 decimal digits. Agreement is required to 120 decimal
places relative to max(1,abs(root)). All subsequent decisions use exact
rational arithmetic or Arb balls.

The high-precision approximation is truncated to a multiple of 10^-112.
The two endpoints are that exact rational centre plus or minus 10^-110.
Arb evaluates F at each endpoint at 717 bits and certifies strictly opposite
signs. Continuity guarantees a zero between them. This conclusion does not
assume the mpmath accuracy or the quality of the SciPy scan.

The generator returns a ball enclosing those rational endpoints. The minimum
measured relative accuracy is 363 bits, exceeding 109 decimal digits.
Serialization retains 100 significant digits. The independent checks test
both exact endpoints of each resulting written decimal interval at 896 bits,
so the rounded text is checked as well as the narrower internal enclosure.

The 384-bit working guard was chosen after a precision probe. At order 0,
ratio 5/4 and index 10, a 461-bit evaluation had radius about 1.93e-70,
whereas the endpoint value is about -1.13e-113. At 640 bits its radius fell
to about 2.70e-124; the production computation uses 717 bits. This is a loss
of approximately 70 decimal digits in complex Arb Bessel evaluation at these
arguments. No bound was inferred from agreement of floating-point digits.

## Certification of the indices

For fixed positive rational X, put

\[
u(r)=\sqrt r\,[J_\nu(X)Y_\nu(rX)-Y_\nu(X)J_\nu(rX)].
\]

This solution satisfies

\[
-u''+\frac{\nu^2-1/4}{r^2}u=X^2u,\quad u(1)=0,\quad u'(1)=2/\pi>0.
\]

If two consecutive zeros are distance d apart, integration by parts and the
Dirichlet Poincare inequality give

\[
\frac{\pi^2}{d^2}\int u^2\leq\int (u')^2
=\int\left(X^2-\frac{\nu^2-1/4}{r^2}\right)u^2
\leq(X^2+1/4)\int u^2.
\]

Thus d >= pi/sqrt(X^2+1/4). Choose a rational mesh h such that
h^2*(X^2+1/4)<9<pi^2. Each mesh interval contains at most one zero. The first
sample is positive, from the initial derivative and the separation bound.
All remaining sample signs are certified with Arb; their changes count every
interior zero, including the interval ending at the outer boundary. X is
chosen as the last root bracket's upper endpoint, where F is nonzero.

Theorem 5.18 in Teschl, *Ordinary Differential Equations and Dynamical Systems*,
identifies this count with the number of Dirichlet eigenvalues below X^2.
All these eigenvalues are positive, since in the original radial equation

\[
\mu\int_1^\lambda rR^2\,dr
=\int_1^\lambda \left(r(R')^2+\frac{\nu^2}{r}R^2\right)\,dr>0
\]

for a nonzero function with zero endpoint values. Ten disjoint positive
sign brackets and a total count of ten therefore leave exactly one root in
each bracket and none omitted before or between them. This proves the
indices, without relying on a numerical scan to count zeros.

The independent checks use a different, finer rational mesh. The known
half-integer case with ratio 2 has roots k*pi: node counts at X=3,4,7 must
be 0,1,2, respectively. These controls run before any production counts.

## Independent numerical check

`checks.py` does not import the generator. For every written entry it solves

\[
\theta'=x-\frac{\nu^2-1/4}{xr^2}\sin^2\theta,\qquad\theta(1)=0,
\]

with SciPy DOP853 and checks theta(lambda)=k*pi. This is the Pruefer phase
of the transformed radial differential equation and uses no Bessel function
values. It is a numerical cross-check, separate from the rigorous certificate.
The free equation at nu=1/2 returns the known nonzero phase pi for x=pi and
ratio 2; perturbing x by one percent must fail the eigenvalue condition.

Every entry also satisfies the variational bounds in the document. The first
root of order 0 and ratio 2, when squared, agrees with the independent annulus
eigenvalue in T390. The half-integer Bessel determinant is additionally
compared with its elementary sine expression for all eight radius ratios.

Sources:
- https://dlmf.nist.gov/10.21.x, equation 10.21.48 and simplicity of its zeros.
- https://dlmf.nist.gov/10.5.E2, the Bessel Wronskian.
- https://dlmf.nist.gov/10.16.E1, elementary half-integer formulas.
- https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf, Chapter 5,
  particularly Theorem 5.18.