back to table · edit · history · where entries came from · files · download
4055 bytes, as of the version from 2026-10-26 22:20 (current). Recorded here, not run.
# Independent verification of the moments in T530
The generator uses Janson's rational K, Q, P=D^+, L^+ recurrences. The
following calculation starts from the Brownian generator instead. It applies
the Feynman–Kac framework in Janson (2007), Appendix C.1, directly to the
potential x_+. It uses no coefficients from generate.py.
Let E be an independent exponential time of rate 1/2. For Brownian motion
started at x, put V_n(x)=E_x[(integral_0^E B(t)_+ dt)^n]. The resolvent
moment equation is
(1 - d²/dx²) V_n(x) = 2 n x_+ V_{n-1}(x), V_0(x)=1.
This follows by differentiating the Feynman–Kac resolvent in the Laplace
parameter at zero; the exponential horizon supplies the factor 1/2.
For n>0 and x<0 the solution decaying at minus infinity is C_n exp(x).
On x>=0 it has the form
V_n(x) = P_n(x) + exp(-x) Q_n(x),
with polynomials P_n,Q_n. These polynomial names are local to this derivation
and are not the P_n,Q_n used for recurrence coefficients in the table.
Start with P_0=1 and Q_0=0. For H=2 n x P_{n-1} and J=2 n x Q_{n-1},
P_n = H + H'' + H'''' + ...,
Q_n' = J/2 + J'/4 + J''/8 + ...,
Q_n(0) = (P_n'(0) + Q_n'(0) - P_n(0))/2.
Both derivative sums terminate. The last equation matches the value and
first derivative at zero to C_n exp(x), giving C_n=P_n(0)+Q_n(0).
No exponentially increasing term is allowed at positive infinity because
moments grow only polynomially with the starting value. These conditions
uniquely determine the resolvent moments.
Controls run before accepting higher orders: V_0=1 and
V_1(x)=2x+exp(-x) on x>=0, V_1(x)=exp(x) on x<0. Thus C_0=C_1=1 and
C_2=17/2. Each polynomial is also substituted into its differential equation
and the matching conditions exactly over Q. Brownian scaling now gives
M_n = C_n / [2^(3n/2) Gamma(3n/2+1)].
checks.py evaluates this expression directly in 768-bit Arb. It also checks
the exact relation C_n=2^n n! L_n^+ through n=12. The independent calculation
therefore checks both the recurrence coefficients and the half-integer Gamma
simplification used by the generator.
A third calculation forms Janson's exact formal-series quotient (268):
alpha_n=(6n)!/[576^n (3n)! (2n)!], beta_0=1,
beta_n=alpha_n+3(2n-1)beta_{n-1}/4. The coefficient of z^n in
(sum (alpha_n+beta_n)z^n)/(sum 2 alpha_n z^n/(1-6n)) is L_n^+.
This is divided coefficient by coefficient over Q, without using K,Q,P.
The first four moments are compared with Janson's printed Table 8.
There are two checks outside the Airy and resolvent calculations. The Gaussian
marginal mean gives E[B(t)_+]=sqrt(t/(2pi)), so M_1=sqrt(2/pi)/3.
For s<=t, a centered bivariate normal calculation with rho=sqrt(s/t) gives
E[B(s)_+ B(t)_+] = sqrt(st)/(2pi)
* [sqrt(1-rho²) + rho (pi/2 + asin(rho))].
After s=t r² and integration over t, the second moment is
M_2 = 2/(3pi) integral_0^1
r² [sqrt(1-r²)+r(pi/2+asin(r))] dr = 17/96.
The two terms integrate to pi/16 and 13pi/64. The checker evaluates the
integral with r=sin(theta) at 85 decimal digits. Its nonzero quadrature control
is integral_0^(pi/2) sin²(theta)cos²(theta)dtheta=pi/16, checked first.
This quadrature is an agreement check; the stored precision is justified by
exact rational arithmetic and Arb, not by the quadrature.
All six written rational entries must equal the independent exact result.
For each odd entry, the entire finite 768-bit enclosure must lie strictly
inside the written interval (decimal +/- one last-place unit). The checker
also tests strict log-convexity M_(n-1) M_(n+1)>M_n² for 1<=n<=11,
including the control M_0=1. With --stored it reads the actual database
entries, repeats the containment tests, inverts the moment formula to test
L_n^+ against both coefficient computations, and retests log-convexity.
Instruction manifest: agents/runs/20261026T220819Z-build-skills/manifest.json.
The exact skill SHA-256 is recorded in numerical-evidence.json. This is build
evidence; independent critique and its argument-selection sidecar remain
separate controller stages.