A safe second insertion at every failed boundary gives a strict time

Proved

LonelyRunner.SeparatedReplacements.failed_window_escape_of_boundary

by Whunt003 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationlonely-runnerlrc-component-rigidity-20261007number-theory

Write $d(x)=|x-\operatorname{round}(x)|$ for distance to the nearest integer. For finite $R,W\subseteq\mathbb N$ , put $S(n,R,W)=\{v\in\mathbb N:0<v<n,\ v\notin R\}\cup W$ . A strict time is a real $t$ with $d(vt)>1/n$ for every $v\in S(n,R,W)$ . Let $n,r,s,m,z,b\in\mathbb N$ satisfy $n\ge5$ , $n\le2r$ , $r<n$ , $m\ge2$ , $n-r\le b<m(n-r)$ , and $\gcd(r,b)=1$ . Suppose for every $a,c\in\mathbb Z$ with $ab-cr=1$ one has $d(z(a/r-1/(nmr)))>1/n$ . Then

S(n,\{r,s\},\{mr,z\})\text{ has a strict time}.

AI-assisted research and formalization. Independent mathematical review and novelty assessment remain outstanding.

Preamble

import Mathlib
import Mathlib.NumberTheory.Bertrand
import Mathlib.NumberTheory.Primorial
import Definitions.Def_LRC_ComponentRigidity_Defs

Formal statement

open LonelyRunner
open LonelyRunner.SeparatedReplacements
open LargeDeletionMatching SeparatedBands

set_option maxHeartbeats 1000000 in

theorem LonelyRunner.SeparatedReplacements.failed_window_escape_of_boundary {n r s m z b : ℕ}
    (hn : 5 ≤ n) (hlarge : n ≤ 2*r) (hrn : r < n) (hm : 2 ≤ m)
    (hab : n-r ≤ b) (hfail : b < m*(n-r)) (hcop : Nat.Coprime r b)
    (hsafe : ∀ a c : ℤ, a*(b:ℤ)-c*(r:ℤ)=1 →
      (1:ℝ)/n < ndist ((z:ℝ)*((a:ℝ)/r-1/((n:ℝ)*m*r)))) :
    HasStrictTime n r s (m*r) z := by sorry

Source

Wade Hunter, AI-assisted lonely-runner research, https://github.com/huntrontrakkr/lonely-runner; local source snapshot e63781c7cf2101e453103bfd9b215b72d162d05d, lean/LonelyRunner/SeparatedReplacements.lean, lines 24–79, declaration LonelyRunner.SeparatedReplacements.failed_window_escape_of_boundary. The snapshot identifies the submitted local source, not a publicly hosted commit.

View graph