Goddyn–Wong acceleration window

Definition

LRC_GW

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

goddyn-wonglonely-runner

For natural numbers $n,r,m$ , the Goddyn–Wong window condition asserts that every integer $b$ with $n-r\le b<m(n-r)$ has a common factor with $r$ . This predicate expresses the individual acceleration criterion used in the Lonely Runner problem.

Definition code

import Mathlib.Data.Nat.GCD.Basic
namespace LonelyRunner.SeparatedReplacements
def GW (n r m : ℕ) : Prop :=
  ∀ b : ℕ, n-r ≤ b → b < m*(n-r) → ¬ Nat.Coprime r b
end LonelyRunner.SeparatedReplacements

Source

Wade Hunter, AI-assisted Lonely Runner research, lean/LonelyRunner/SeparatedReplacements.lean, definition GW; https://github.com/huntrontrakkr/lonely-runner

View graph