Lonely Runner: Fourteen of Twenty

Abstract

A reflected finite certificate supplies a rational lonely time for every fourteen speeds chosen from one through twenty.

Theorem 1.1 (Rational torus distance is an exact residue window).

$\forall s, a, d \in N, 0 < d \Rightarrow \frac{1}{15} \leq torusDist (s \cdot \frac{a}{d}) ⟺ d \leq 15 \cdot (s \cdot a mod d) \land 15 \cdot (s \cdot a mod d) \leq 14 \cdot d .$

Proof. Machine-checked in Lean as D5/S1/Phase/LonelyRunnerFourteenOfTwenty.torusDist_nat_ratio_ge_iff_nat_residue_window (✓ std3). ∎

Source. Repository-derived.

Commentary.

For natural s, a, and positive d, Mathlib’s fractional-part division identity rewrites the torus distance at time a/d as the residue of sa modulo d divided by d. Clearing the positive denominator gives the two natural-number window inequalities exactly.

This equivalence is the arithmetic bridge used by every reflected mask computation below; it is not a restatement of the final existence claim.

Theorem 1.2 (Fifteen masks cover every fourteen-speed selection).

$safeMask (\frac{1}{11}) = s p ee d U ni v erse ∖ {11} \land safeMask (\frac{1}{12}) = s p ee d U ni v erse ∖ {12} \land safeMask (\frac{1}{13}) = s p ee d U ni v erse ∖ {13} \land safeMask (\frac{1}{14}) = s p ee d U ni v erse ∖ {14} \land safeMask (\frac{1}{15}) = s p ee d U ni v erse ∖ {15} \land safeMask (\frac{1}{22}) = s p ee d U ni v erse ∖ {1} \land safeMask (\frac{11}{23}) = s p ee d U ni v erse ∖ {2} \land safeMask (\frac{6}{25}) = s p ee d U ni v erse ∖ {4} \land safeMask (\frac{8}{25}) = s p ee d U ni v erse ∖ {3} \land safeMask (\frac{5}{26}) = s p ee d U ni v erse ∖ {5} \land safeMask (\frac{4}{29}) = s p ee d U ni v erse ∖ {7} \land safeMask (\frac{5}{29}) = s p ee d U ni v erse ∖ {6} \land safeMask (\frac{11}{29}) = s p ee d U ni v erse ∖ {8} \land safeMask (\frac{1}{9}) = s p ee d U ni v erse ∖ {9, 18} \land safeMask (\frac{1}{10}) = s p ee d U ni v erse ∖ {10, 20} \land powersetCard (6, res i d u a lSp ee d s) \subseteq res i d u a lC o v ere d S i x S u b se t s \land \forall S : Finset (N), (S \subseteq s p ee d U ni v erse \land ∣ S ∣ = 14) \Rightarrow \exists (t, M) \in cer t i f i c a t e, S \subseteq M .$

Proof. Machine-checked in Lean as D5/S1/Phase/LonelyRunnerFourteenOfTwenty.certificate_package (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first fifteen conjuncts are the exact safe masks at the listed rational times. Each equality is checked by kernel reduction after transport through the residue-window theorem.

The next conjunct exhausts the seven six-element subsets of the residual seven-speed set. The last conjunct lifts those computations by a complement argument to every fourteen-element subset of the full twenty-speed universe.

Theorem 1.3 (Every fourteen of the twenty speeds have a rational lonely time).

$\forall S : Finset (N), (S \subseteq s p ee d U ni v erse \land ∣ S ∣ = 14) \Rightarrow \exists t \in Q, 0 \leq t \leq 1, \forall s \in S, \frac{1}{15} \leq torusDist (s \cdot t) .$

Proof. Machine-checked in Lean as D5/S1/Phase/LonelyRunnerFourteenOfTwenty.lonely_runner_fourteen_of_twenty (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every fourteen-element subset S of speeds one through twenty, the finite certificate supplies a rational time in the unit interval whose exact safe mask contains S. Membership in that mask gives torus distance at least 1/15 for every selected speed.

The theorem covers all 38,760 such subsets through the structured complement proof; it does not rely on the impractical direct powerset reduction and does not assert the unrestricted Lonely Runner conjecture.

References

Truth anchor: D5/S1/Phase/LonelyRunnerFourteenOfTwenty.certificate_package
Truth anchor: D5/S1/Phase/LonelyRunnerFourteenOfTwenty.lonely_runner_fourteen_of_twenty
Truth anchor: D5/S1/Phase/LonelyRunnerFourteenOfTwenty.torusDist_nat_ratio_ge_iff_nat_residue_window

Keyboard shortcuts

trureturing Blueprint

Lonely Runner: Fourteen of Twenty

Abstract

References