Prove2Me

Strictness or GW rigidity for arbitrarily many small insertion components

Proved
LonelyRunner.SmallComponentRigidity.strict_or_gw_tight

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

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

Write d(x)=∣x−round⁡(x)∣d(x)=|x-\operatorname{round}(x)| for distance to the nearest integer. For finite R,W⊆NR,W\subseteq\mathbb N, put S(n,R,W)={v∈N:0<v<n, v∉R}∪WS(n,R,W)=\{v\in\mathbb N:0<v<n,\ v\notin R\}\cup W. A strict time is a real tt with d(vt)>1/nd(vt)>1/n for every v∈S(n,R,W)v\in S(n,R,W). Write GW⁡(n,r,m)\operatorname{GW}(n,r,m) for the assertion that no natural number bb with n−r≤b<m(n−r)n-r\le b<m(n-r) is coprime to rr. A separated cut C⊆WC\subseteq W satisfies p+q<ngcd⁡(p,q)p+q<n\gcd(p,q) for every p∈Cp\in C and q∈W∖Cq\in W\setminus C. The insertion-component hypothesis means that WW admits a finite partition into blocks of size at most two, each a separated cut. Equivalently, the graph joining distinct p,qp,q when ngcd⁡(p,q)≤p+qn\gcd(p,q)\le p+q has components of size at most two. Assume n≥5n\ge5, n≤2rn\le2r and r<nr<n for every r∈Rr\in R, every p∈Wp\in W is at least nn, and ∣R∣=∣W∣|R|=|W|, with the insertion-component hypothesis satisfied. Then either S(n,R,W)S(n,R,W) has a strict time, or it has no strict time and both conclusions hold:

∀v∈S(n,R,W),d(v/n)≥1/n,\forall v\in S(n,R,W),\quad d(v/n)\ge1/n, ∃ a bijection f:R→W ∀r∈R ∃mr≥2:f(r)=mrr ∧GW⁡(n,r,mr).\exists\text{ a bijection }f:R\to W\ \forall r\in R\ \exists m_r\ge2:\quad f(r)=m_rr\ \land\operatorname{GW}(n,r,m_r).

The second branch is tightness with an explicit weak lonely time t=1/n. No divisibility matching or bound on the number of components is assumed. The unrestricted conjecture and larger connected insertion components remain outside this result.

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


theorem LonelyRunner.SmallComponentRigidity.strict_or_gw_tight {n : ℕ} {R W : Finset ℕ}
    (hn : 5 ≤ n) (hR : ∀ r ∈ R, n ≤ 2*r ∧ r < n)
    (hW : ∀ p ∈ W, n ≤ p) (hparts : PairComponents n W)
    (hcard : R.card=W.card) :
    HasStrictTime n R W ∨
      (¬ HasStrictTime n R W ∧ WeakAt n R W (1/(n:ℝ)) ∧
        ∃ f : ℕ → ℕ, Set.BijOn f (R : Set ℕ) (W : Set ℕ) ∧
          ∀ r ∈ R, ∃ m : ℕ, 2 ≤ m ∧ f r=m*r ∧ GW n r m) := by sorry
Source
Wade Hunter, AI-assisted lonely-runner research, https://github.com/huntrontrakkr/lonely-runner; local source snapshot e63781c7cf2101e453103bfd9b215b72d162d05d, lean/LonelyRunner/SmallComponentRigidity.lean, lines 298–311, declaration LonelyRunner.SmallComponentRigidity.strict_or_gw_tight. The snapshot identifies the submitted local source, not a publicly hosted commit.

View graph