Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

A surviving primitive fibre yields a strict time

Proved
LonelyRunner.ComplementaryEscape.strict_of_surviving_fibre

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

formalizationlonely-runnerlrc-shared-repair-20261007number-theory

Write d(x)=∣x−round⁡(x)∣d(x)=|x-\operatorname{round}(x)|d(x)=∣x−round(x)∣ for distance to the nearest integer. For finite sets R,W⊆NR,W\subseteq\mathbb NR,W⊆N, let 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 WS(n,R,W)={v∈N:0<v<n, v∈/R}∪W. A strict time means a real ttt such that d(vt)>1/nd(vt)>1/nd(vt)>1/n for every v∈S(n,R,W)v\in S(n,R,W)v∈S(n,R,W). Write Ur={0≤b<r:gcd⁡(r,b)=1}U_r=\{0\le b<r:\gcd(r,b)=1\}Ur​={0≤b<r:gcd(r,b)=1}, Fn,r={n−r≤b<n:gcd⁡(r,b)=1}F_{n,r}=\{n-r\le b<n:\gcd(r,b)=1\}Fn,r​={n−r≤b<n:gcd(r,b)=1}, and B(n,r,m,q,b)B(n,r,m,q,b)B(n,r,m,q,b) for the existence of an integer DDD with ∣nmD−q∣≤mr|nmD-q|\le mr∣nmD−q∣≤mr and r∣Db−qr\mid Db-qr∣Db−q. An active fibre for (n,r,m,q)(n,r,m,q)(n,r,m,q) consists of natural numbers (d,h,U,V)(d,h,U,V)(d,h,U,V) with d,V>0d,V>0d,V>0, h≥2h\ge2h≥2, r=dhr=dhr=dh, q=dUq=dUq=dU, gcd⁡(h,U)=gcd⁡(h,V)=1\gcd(h,U)=\gcd(h,V)=1gcd(h,U)=gcd(h,V)=1, ∣nmV−U∣≤hm|nmV-U|\le hm∣nmV−U∣≤hm, and, for every b∈Urb\in U_rb∈Ur​, B(n,r,m,q,b)B(n,r,m,q,b)B(n,r,m,q,b) if and only if h∣Vb−Uh\mid Vb-Uh∣Vb−U. Let F,GF,GF,G be active fibres for (n,r,m,q)(n,r,m,q)(n,r,m,q) and (n,r,m,u)(n,r,m,u)(n,r,m,u). Assume r≥7r\ge7r≥7, r+2≤n≤2rr+2\le n\le2rr+2≤n≤2r, m>0m>0m>0, r∈Rr\in Rr∈R, mr<q<umr<q<umr<q<u, F.h,G.h∈{3,4,6}F.h,G.h\in\{3,4,6\}F.h,G.h∈{3,4,6}, and either n≥12n\ge12n≥12 or F.h=4F.h=4F.h=4. Suppose B(n,r,m,u,c)B(n,r,m,u,c)B(n,r,m,u,c) implies ¬B(n,r,m,q,c)\neg B(n,r,m,q,c)¬B(n,r,m,q,c) for every c∈Urc\in U_rc∈Ur​. If some b∈Fn,rb\in F_{n,r}b∈Fn,r​ satisfies G.h∣G.Vb−G.UG.h\mid G.Vb-G.UG.h∣G.Vb−G.U and b((nG.V/G.h+1)/(u/(mr)))<m(n−r)b((nG.V/G.h+1)/(u/(mr)))<m(n-r)b((nG.V/G.h+1)/(u/(mr)))<m(n−r), then S(n,R,{mr,q,u})S(n,R,\{mr,q,u\})S(n,R,{mr,q,u}) has a strict time. The quotients in the margin condition are real.

Preamble
import Mathlib
import Mathlib.Data.ZMod.Units
import Mathlib.GroupTheory.Index
import Mathlib.RingTheory.Coprime.Lemmas
import Mathlib.RingTheory.Int.Basic
import Definitions.Def_LRC_SharedRepair_Defs
Formal statement
open LonelyRunner
open LonelyRunner.ComplementaryEscape
open CollectiveUnits CollectiveSecondFastest CollectiveFibreNormalForm

/-- All geometric hypotheses of an escape are derived from the active
small-fibre certificates; only the selected flank's arithmetic margin remains. -/
theorem LonelyRunner.ComplementaryEscape.strict_of_surviving_fibre {n r m q u b : ℕ} {R : Finset ℕ}
    (F : ActiveFibre n r m q) (G : ActiveFibre n r m u)
    (hr : 7 ≤ r) (hrmax : r+2 ≤ n) (hm : 0 < m) (hrR : r ∈ R)
    (hlarge : n ≤ 2*r) (hpq : m*r < q) (hqu : q < u)
    (hF : F.h=3 ∨ F.h=4 ∨ F.h=6) (hG : G.h=3 ∨ G.h=4 ∨ G.h=6)
    (hsize : 12 ≤ n ∨ F.h=4)
    (hcomp : ∀c ∈ units r, CollectiveBoundary.Blocks (n:ℤ) r m u c →
      ¬CollectiveBoundary.Blocks (n:ℤ) r m q c)
    (hb : b ∈ primitiveFlanks n r) (hbg : (G.h:ℤ) ∣ (G.V:ℤ)*b-G.U)
    (hmargin : (b:ℝ)*(((n:ℝ)*G.V/G.h+1)/((u:ℝ)/((m:ℝ)*r))) <
      (m:ℝ)*((n:ℝ)-r)) :
    SeparatedMulti.HasStrictTime n R {m*r,q,u} := by sorry
Source
Wade Hunter, lonely-runner research repository, https://github.com/huntrontrakkr/lonely-runner; local source snapshot 9b5f51aa235e321a3ec794c9bf60358933a8e6dc, lean/LonelyRunner/ComplementaryEscape.lean, lines 114–176, declaration LonelyRunner.ComplementaryEscape.strict_of_surviving_fibre. AI-assisted formalization. The snapshot identifier records the submitted local source; it is not a claim that this commit is publicly hosted.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me