back to table · edit · history · where entries came from · files · download
2699 bytes, as of the version from 2026-10-26 21:52 (current). Recorded here, not run.
# Independent resolvent check for T529
Let H_s(t;x,y) be the heat kernel of (1/2)d²/dx² - s x_+ and let
G_s(x) = integral_0^infinity exp(-t/2) H_s(t;x,0) dt.
Feynman–Kac and conditioning on the endpoint give
G_s(0) = integral_0^infinity exp(-t/2) E[exp(-s t^(3/2) A)] / sqrt(2 pi t) dt.
This is the framework in Janson, arXiv:0704.2289v3, Appendix C.2,
equations (364)–(371), applied directly without using the moment recurrences.
The expansion coefficients G_s = sum_n (-s)^n g_n satisfy
(1/2)(1-d²/dx²)g_0 = delta_0,
(1/2)(1-d²/dx²)g_n = x_+ g_(n-1), n >= 1.
The decaying zeroth Green function is g_0(x)=exp(-|x|), so g_0(0)=1.
For x>0 put g_n(x)=exp(-x)p_n(x), with p_0=1. For x<0 the
solution is c_n exp(x). Continuity of the function and, for n>=1,
of its first derivative gives c_n=p_n(0) and p_n'(0)=2p_n(0).
Consequently
2p_n' - p_n'' = 2x p_(n-1).
Write f=x p_(n-1). The unique polynomial q=p_n' solves q-q'/2=f,
so q=sum_(j>=0) f^(j)/2^j (a finite sum). Integrating q and setting
p_n(0)=q(0)/2 gives p_n exactly over Q. The checker instead solves
these polynomial coefficients from the highest degree downward, and
checks the differential equation and boundary condition as polynomial
identities at every order. Decay and the jump/continuity conditions
select the unique Green function coefficients.
Extracting the coefficient at the origin yields
M_n = p_n(0) sqrt(pi) n! / (2^(3n/2) Gamma((3n+1)/2)).
The independent checker evaluates this expression directly with 768-bit
Arb Gamma values. It does not use the generator's moment prefactor or
its K_n or P_n recurrences. As a further exact comparison, p_n(0)/2^n
must equal P_n. The controls run first: p_0(0)=1 and M_0=1;
p_1(x)=x²/2+x/2+1/4, hence p_1(0)=1/4.
Separately, b(t) is normal with variance t(1-t), so
E[b(t)_+]=sqrt(t(1-t)/(2 pi)). Integrating the beta integral gives
M_1 = Beta(3/2,3/2)/sqrt(2 pi) = sqrt(pi/2)/8.
A third coefficient calculation uses the formal quotient in Janson (242):
P(z)=a(z)/h(z), where a_k=(6k)!/(576^k(3k)!(2k)!) and
h_k=a_k/(1-6k). Formal division uses only factorial coefficients and rational
arithmetic, independently of the nonlinear K recurrence. These series are
used formally; no convergence of the asymptotic series is assumed.
The stored decimal spelling denotes an interval of one final-place unit on
either side of its center. The checker parses center and unit as exact
rationals, then proves containment of both the generation ball and the
independent 768-bit ball within that interval. Finiteness and relative
accuracy checks prevent vacuous overlap. Exact even moments are compared as
rationals; the precision target concerns the six nonrational odd moments.