From 9da277ce24355303384da261d465ee41200f0eb1 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 16 Jun 2026 23:01:00 -0500 Subject: [PATCH] feat: prove general lonely_k_speeds_1_to_k theorem for all k General theorem: for speeds [1,2,...,k] at t = 1/(k+1), the origin is uncovered. Proves the Lonely Runner Conjecture for the infinite family of consecutive integer speeds. Subsumes k=2 and k=3 lemmas. --- .../Semantics/Semantics/LonelyRunner.lean | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/LonelyRunner.lean b/0-Core-Formalism/lean/Semantics/Semantics/LonelyRunner.lean index d19e38d6..9c96ee35 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/LonelyRunner.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/LonelyRunner.lean @@ -308,4 +308,101 @@ def lonelyRunnerReceipt : String := #eval! lonelyRunnerReceipt +/-! ## 11. General theorem: speeds [1, 2, ..., k] -/ + +/-- Lemma: For integer speeds 1..k at time 1/(k+1), the origin is uncovered. + Runner i is at position i/(k+1) on S¹. + Distance from origin is min(i/(k+1), 1 - i/(k+1)) ≥ 1/(k+1). + Since coverage requires distance < 1/(k+1), the origin has Φ = 0. -/ +lemma origin_uncovered_at_one_over_k_plus_one (k : ℕ) (hk : k > 0) : (0 : ℝ) ∈ + scarRegion ((List.range k).map fun i : ℕ => Runner.mk (i+1 : ℝ)) (1 / ((k : ℝ) + 1)) := by + rw [scarRegion, Set.mem_setOf_eq] + have h_all_dist_ge : ∀ (i : ℕ), i < k → circleDist (0 : ℝ) ((i+1 : ℝ) / ((k : ℝ) + 1)) ≥ 1 / ((k : ℝ) + 1) := by + intro i hi + unfold circleDist + have hpos : (i+1 : ℝ) / ((k : ℝ) + 1) ≥ 0 := by positivity + have hi_val : (i+1 : ℝ) / ((k : ℝ) + 1) ≥ 1 / ((k : ℝ) + 1) := + div_le_div_of_nonneg_right + (by + have h_nat : (i+1 : ℕ) ≥ (1 : ℕ) := by omega + exact_mod_cast h_nat) + (by positivity : 0 ≤ (k : ℝ) + 1) + have hi_val2 : 1 - (i+1 : ℝ) / ((k : ℝ) + 1) ≥ 1 / ((k : ℝ) + 1) := by + have h_sum : ((i+1 : ℝ) / ((k : ℝ) + 1)) + (1 - (i+1 : ℝ) / ((k : ℝ) + 1)) = 1 := by ring + have h_upper : (i+1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast (show i+1 ≤ k from hi) + have h_numer : (k+1 : ℝ) - (i+1 : ℝ) ≥ 1 := by + have hi' : (i+1 : ℝ) ≤ (k : ℝ) := by + have h_succ : (i+1 : ℕ) ≤ k := Nat.succ_le_of_lt hi + exact_mod_cast h_succ + nlinarith + have h_eq : 1 - (i+1 : ℝ) / ((k : ℝ) + 1) = ((k : ℝ) + 1 - (i+1 : ℝ)) / ((k : ℝ) + 1) := by + field_simp [show (k : ℝ) + 1 ≠ 0 from by positivity] + calc + 1 - (i+1 : ℝ) / ((k : ℝ) + 1) = ((k : ℝ) + 1 - (i+1 : ℝ)) / ((k : ℝ) + 1) := h_eq + _ ≥ 1 / ((k : ℝ) + 1) := + div_le_div_of_nonneg_right h_numer (by positivity : 0 ≤ (k : ℝ) + 1) + have hmin : 1 / ((k : ℝ) + 1) ≤ min ((i+1 : ℝ) / ((k : ℝ) + 1)) (1 - (i+1 : ℝ) / ((k : ℝ) + 1)) := + le_min hi_val hi_val2 + simpa [sub_zero, abs_of_nonneg hpos] using hmin + unfold coverageDensity coverageRadius + have hlen : ((List.range k).map fun i : ℕ => Runner.mk (i+1 : ℝ)).length = k := by simp + rw [hlen] + -- Lemma: filter is empty because no runner satisfies the distance condition + have h_filter_empty : ((List.range k).map fun i : ℕ => Runner.mk (i+1 : ℝ)).filter + (fun r => circleDist (0 : ℝ) (runnerPos r (1 / ((k : ℝ) + 1))) < 1 / ((k : ℝ) + 1)) = [] := by + apply List.eq_nil_iff_forall_not_mem.mpr + intro r + intro hr + rcases (by simpa using hr) with ⟨hmem, hdist⟩ + rcases hmem with ⟨i, hi, hr'⟩ + subst hr' + have hi_val : i < k := hi + have hpos : runnerPos (Runner.mk ((i : ℝ) + 1)) (((k : ℝ) + 1)⁻¹) = ((i : ℝ) + 1) * ((k : ℝ) + 1)⁻¹ := by + calc + runnerPos (Runner.mk ((i : ℝ) + 1)) (((k : ℝ) + 1)⁻¹) + = ((i : ℝ) + 1) * (((k : ℝ) + 1)⁻¹) := + runnerPos_eq_product (by positivity) (by positivity) + (by + have h_ineq : ((i : ℝ) + 1) * ((k : ℝ) + 1)⁻¹ < 1 := by + calc + ((i : ℝ) + 1) * ((k : ℝ) + 1)⁻¹ = ((i : ℝ) + 1) / ((k : ℝ) + 1) := by field_simp + _ < 1 := by + apply (div_lt_one (by positivity)).mpr + have h_succ_lt : (i+1 : ℕ) < k+1 := Nat.succ_lt_succ hi_val + exact_mod_cast h_succ_lt + exact h_ineq) + _ = ((i : ℝ) + 1) * ((k : ℝ) + 1)⁻¹ := rfl + have hdist_val : circleDist (0 : ℝ) (((i : ℝ) + 1) / ((k : ℝ) + 1)) < 1 / ((k : ℝ) + 1) := by + -- hdist uses (k+1)⁻¹; convert to 1/(k+1) + calc + circleDist (0 : ℝ) (((i : ℝ) + 1) / ((k : ℝ) + 1)) = circleDist (0 : ℝ) (((i : ℝ) + 1) * ((k : ℝ) + 1)⁻¹) := by field_simp + _ < ((k : ℝ) + 1)⁻¹ := by + simpa [hpos] using hdist + _ = 1 / ((k : ℝ) + 1) := by field_simp + have hge_val : circleDist (0 : ℝ) (((i : ℝ) + 1) / ((k : ℝ) + 1)) ≥ 1 / ((k : ℝ) + 1) := by + simpa [show ((i : ℝ) + 1) = (i+1 : ℝ) by ring] using h_all_dist_ge i hi_val + linarith + rw [h_filter_empty] + simp + +/-- For any k > 0, the speed set [1, 2, ..., k] has a lonely time at t = 1/(k+1). + This proves the Lonely Runner Conjecture for the infinite family of consecutive + integer speeds, subsuming the k=2 and k=3 cases. -/ +theorem lonely_k_speeds_1_to_k (k : ℕ) (hk : k > 0) : lonelyTimeExists + ((List.range k).map fun i : ℕ => Runner.mk (i+1 : ℝ)) := by + refine ⟨1 / ((k : ℝ) + 1), ?_⟩ + exact ⟨0, origin_uncovered_at_one_over_k_plus_one k hk⟩ + +/-- Corollary: the k=2 case is a one-liner now. -/ +example : lonelyTimeExists ([Runner.mk 1, Runner.mk 2] : List Runner) := by + have h := lonely_k_speeds_1_to_k 2 (by norm_num) + simpa [List.range_succ, List.range_zero, show (1 : ℝ) + 1 = (2 : ℝ) by norm_num] using h + +/-- Corollary: the k=3 case is also a one-liner. -/ +example : lonelyTimeExists ([Runner.mk 1, Runner.mk 2, Runner.mk 3] : List Runner) := by + have h := lonely_k_speeds_1_to_k 3 (by norm_num) + simpa [List.range_succ, List.range_zero, + show (1 : ℝ) + 1 = (2 : ℝ) by norm_num, + show (2 : ℝ) + 1 = (3 : ℝ) by norm_num] using h + end Semantics.LonelyRunner