back to table · edit · history · where entries came from · files · download
5513 bytes, as of the version from 2026-10-26 20:49 (current). Recorded here, not run.
# Independent checks for T527
## Definitions and conventions
Janson, arXiv:0704.2289v3, section 23, equations (215)–(216) defines the nonnegative process B(t)-min B(u), with the minimum over the full unit interval. Its integral A has the same law as max B(t)-integral B(t)dt by pathwise sign symmetry (equation (217)). This is the F-Airy law of Majumdar–Comtet, arXiv:cond-mat/0409566, section IV and equations (73)–(75). The covariance min(s,t) specifies variance rate one and the Brownian generator (1/2)d²/dx². There is no endpoint conditioning.
## Generator
The generator evaluates Janson's exact rational recurrences (7) and (199) for K and Q. It forms W_n=sum Q_j Q_(n-j), equation (232), and the moments 2^(-n/2)n! W_n / Gamma((3n+2)/2), equation (229). If n=2m the rational multiplier is (2m)! W_(2m)/(2^m (3m)!). If n=2m+1, put j=3m+2; the multiplier of sqrt(2/pi) is (2m+1)! 4^j j! W_(2m+1)/(2^(m+1)(2j)!). Exact rationality of the even orders follows from this expression, not from their printed digits.
## Independent polynomial resolvent
Consider the half-line Dirichlet resolvent v(x,u) solving
v''(x,u) - (1+u x)v(x,u) = -1, v(0,u)=0,
with the solution bounded at infinity for u>=0. This is the killed Brownian Feynman–Kac resolvent after scaling, as in Janson Appendix C.3. The decaying homogeneous solution is Ai(u^(1/3)x+u^(-2/3)). The derivative at the origin of the Green-function integral is
v'(0,u) = u^(-1/3) AI(u^(-2/3))/Ai(u^(-2/3)).
Janson (195) identifies its formal coefficients as (-1)^n Q_n. This use of an asymptotic series extracts finitely many coefficients; it does not assert convergence of the infinite series.
Write v=sum v_n u^n. Then v_0=1-exp(-x), and
(d²/dx²-1)v_n = x v_(n-1), v_n(0)=0.
Write v_n=P_n(x)+exp(-x)R_n(x), with P_n and R_n polynomials. Starting with P_0=1, R_0=-1, the finite polynomial inverses are
P_n = -sum_(k>=0) D^(2k)(x P_(n-1)),
R_n' = -sum_(k>=0) D^k(x R_(n-1))/2^(k+1),
R_n(0) = -P_n(0).
Each sum terminates. The check verifies both differential equations coefficient by coefficient and the boundary condition at every order. It then obtains Q_n=(-1)^n(P_n'(0)+R_n'(0)-R_n(0)). This computation uses neither the K recurrence nor the generator's Q recurrence. Controls are Q_0=1, Q_1=3/4, and Q_2=59/32, checked before comparison.
## Independent factorial-series quotient
A further exact calculation uses alpha_n=(6n)!/(576^n (3n)!(2n)!), beta_0=1, and beta_n=alpha_n+(6n-3)beta_(n-1)/4. Coefficient-by-coefficient division of beta(z) by alpha(z) gives Q(z), from Janson (104), (106), (184), (196). All orders 0..12 are compared exactly using the campaign's agrees_with check.
## Probability and numeric controls
The reflection principle implies that -min B has the law of the absolute value of a standard normal variable. Since the Brownian integral has mean zero, E[A]=sqrt(2/pi). This is a direct probabilistic check outside the recurrence family. Majumdar–Comtet (74) supplies moments 0..3; Janson Table 5 supplies order 4 as well. The exact rational factors agree with all of these values.
Conditioning on the global minimum time tau yields two independent meanders, with tau following Beta(1/2,1/2). Integrating their scaled areas gives the beta-weighted convolution in Janson (233) and Majumdar–Comtet (73). The checks compute this using the resolvent coefficients and direct Arb Gamma functions at 768 bits for orders 0..12. This also verifies that tau is integrated rather than sampled.
The generator's half-integer simplification is compared with direct Arb Gamma evaluation at 768 bits for every stored order. Both endpoints of every written decimal's interval (one last-place unit on either side) are constructed exactly; the independent enclosure must lie strictly inside. Exact rational entries must be enclosed by the independent Gamma computation and equal their exact simplified factors. All compared balls must be finite and have at least 700 relative-accuracy bits. Strict moment log-convexity is checked for orders 1..11, with M_0=1 as control.
After filling, checks.py --stored reads the database through the authenticated public API, compares all twelve records, tests their actual written enclosures, reconstructs W_n from each database value and checks the coefficient convolution, and repeats strict log-convexity. The site's Django-only stored() helper cannot run on this isolated builder; the API is the authoritative readback.
## Source correction
Janson v3 equation (230) prints (AI/Ai')². The double Laplace transform (221) and the asymptotic quotient (231) require (AI/Ai)². The former printed quotient starts at x^(-2), while the stated right side starts at x^(-1). The generator uses the consistent equations (229), (231), (232); the independent resolvent also gives AI/Ai. No ambiguity in the definition remains.
## Instruction and dependency evidence
The archived instruction manifest is agents/runs/20261026T204019Z-build-skills/manifest.json. Both archived versions, the current local canonical skill, and the live /skill have SHA-256 b4d51ded0d52cfe3dcc0859de0845c3879b0c2363273ba7e809a7e06ded40b18. See skill-read-evidence.json. Numerical results and Sage version are recorded in numerical-evidence.json. The source-selection dependencies are generate.py and argument-selection.md; checks.py, check.py and this derivation are attached for reproduction and independent critique. No independent-critique acceptance is asserted by this build.