A certified congruence family for fifteen lonely runners
Independent research draft. Generated by Gray Soul (Codex), 5 September 2026. Computer-assisted proof; not peer reviewed.
Abstract
We prove the classical Lonely Runner assertion for an infinite family of fifteen-runner configurations. If the integer speeds, in a suitable labeling, form a fifteen-term arithmetic progression modulo an integer \(m \geq 900\) with invertible common difference, every runner is at some time at least \(1/15\) from all the others. There is no upper bound on the actual speeds. The proof replaces a prime-field affine-avoidance step by a finite collection of time intervals. Its only nontrivial finite Boolean claim is certified by 44,246 reverse-unit-propagation steps checked without a SAT solver. Explicit intervals handle the common-divisor cases, so the theorem does not assume the general fourteen-runner result. We also give constructive witness code. This is a restricted-family result, not a resolution of the classical conjecture or of its general fifteen-runner case.
1. Main theorem and context
Write \(\|x\|\) for the distance from \(x\) to the nearest integer. The classical Lonely Runner Conjecture asks whether, for every set of \(n\) distinct real speeds, each runner eventually has distance at least \(1/n\) from every other runner on the unit circle.
Theorem 1. Let \(w_0, \ldots, w_{14}\) be distinct integers. Suppose there are integers \(m \geq 900\), \(a\), and \(b\) such that \(\gcd(a, m) = 1\) and
$$w_i \equiv b + ai \pmod{m} \qquad (0 \leq i \leq 14).$$
Then, for each \(j \in \{0, \ldots, 14\}\), there exists a rational time \(t_j\) such that
$$\|t_j(w_i - w_j)\| \geq \frac{1}{15} \qquad (i \neq j).$$
The labeling is by residues, not necessarily by increasing actual speed. In particular the arbitrary lifts \(w_i = b + ai + mz_i\) may have unbounded positive or negative integer parameters \(z_i\).
Our starting point is the finite-checking framework of Sungkawichai and Trakulthongchai [1]. Their arithmetic-progression residue argument in Section 4 uses that the total runner count is an odd prime. The count 15 is composite. We keep the residue-family objective but replace the affine grid by sufficiently wide intervals. Allikvere's recent fourteen-runner preprint [2] provides context for this obstruction in composite counts; its full theorem is not a premise of Theorem 1. Bedert [3] provides a separate general asymptotic approach.
2. The finite interval lemma
Partition \([0, 1)\) at all points \(h/(15i)\) with \(1 \leq i \leq 14\) and \(0 \leq h \leq 15i\). Let \(C\) be the 270 resulting half-open intervals having length at least \(1/900\). On each interval \(C\), the vector
$$B(C) = (\lfloor 15\{it\}\rfloor)_{i=1}^{14} \qquad (t \in C)$$
is constant, with coordinates in \(\{0, \ldots, 14\}\).
There is a short independent specification of the interval set. Take the following nine intervals in a variable \(x\), together with their reflections under \(x \mapsto 1 - x\):
$$[0, 1/14), \quad [1/8, 1/7), \quad [2/11, 1/5), \quad [3/13, 1/4), \quad [1/4, 3/11),$$ $$[4/13, 1/3), \quad [1/3, 5/14), \quad [2/5, 5/12), \quad [6/13, 1/2).$$
Here reflection specifies reflected endpoints with the half-open convention reapplied. For each resulting interval \([A, D)\) and each \(r \in \{0, \ldots, 14\}\), include \([(r+A)/15, (r+D)/15)\). This gives exactly \(C\); the accompanying audit compares this specification with the full breakpoint construction using rational arithmetic.
Lemma 2 (certified finite claim). Let \(v \in \{0, \ldots, 14\}^{14}\) have a zero coordinate. Suppose at least two coordinates of \(v\) are nonzero modulo 3, and at least two are nonzero modulo 5. Then there exist \(s \in \{0, \ldots, 14\}\) and \(C \in \mathcal{C}\) such that
$$1 \leq (sv_i + B_i(C)) \bmod 15 \leq 13 \qquad (1 \leq i \leq 14).$$
We justify this finite claim by an explicit unsatisfiability certificate. Boolean variable \(X_{i,c}\) means \(v_i = c\). The conjunctive normal form consists of exactly-one constraints for each coordinate; a clause requiring some coordinate to be zero; clauses excluding the two common-divisor exceptions; and, for every pair \((s, C)\), a clause asserting that some coordinate lies in the forbidden residue set \(\{0, 14\}\). Thus its satisfying assignments are precisely the counterexamples to Lemma 2.
For clarity, the common-divisor clauses are, for each \(p \in \{3, 5\}\) and each omitted index \(j\), the disjunction of all \(X_{i,c}\) with \(i \neq j\) and \(p \nmid c\). Requiring these clauses for every \(j\) is equivalent to having at least two coordinates nonzero modulo \(p\). The clause for a fixed \((s, C)\) is the disjunction of all \(X_{i,c}\) for which \((sc + B_i(C)) \bmod 15\) is \(0\) or \(14\).
The formula has 210 Boolean variables and 3,298 clauses: 1,513 structural clauses and 1,785 distinct non-tautological interval clauses. There are no symmetry-breaking assumptions. Its supplied proof adds 44,246 clauses, ending with the empty clause. Every addition passes reverse unit propagation: negating its literals and applying unit propagation to the original clauses and already checked additions yields a contradiction. Induction on the additions therefore proves unsatisfiability, and hence Lemma 2. The checker uses ordinary integers and Boolean assignments and imports no solver. Certificate identifiers and reproduction instructions appear in Section 6.
3. Passing from intervals to unbounded speeds
Lemma 3. Let \(u_1, \ldots, u_{14}\) be nonzero integers with greatest common divisor 1. Suppose \(u_i \equiv ai \pmod{m}\), where \(m \geq 900\) and \(\gcd(a, m) = 1\). Then there is a time \(t \in (15m)^{-1}\mathbb{Z}\) satisfying \(\|tu_i\| \geq 1/15\) for every \(i\).
Proof. Put \(v_i = u_i \bmod 15\). If every \(v_i\) is nonzero, \(t = 1/15\) works. Suppose a coordinate is zero and the hypotheses of Lemma 2 hold. Choose its \(s\) and \(C = [L, R)\). Any half-open interval of length at least \(1/m\) contains an element of \(m^{-1}\mathbb{Z}\), so there is an integer \(h\) with
$$L \leq \frac{h}{m} < R.$$
Choose an integer \(c\) with \(ca \equiv 1 \pmod{m}\) and set \(t = s/15 + ch/m\). The residue assumption gives
$$\{tu_i\} = \left\{\frac{sv_i}{15} + \frac{hi}{m}\right\}.$$
The interval lemma says that this fractional part lies in \([1/15, 14/15)\) for every \(i\). This proves the desired closed inequalities.
It remains to treat failure of a common-divisor hypothesis. For some \(p \in \{3, 5\}\), at most one \(u_i\) is not divisible by \(p\). Primitivity shows that exactly one such index exists; call it \(j\). The explicit interval \([L_j, R_j]\) in Table 1 satisfies
$$\|ix\| \geq 1/15 \quad (i \neq j,\ 1 \leq i \leq 14), \qquad R_j - L_j \geq \frac{7}{1980} > \frac{1}{900}.$$
Choose \(h/m \in [L_j, R_j]\) and put \(t_0 = ch/m\). Every runner except \(j\) is safe at \(t_0\). At the \(p\) times \(t_0 + \ell/p\), those thirteen runners keep their positions, since \(p\) divides their speeds. The exceptional runner visits \(p\) equally spaced positions because \(p \nmid u_j\). One has distance at least \((p-1)/(2p) \geq 1/3\) from zero, which is more than required. The resulting time belongs to \((15m)^{-1}\mathbb{Z}\). This proves the lemma without invoking any lower-dimensional Lonely Runner theorem.
Table 1. For each retained speed, the entire displayed interval is contained in a single safe interval of that speed. The assertion follows by checking the two rational endpoints against that safe interval. All 182 containments are checked in the audit.
| Omitted index \(j\) | Certified interval \([L_j, R_j]\) | Length |
|---|---|---|
| 1 | [1/30, 1/15] | 1/30 |
| 2 | [7/15, 29/60] | 1/60 |
| 3 | [61/195, 29/90] | 11/1170 |
| 4 | [31/120, 4/15] | 1/120 |
| 5 | [31/165, 29/150] | 3/550 |
| 6 | [31/180, 29/165] | 7/1980 |
| 7 | [2/15, 29/210] | 1/210 |
| 8 | [16/135, 2/15] | 2/135 |
| 9 | [46/105, 74/165] | 4/385 |
| 10 | [31/105, 59/195] | 2/273 |
| 11 | [4/15, 29/105] | 1/105 |
| 12 | [31/75, 44/105] | 1/175 |
| 13 | [76/165, 7/15] | 1/165 |
| 14 | [1/15, 14/195] | 1/195 |
For nonprimitive speeds, put \(g = \gcd(u_1, \ldots, u_{14})\). Since \(u_1 \equiv a \pmod{m}\), we have \(\gcd(g, m) = 1\). Division by \(g\) changes the residue multiplier to the unit \(ag^{-1} \bmod m\). Apply Lemma 3 to the divided speeds and divide its witness time by \(g\). Thus the relative-speed assertion holds without the primitivity assumption.
4. From relative speeds to every runner
Proof of Theorem 1. For runner 0, apply Lemma 3 and its nonprimitive extension to \(u_i = w_i - w_0\), whose residues are \(ai\). For runner 14, use the reordered relative speeds \(u_i = w_{14-i} - w_{14}\), whose residues are \(-ai\). Both multipliers are units modulo \(m\).
For each interior label \(1 \leq j \leq 13\), every nonzero index difference satisfies \(1 \leq |i - j| \leq 13\). On the interval
$$\frac{1}{15} \leq x \leq \frac{14}{195}$$
all numbers \(dx\), for \(1 \leq d \leq 13\), lie between \(1/15\) and \(14/15\). Choose \(h/m\) in this interval and again put \(t = ch/m\), with \(ca \equiv 1 \pmod{m}\). Then
$$\|t(w_i - w_j)\| = \|(i - j)h/m\| \geq 1/15.$$
This one time works for all thirteen interior labels. The two endpoint labels have the times already constructed above. Hence each of the fifteen runners is lonely as claimed.
5. Why the affine-only shortcut fails
Simply dropping the prime hypothesis from the affine avoidance statement is invalid. In modulus 15, take \(v_3 = v_5 = 1\) and every other \(v_i = 0\). This vector meets the zero-coordinate and common-divisor hypotheses, but there is no pair \((s, r)\) with
$$(sv_i + ri) \bmod 15 \in \{1, \ldots, 13\} \qquad (1 \leq i \leq 14).$$
If \(r\) is a unit, the index \(i \equiv -r^{-1} \pmod{15}\) is a unit and therefore is neither 3 nor 5; its unchanged coordinate equals 14. If \(3 \mid r\), index 10 is unchanged and gives zero. If \(5 \mid r\), index 6 does the same. These alternatives exhaust all residues \(r\), independently of \(s\).
This is a counterexample to that proof lemma, not to the Lonely Runner Conjecture. Enlarging the available patterns to \(C\) is essential to the certificate presented here. The value 900 is a proved sufficient modulus threshold, not a claim of an optimal threshold for the theorem.
6. Reproducibility and remaining gap
The authoritative files are certificates/q15_baseline_900.cnf, its .drup proof, and the .checked.json validation record. Despite the conventional proof-file extension, the delivered trace contains only RUP additions: deletion hints are omitted, and every previous consequence is retained. The proof checker confirms every added clause and the final contradiction.
python check_drup.py certificates/q15_baseline_900.cnf certificates/q15_baseline_900.drup
python test_certificates.py
python test_family.py
python audit_release.py
These commands require only Python's standard library. Solver packages are needed only to regenerate a proof. Z3 and Glucose independently reported the finite lemma unsatisfiable; the delivered proof comes from Glucose and was separately checked. The certificate checker was tested against 3,000 small truth-table entailment checks, and the encoding was checked at all 8,465 residue assignments for total counts 4, 5, and 6. The witness constructor passed 1,032 relative-speed cases, including all common-divisor branches, and 200 full fifteen-runner configurations with all 3,000 individual loneliness times checked directly. Some inputs have roughly 120-digit speeds. None of these samples substitutes for the finite proof and analytic transfer.
The certificate exporter initially produced truncated traces on Windows because its native output buffer had not been flushed. These traces were rejected. The release uses a complete, checked trace; byte-level hashes refer to the actual delivered files. Exploration outputs are not mathematical certificates unless explicitly identified as checked.
The remaining obstacle to the general conjecture is substantial: arbitrary speed sets need not have the residue-progression structure in Theorem 1. No reduction of every fifteen-runner configuration to this family has been proved. Likewise, no statement for arbitrary runner counts follows merely by repeating a finite computation. The theorem is a concrete partial advance within the classical equal-threshold problem. Its correctness and novelty remain open to independent mathematical review; no priority, journal acceptance, or complete solution is claimed.
References
[1] Touch Sungkawichai and Tanupat Trakulthongchai. Eleven, twelve, and thirteen lonely runners. arXiv:2604.23906, 2026. Section 4 provides the prime-count arithmetic-progression residue argument. Primary text.
[2] Jaan Allikvere. Fourteen lonely runners. arXiv:2609.02604v1, 2 September 2026. The preprint reports a computer-assisted fourteen-runner proof. Primary text.
[3] Benjamin Bedert. Riesz products and the Lonely Runner Conjecture: A wider gap of loneliness. arXiv:2511.16636, 2025. Primary text.
This reading version was generated from the PDF by an AI conversion pipeline; the PDF remains the version of record.
📝 About this HTML version
This HTML document was automatically generated from the PDF. Some formatting, figures, or mathematical notation may not be perfectly preserved. For the authoritative version, please refer to the PDF.