Strict safety persists along a nearby rational-center segment

Proved

LonelyRunner.ComponentRestoration.safe_segment

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. Let $n,r,v\in\mathbb N$ , $a\in\mathbb Z$ , and $t,u\in\mathbb R$ . Assume $0<r<n$ , $v<n$ , $d(va/r)\ge1/r$ , $|rt-a|\le1/n$ , and $d(vt)>1/n$ . If $u$ is between $t$ and $a/r$ , then

d(vu)>1/n.

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.ComponentRestoration
open SeparatedMulti InteractionComponents


theorem LonelyRunner.ComponentRestoration.safe_segment {n r v : ℕ} {a : ℤ} {t u : ℝ}
    (hn : 0 < n) (hr : 0 < r) (hrn : r < n) (hvn : v < n)
    (hcenter : 1/(r:ℝ) ≤ ndist ((v:ℝ)*((a:ℝ)/r)))
    (hbad : |(r:ℝ)*t-a| ≤ 1/(n:ℝ))
    (hsafe : 1/(n:ℝ) < ndist ((v:ℝ)*t))
    (hu : u ∈ Set.Icc (min t ((a:ℝ)/r)) (max t ((a:ℝ)/r))) :
    1/(n:ℝ) < ndist ((v:ℝ)*u) := by sorry

Source

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

View graph