back to table · edit · history · where entries came from · files · download
3148 bytes, as of the version from 2026-10-28 01:34 (current). Recorded here, not run.
# Independent checks for T567
The generator uses the Debye recurrence, DLMF 10.41.9. The full-polynomial
checker instead starts from DLMF 10.32.9,
K_nu(nu z) = (1/2) integral over R of exp(nu*(-z*cosh(t)+t)) dt, z > 0.
This full-line form follows by splitting cosh(nu*t) in the cited half-line
integral and reflecting the negative exponential. The phase has its unique
maximum at t0 = asinh(1/z), where z*cosh(t0) = sqrt(1+z^2) = 1/p and
z*sinh(t0)=1. Its value is -eta with the DLMF 10.41.7 convention. Write
h=nu^(-1/2), a=sqrt(p), and t=t0+a*v*h. The phase after removal of its
maximum and Gaussian factor exp(-v^2/2) is
sum over j>=1 of e_j(a,v)*h^j,
e_j = -v^(j+2)*a^j/(j+2)! when j is even,
e_j = -v^(j+2)*a^(j+2)/(j+2)! when j is odd.
The coefficients E_n of exp(sum e_j h^j) are obtained by differentiating
that formal exponential: E_0=1 and n*E_n=sum(j*e_j*E_(n-j),j=1..n).
The checker implements this finite convolution in QQ[a,v], without calling
power-series exp, numerical quadrature, or the Debye recurrence.
Normalized Gaussian integration replaces v^(2m) by (2m-1)!! and odd powers
by zero. All odd h coefficients vanish. The even coefficients contain only
even powers of a; replacing a^(2r) by p^r gives the K-series coefficient,
which is (-1)^k U_k(p) at h^(2k). The Jacobian supplies sqrt(pi*p/(2*nu)),
exactly the prefactor in DLMF 10.41.4. Thus this procedure checks every
coefficient of every stored polynomial, not just a finite set of values.
Controls run before comparison: Gaussian moments 0 through 6 are
1,0,1,0,3,0,15; the leading coefficient polynomial is 1; the first correction
has the DLMF sign and normalization. A deliberately changed coefficient of
U_12 must fail the independent equality check.
Additional checks use U_1,U_2,U_3 printed in DLMF 10.41.10 and an external
family: the reciprocal scaled-Gamma (Stirling) expansion. Taking the small-z
limit of the uniform I-series gives U_k(1) as its coefficients. Equivalently,
in the formal variable h,
sum U_k(1) h^k = exp(-sum B_(2m)*h^(2m-1)/(2m*(2m-1))),
using the logarithmic Gamma expansion DLMF 5.11.1 and the scaled-Gamma
normalization 5.11.3. The checker computes Bernoulli numbers independently
from their binomial recurrence, checks B1=-1/2, B2=1/6 and B4=-1/30, and then
forms the exponential coefficientwise. The first reciprocal coefficients
1,-1/12,1/288,139/51840 are controls. This verifies all thirteen endpoints.
It also tests the defining recurrence for all twelve stored transitions,
degree 3k, parity U_k(-p)=(-1)^k U_k(p), lowest exponent k, and the exact
origin values. Those structural checks supplement the integral comparison.
They do not substitute for it. The same validation function is applied to
polynomials parsed from the authenticated website document after filling.
Sources read:
- https://dlmf.nist.gov/10.41#ii , equations 3,4,7,8,9,10.
- https://dlmf.nist.gov/10.32#E9 , Bessel K integral.
- https://dlmf.nist.gov/5.11#E1 and #E3 , logarithmic Gamma and scaled Gamma.
This is exact symbolic arithmetic. No decimal precision or asymptotic
truncation-error guarantee is inferred from storing twelve corrections.