arXiv:2608.13599v1
Abstract
For a set V of n-1 distinct positive integers write LR(V) = max_t min_{v in V} ||v t||, where ||x|| is the distance from x to the nearest integer; V is tight if LR(V) = 1/n, the value predicted by the Lonely Runner Conjecture. Goddyn and Wong (Integers 6 (2006), #A38) classified the tight sets obtained from the baseline [n-1] by replacing one speed r with a multiple mr, and proved that for a fixed r only finitely many non-multiple replacements can be tight, remarking that this "partially explains" why the two sporadic tight sets {1,3,4,7} and {1,3,4,5,9}, in which the speed 2 is replaced by an odd number, have no analogues. We make their finiteness effective and settle the case they singled out. Let U(n,r) be the region left uncovered when speed r is deleted from the baseline. We compute the length of every connected component of U(n,r) exactly, in both regimes 2r > n-1 and 2r <= n-1, in terms of an arithmetic quantity I(n,r). Since a connected set on which the inserted speed w must stay 1/n-close to the integers cannot be longer than 2/(wn), this yields the explicit necessary bound w <= 4rI/(2s-I) with s = n-r, and hence: if ([n-1] minus {r}) union {w} is tight with 2r <= n-1, then n <= 6r. This improves the constant implicit in Goddyn and Wong's finiteness theorem from 12 to 6 and makes the classification of single-speed modifications a finite computation for each n. Carrying the computation out for r = 2 we obtain the complete classification: ([n-1] minus {2}) union {w} with w > n-1 is tight if and only if (n,w) = (5,7) or (6,9); the same method disposes of r = 3 entirely. We also report exhaustive censuses in exact rational arithmetic, and note that the natural guess that tight sets have all speeds below 2n is false, a counterexample being the Goddyn-Wong set {1,...,29,31,90} with n = 32.
AI-generated audit
Audit summary
Not a correctness certificate. A “Correct” result may include yellow typos or minor formal corrections that do not affect substantive soundness. It means this audit found no unresolved substantive error under the stated criteria; it does not replace expert scrutiny or formal verification.
Current report
Detailed mathematical audit
01Statements4 reported findingsContains unsupported statements
The component-length formula, effective bound, complete classifications for deleted speeds and , the one-speed census, the bounded-window census, and the explicit tight counterexample are correct. The two-speed census in Theorem 1.8(ii) is not able to be verified because its released exhaustive-search implementation omits all cases in which speed is deleted.
Exact component lengths and the effective replacement bound
Pages 3 and 5–6 · Theorems 1.4 and 1.6 · arXiv:2608.13599v1
Dirichlet's lemma confines every component of to a -neighborhood of a reduced fraction . The runner supplies the inner puncture exactly when , while the largest legal representatives in the residue classes supply the two outer walls. All other runner constraints are weaker. This yields the two displayed component-length formulas. Covering a longest component with the inserted speed gives , and together with gives .
The deleted-speed and classifications
Pages 3 and 6–7 · Theorem 1.7 · arXiv:2608.13599v1
For , the exact value of reduces the effective bound to five possible values of and finitely many ; exact breakpoint evaluation leaves only and . For , the same formula reduces to with an explicit finite range for , and exact evaluation finds no tight set. The range follows from the verified divisibility classification of Goddyn and Wong.
The released search does not cover replacements that delete speed
Page 4 · Theorem 1.8(ii); computational proof in Section 4 and the archived file twoswap_hunt.py · arXiv:2608.13599v1
The theorem quantifies over all distinct and claims that, for and , the only tight two-speed modification is . The released driver enumerates deleted pairs with combinations(range(2,n),2), so it never tests any pair . Neither the manuscript nor another released search supplies a general argument excluding those omitted cases throughout the theorem's range. No counterexample was found, but the full quantified census is not established by the supplied computation. A repair requires enumerating the missing branch with the same exact certification, or proving an independent exclusion theorem for it.
Archived verification repository, twoswap_hunt.py ↗The remaining exact censuses and the speed- example
Pages 4 and 7–8 · Theorem 1.8(i), (iii), (iv), Proposition 1.9, and Section 4 · arXiv:2608.13599v1
The one-speed driver covers every deleted speed and every inserted in the stated box. The window driver enumerates every primitive -subset of in the stated range. Survivors of the proved-safe floating-point filter are evaluated exactly at the complete breakpoint set. The independently implemented wall-subdivision and branch-and-bound checks agree with the component formulas and certify every listed tight set, including at .
02Proofs4 reported findingsContains incorrect or incomplete proofs
The analytic proofs and the exact-certification method are correct. The computational proof of Theorem 1.8(ii) is incomplete because a quantified family of deleted-speed pairs is absent from the enumeration.
Wall analysis for
Pages 5–6 · Equations (4)–(7) and proof of Theorem 1.4 · arXiv:2608.13599v1
Fractions with non-coprime numerator are excluded by a surviving divisor of . For a reduced fraction, multiples of yield exactly the inner wall when present. Among nonmultiples, the constraints with residue distance one are binding, and inequality (7) shows every residue-distance-at-least-two constraint is weaker. The proof also blocks the remaining portion of each Dirichlet interval, so no unlisted components occur.
Every candidate maximum is checked exactly and the pre-filter is safe
Pages 4 and 7–8 · Lemmas 2.2 and 4.1; Section 4.3 · arXiv:2608.13599v1
The minimum of finitely many sawtooth functions can attain a positive maximum only at a peak of an active function or at a crossing of two active functions, giving the complete rational breakpoint set. Exact rational evaluation at that set determines . Lemma 4.1 bounds the floating-point error far below the discard margin, and every survivor is recomputed exactly. An independent wall-subdivision implementation matched all tested component sets and formulas, while adaptive branch-and-bound independently certified the listed tight sets.
One deletion branch is absent from the purported exhaustive search
Page 8 · Section 4.2 and Table 2; archived twoswap_hunt.py and reproduce_all.py · arXiv:2608.13599v1
Both released entry points loop over combinations(range(2,n),2). The proof obligation includes pairs with , because Theorem 1.8(ii) imposes no lower bound . The window census covers only a smaller parameter window and does not fill the omitted range , . Repair classification: no repair supplied for the full statement; extending the exact enumeration to combinations(range(1,n),2) is a plausible repair only until its output is produced and independently checked.
Archived verification repository ↗The divisibility classification is applied in its stated range
Pages 2–3 and 6 · Theorem 1.1, Proposition 1.3, and proof of Theorem 1.7 · arXiv:2608.13599v1
The cited theorem gives exactly the criterion for tight replacements . Proposition 1.3 correctly shows that a deleted speed with must divide an inserted speed: at , all surviving baseline speeds are farther than , while a nonzero value of is at least .
Goddyn–Wong, Tight instances of the lonely runner, Theorem 2.3 ↗03Novelty0 reported findingsNo non-novelty findings
No non-novelty findings.