back to table · edit · history · where entries came from · files · download
2814 bytes, as of the version from 2026-10-26 20:13 (current). Recorded here, not run.
# Independent killed-motion check for T526
This check uses the Feynman–Kac boundary-value problem, not the K/Q recurrence
that generates the entries. The source framework is Janson (2007), Appendix C.3,
equations (372), (380)–(383), and the standard Brownian generator (1/2) d²/dx².
For Brownian motion started at x>0 and killed at its first zero τ, put
u_n(x) = ∫_0^∞ e^(-t) E_x[(∫_0^t B(s) ds)^n; τ>t] dt.
Differentiating the Feynman–Kac resolvent in the area coupling gives
(1 - (1/2) d²/dx²) u_n = n x u_(n-1),
u_n(0)=0, u_0(x)=1-exp(-sqrt(2)x).
The solution has polynomial growth; this excludes the growing homogeneous
exponential. Set y=sqrt(2)x and u_n(x)=n! 2^(-n/2) v_n(y). Then
(1-D²)v_n = y v_(n-1), v_0=1-exp(-y).
Write v_n=P_n+exp(-y)R_n, where P_n and R_n are rational polynomials. The two
polynomial equations are
P_n-P_n'' = y P_(n-1),
2 R_n'-R_n'' = y R_(n-1),
R_n(0)=-P_n(0).
These have finite derivative-sum solutions:
P_n = Σ_(j>=0) D^(2j)(y P_(n-1)),
R_n' = Σ_(j>=0) D^j(y R_(n-1))/2^(j+1).
The code integrates R_n' coefficient by coefficient and fixes its constant
from the boundary condition. It then checks both polynomial equations exactly
at every order before using v_n'(0)=P_n'(0)+R_n'(0)-R_n(0).
The survival probability satisfies P_x(τ>t)/x → sqrt(2/(pi t)); the conditioned
path tends to a duration-t meander, whose area is t^(3/2) A_me. Hence
u_n'(0) = sqrt(2/pi) Γ((3n+1)/2) M_n,
M_n = sqrt(pi) 2^(-n/2) n! v_n'(0)/Γ((3n+1)/2).
The positive-time moment bounds and Laplace damping justify the finite moment
derivatives of the resolvent. This is also the moment consequence of Janson's
equation (383). The numerical check evaluates Γ directly in Arb at 768 bits,
independently of the generator's parity simplification. Polynomial slopes are
compared exactly with the generator's Q_n for every n=0,...,12.
Controls precede comparisons: v_0'(0)=1 and the resulting M_0=1; v_1'(0)=3/4;
Janson Table 4 gives M_1=(3/4)sqrt(pi/2), M_2=59/60,
M_3=(465/512)sqrt(pi/2), and M_4=5345/3696. The fractional interval parser
is checked on 1.25 and 12e2, whose uncertainty is one final written unit.
All twelve written values, including values fetched back from the database,
are checked against this independent result. Decimal intervals must fully
contain the high-precision independent ball, not merely overlap it. Even rows
must equal the independently reconstructed rational. The Q recurrence is also
checked on the recovered stored intervals, and strict moment log-convexity
M_n² < M_(n-1) M_(n+1) is checked for n=1,...,11 with M_0=1.
Instructions: agents/runs/20261026T200330Z-build-skills/manifest.json;
both recorded hashes are
b4d51ded0d52cfe3dcc0859de0845c3879b0c2363273ba7e809a7e06ded40b18.