Prove2Me

GW matching is forced when insertion components have size at most two

Proved
LonelyRunner.SmallComponentRigidity.matching_windows

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, ∣R∣=∣W∣|R|=|W|, the insertion-component hypothesis holds, and S(n,R,W)S(n,R,W) has no strict time. Then

∃ 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).

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.matching_windows {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) (hno : ¬ HasStrictTime n R W) :
    ∃ 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 143–218, declaration LonelyRunner.SmallComponentRigidity.matching_windows. The snapshot identifies the submitted local source, not a publicly hosted commit.

View graph