Papers With

← All papers
First page of A new unconditional lower bound for shoreline search

A new unconditional lower bound for shoreline search

Alexander Temerev

math.MG Aug 18, 2026 · v1 math.OC
formalization geometry
Read PDF arXiv abstract
TL;DR
A Lean/Mathlib repository verifies key algebraic lemmas (crossing lemma, one-Lipschitz reduction, sum-splitting and prepayment inequalities) supporting the lower-bound proof.
Abstract
A unit-speed searcher starts at the origin of the Euclidean plane and must hit an unknown straight line whose direction and distance from the origin are both unknown. We prove that every deterministic search path has competitive ratio at least $C_{\log}\approx 12.5937096701246675$. The bound is unconditional: the path need not be cyclic, self-similar, spiral-like, or monotone in angle. For each projection direction, we compare the path with a zigzag obtained by sorting its alternating record turns. The resulting completion constraints are interpreted as jobs with scale-dependent deadlines and lower-bounded through a finite-window scheduling argument in logarithmic time. Averaging these directional bounds then uses the exact Euclidean velocity budget. In one dimension, the same method recovers the optimal cow-path constant $9$. Finally, Arb ball arithmetic provides a rigorous numerical enclosure of the constant.
Problem

In shoreline search a unit-speed searcher must reach an unknown straight line of unknown direction and distance, minimizing the competitive ratio between hitting time and distance. The best unconditional lower bound was Isbell's 6.3972, with 12.5385 known only under cyclic restrictions.

Approach

For each projection direction the path is compared with a zigzag obtained by sorting its alternating record turns. These completion constraints are interpreted as jobs with scale-dependent deadlines and lower-bounded via a finite-window logarithmic-time scheduling lemma. Directional bounds are averaged using the exact Euclidean velocity budget identity. Arb ball arithmetic certifies the resulting constant, and Lean/Mathlib files check the exact crossing lemma, the one-Lipschitz projection reduction, the sum-splitting inequality, the deadline factor bound, and the logarithmic prepayment inequality.

Results

Every deterministic search path has competitive ratio at least C_log ≈ 12.5937096701246675, an unconditional bound requiring no cyclicity or ordering assumption. The same method recovers the optimal cow-path constant 9 in one dimension, and Arb certifies 12.59370967012466 < C_log < 12.59370967012468.