math.PR — Probability

Lower bounds for the Beardwood–Halton–Hammersley constant

Contributed by Tejasvi Singh Tomar

Let $\beta$ be the Beardwood–Halton–Hammersley constant: the shortest tour through $n$ independent uniform random points in the unit square has length asymptotic to $\beta\sqrt n$ almost surely. Dong and Cao proved $\beta\ge0.6421$ from an inequality $\beta\ge5/8+\sum_{k=3}^{K}C_k$, where $C_k$ is an integral over configurations of $k$ points in the plane that form a connected graph when points at distance at most $1$ are joined. For $C_3$, $C_4$ and $C_5$, sharper bounds come from a first-order expansion of the area of the union of the unit disks on boxes of configurations. For $C_6+\dots+C_{22}$, which Dong and Cao did not use, a lower bound comes from comparing each point only with the three points before it in the order of their first coordinates. We obtain $\beta\ge0.6496$, and $\beta\ge0.6508$ if the exponential function of the C library used to evaluate the bound for $C_6+\dots+C_{22}$ has a relative error below $10^{-9}$. The proofs are computer-assisted; the bound $0.6496$ is proved in Lean 4, with finite checks evaluated by compiled code, from the inequality of Dong and Cao and two statements about unions of disks that we prove but do not formalize.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23716094