back to table · edit · history · where entries came from · files · download
3319 bytes, as of the version from 2026-10-26 19:49 (current). Recorded here, not run.
# Independent resolvent check for T525
This check uses the Markov generator of reflected Brownian motion rather than the D/L recurrence in generate.py. Its source is the Feynman–Kac framework in Janson, Appendix C and C.1 (https://arxiv.org/abs/0704.2289). The polynomial solution described here is derived directly from that framework.
Write u_n(t,x) = E_x[(integral_0^t |B(s)| ds)^n]. On x >= 0, the moment equation is partial_t u_n = (1/2) partial_x^2 u_n + n x u_(n-1), with Neumann boundary partial_x u_n(t,0)=0, u_0=1, and u_n(0,x)=0 for n>0. Taking the time Laplace transform at rate 1 gives (1 - (1/2)partial_x^2)U_n=n x U_(n-1). The transform exists because the time dependence of each finite moment is polynomially bounded.
Put y=sqrt(2)x and g_n(y)=2^(n/2) U_n(y/sqrt(2))/n!. Then
(1 - d^2/dy^2)g_n = y g_(n-1),
g_n'(0)=0, g_0=1.
The solution of polynomial growth is unique: the difference of any two such solutions solves the homogeneous equation, has zero Neumann data, and cannot contain either a growing exponential or a nonzero multiple of exp(-y) with zero derivative at the origin.
Use g_n=P_n+exp(-y)Q_n with rational polynomials. Start P_0=1, Q_0=0. If F=yP_(n-1) and H=yQ_(n-1), set
P_n = sum_(k>=0) F^(2k),
V_n = sum_(k>=0) H^(k)/2^(k+1),
Q_n(y) = integral_0^y V_n(s) ds + P_n'(0) + V_n(0).
These are finite sums. They solve P_n-P_n''=F, 2Q_n'-Q_n''=H and P_n'(0)+Q_n'(0)-Q_n(0)=0 exactly. All three residuals are checked at every order. The controls are g_0=1 and g_1=y+exp(-y), which give g_0(0)=g_1(0)=1. The next origin value is 9/4.
Brownian scaling at x=0 gives U_n(0)=Gamma(3n/2+1) M_n, hence
M_n = n! g_n(0) / [2^(n/2) Gamma(3n/2+1)].
The checker evaluates this last expression with Arb Gamma at 768 bits, independently of the generator's half-integer simplification. It also verifies g_n(0)=L_n exactly for every n=0,...,12.
Two additional sources of controls are the Gaussian marginal identity E|B(t)|=sqrt(2t/pi), whose integral is (2/3)sqrt(2/pi), and Janson's Table 3, which gives M_2=3/8, M_3=(263/630)sqrt(2/pi), and M_4=903/2560. The checker also evaluates the second moment from the joint-normal absolute product formula: after s=t u and u=sin(theta)^2, M_2=(8/(3pi)) integral_0^(pi/2) [sin(theta)^2 cos(theta)^2 + theta sin(theta)^3 cos(theta)] dtheta. The two integrals are pi/16 and 5pi/64, respectively, giving 3/8. This analytic control has no recurrence coefficients.
The written decimal is an interval, with radius one unit in its last place. The independent 768-bit enclosure must lie strictly within that interval; overlap alone is insufficient. Controls deliberately shift a decimal by ten units in its last place and change an exact rational, and both must be rejected. Stored values are checked by the same interval test, transformed back to L_n for the recurrence residual, and tested for positive strict log-convexity with the zeroth moment 1. The duration formula follows from Brownian scaling, a process identity, rather than a numerical fit.
Instruction manifest: ../20261026T193829Z-build-skills/manifest.json (attached verbatim as skill-manifest.json). Both versions have SHA-256 b4d51ded0d52cfe3dcc0859de0845c3879b0c2363273ba7e809a7e06ded40b18. This build evidence does not replace the campaign's independent critique.