Three-gap theorem

DefinitionPoints of the three-gap configuration#✓fully proved

Let \(n\) be a natural number and \(\alpha\) a real number, and write \(\operatorname{frac}(t) = t - \lfloor t \rfloor\) for the fractional part of a real number \(t\). A real number \(x\) is a three-gap point of \(n\) and \(\alpha\) if \(x = \operatorname{frac}(k\alpha)\) for some natural number \(k < n\).

def IsThreeGapPoint (n : ℕ) (α x : ℝ) : Prop :=
  ∃ k : ℕ, k < n ∧ x = Int.fract ((k : ℝ) * α)

Used by 2

Used byGap lengths of the three-gap configuration · Three-gap theorem

DefinitionGap lengths of the three-gap configuration#✓fully proved

Let \(n\) be a natural number and \(\alpha\) a real number. In this definition a point means a three-gap point of \(n\) and \(\alpha\), that is, a number \(\operatorname{frac}(k\alpha) = k\alpha - \lfloor k\alpha \rfloor\) for a natural number \(k < n\). A real number \(d\) is a gap length of \(n\) and \(\alpha\) if either \(d = y - x\) for points \(x < y\) with no point strictly between \(x\) and \(y\), or there are a least point \(x_{\min}\) and a greatest point \(x_{\max}\) and \(d = 1 + x_{\min} - x_{\max}\).

def IsThreeGapLength (n : ℕ) (α d : ℝ) : Prop :=
  (∃ x y : ℝ, IsThreeGapPoint n α x ∧ IsThreeGapPoint n α y ∧ x < y ∧
    (∀ z : ℝ, IsThreeGapPoint n α z → x < z → z < y → False) ∧ d = y - x) ∨
  (∃ xlo xhi : ℝ, IsThreeGapPoint n α xlo ∧ IsThreeGapPoint n α xhi ∧
    (∀ z : ℝ, IsThreeGapPoint n α z → z ≤ xhi) ∧
    (∀ z : ℝ, IsThreeGapPoint n α z → xlo ≤ z) ∧ d = 1 + xlo - xhi)

Uses 1 · Used by 1

Statement usesPoints of the three-gap configuration

Used byThree-gap theorem

TheoremThree-gap theorem#✓fully proved

Let \(n \ge 1\) be a natural number and \(\alpha\) an irrational real number. Consider the points \(\operatorname{frac}(k\alpha) = k\alpha - \lfloor k\alpha \rfloor\) for \(0 \le k < n\) on the circle \([0, 1)\). The set of gap lengths of \(n\) and \(\alpha\), that is, the lengths of the gaps between cyclically consecutive points, including the gap that wraps around from the greatest point to the least, is finite and has at most three elements. If it has exactly three elements, the largest of them is the sum of the other two.

Proof: We formalize the standard successor argument of Sós (1958) and Świerczkowski (1959), following Alessandri and Berthé, Three distance theorems and combinatorics on words, §2.

theorem three_gap (n : ℕ) (hn : 1 ≤ n) (α : ℝ) (hα : Irrational α) :
    ∃ G : Finset ℝ,
      (∀ d : ℝ, d ∈ G ↔ IsThreeGapLength n α d) ∧
      G.card ≤ 3 ∧
      (G.card = 3 → ∃ a b c : ℝ,
        a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ a < b ∧ b < c ∧ c = a + b)

Sources

• https://en.wikipedia.org/wiki/Three-gap_theorem.

Uses 2

Statement usesGap lengths of the three-gap configuration

Proof usesPoints of the three-gap configuration

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.