Covering hypercubic grids by polygonal trails: capacity bounds and the optimum for P(4,3)

The classical nine-dot puzzle asks for a polygonal trail through a square grid using as few segments as possible. We study its higher-dimensional analogue on P(n,k) := {0,…,n−1}^k for integers n,k ≥ 2, allowing arbitrary real vertices and unrestricted segment directions, and denote the minimum number of segments by h(n,k). For n ≥ 3 and k ≥ 2, we give a geometric proof of the previously stated capacity bound: a trail of r ≥ 1 segments meets at most 1+r(n−1) grid points. Refinements of this bound, combined with exhaustive finite checks, establish h(4,3)=23 and h(5,3) ≥ 32. We also exhibit a 22-segment trail through 63 points of P(4,3), the maximum possible, and a 23-segment covering trail contained in [0,4]^3, which settles the corresponding box-constrained problem. The general capacity theorem, a large-grid lower bound refuting a previously proposed formula for h(n,k), and the boxed construction are verified by the Lean 4 kernel, whereas the finite exclusions use native reflection and additionally trust the native compiler and runtime. A companion technical note provides the computational specification and reproducible proof artifacts. The companion technical note and reproducible proof artifacts are available at https://doi.org/10.5281/zenodo.24145830. The manuscript includes a declaration detailing the use of AI assistance.