The Lonely Runner value and one-deletion statement

The formal definition OneDeletionDefs.lonelyValue is the supremum over all real times of the infimum of the nearest-integer distance among the retained speeds.

The fixed claim quantifies over N ≥ 2 and 1 ≤ r ≤ N; it requires the lower bound 1/N and characterizes equality by r = N or N = 2.