A surviving primitive fibre yields a strict time
ProvedLonelyRunner.ComplementaryEscape.strict_of_surviving_fibreformalizationlonely-runnerlrc-shared-repair-20261007number-theory
Write for distance to the nearest integer. For finite sets , let . A strict time means a real such that for every . Write , , and for the existence of an integer with and . An active fibre for consists of natural numbers with , , , , , , and, for every , if and only if . Let be active fibres for and . Assume , , , , , , and either or . Suppose implies for every . If some satisfies and , then 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.