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.

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