# Verification report for the exact area excursion height bound

The manuscript proves a uniform maximum bound for a Brownian excursion of
duration T conditioned on the exact area rho T, with fixed rho>0. For
large T and H>=1, the tail is at most C_rho T^(3/2) exp(-c_rho H). Every
fixed positive moment of the maximum is O((log T)^r).

The proof uses the weakly continuous exact-area law of Zambotti, the
classical scalar area asymptotic of Janson, a positivity-preserving
Gaussian regression shift, and elementary Dirichlet-kernel and
Brownian-reflection estimates. The endpoint estimate is justified at
positive bridge endpoints before taking the excursion limit. No unproved
process-level equivalence of ensembles or intrinsic ultracontractivity
bound is used.

The symbolic checker verifies 15 algebraic identities, including the area
variance, shift, density ratio, saddle cancellation, leading prefactor,
and exit-time ODE. A further exact-rational test checks 471 time partitions.
Three Airy normalization quadratures and nine area-density calculations
provide numerical consistency checks only. They are not certified
enclosures or substitutes for the analytic proof. All checks passed in
the existing research Python environment on 5 October 2026.

The frozen dataset record AIM-PROBABILITY-0093 corresponds to the archived
official AIM item 2.18, not its extracted number 22.18. For its literal
duration 2N and area N, the theorem implies uniform degeneration after
division by N^(1/3), hence no nondegenerate random limit on an N^(2/3)
window. This does not resolve variants with a different area exponent,
moving wall or multiple curves, or identify a constant-scale process limit.

Agranov et al.'s prior one-point Ferrari--Spohn picture is credited.
The bounded literature search does not establish priority. The checks
and proof audit were performed in the originating AI-assisted research
workflow; independent peer review and formal proof verification are not
claimed. The paper is an unrefereed preprint.