Knight and king distances on the integer lattice

DefinitionKnight moves#✓fully proved

For integers \(a\) and \(b\), the \((a,b)\)-knight's move set is

\[N_{a,b} = \{(\pm a, \pm b), (\pm b, \pm a)\} \subset \mathbb{Z}^2,\]

the finite set of the points \((a, b)\), \((-a, b)\), \((a, -b)\), \((-a, -b)\), \((b, a)\), \((-b, a)\), \((b, -a)\) and \((-b, -a)\).

public def knightMoves (a b : ℤ) : Finset (ℤ × ℤ) :=
  {(b, a), (a, b), (-a, b), (-b, a), (-b, -a), (-a, -b), (a, -b), (b, -a)}

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of N_{a,b}.

Used by 7

Used byKnight distance asymptotics · Uniform bound for knight distance on a box · Velocity formula for the (a, b)-knight · The usual knight reaches (1, 1) in two moves · The knight reaches \((1,2)\) in one move · The knight needs three moves to reach \((1,0)\) · The knight's distance to the origin is zero

DefinitionKing moves#✓fully proved

The king's move set \(K \subset \mathbb{Z}^2\) consists of the eight unit horizontal, vertical and diagonal steps:

\[K = \{(1, 0), (1, 1), (0, 1), (-1, 1), (-1, 0), (-1, -1), (0, -1), (1, -1)\}.\]

public def kingMoves : Finset (ℤ × ℤ) :=
  {(1, 0), (1, 1), (0, 1), (-1, 1), (-1, 0), (-1, -1), (0, -1), (1, -1)}

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of K.

Used by 1

Used byKing distance is the max norm

DefinitionPiece distance on the integer lattice#✓fully proved

Let \(A \subseteq \mathbb{Z}^2\) be a finite set of moves and, for \(h \ge 1\), let \(hA = \{a_1 + \dots + a_h : a_1, \dots, a_h \in A\}\) be its \(h\)-fold sumset. The piece distance of a point \(p \in \mathbb{Z}^2\) for \(A\) is the natural number that is \(0\) if \(p = (0,0)\) and otherwise the infimum of the set of integers \(h \ge 1\) with \(p \in hA\), where the infimum of the empty set is taken to be \(0\).

Points other than the origin that are not a sum of moves from \(A\) therefore have distance \(0\).

public noncomputable def pieceDistance (A : Finset (ℤ × ℤ)) (p : ℤ × ℤ) : ℕ :=
  if p = 0 then 0 else sInf {h : ℕ | 1 ≤ h ∧ p ∈ h • A}

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of A(x,y).

Used by 9

Used byKnight distance asymptotics · Uniform bound for knight distance on a box · Velocity formula for the (a, b)-knight · Piece distance from a minimal fold · King distance is the max norm · The usual knight reaches (1, 1) in two moves · The knight reaches \((1,2)\) in one move · The knight needs three moves to reach \((1,0)\) · The knight's distance to the origin is zero

DefinitionMax-norm ball#✓fully proved

For a natural number \(h\), the max-norm ball \(B_h \subset \mathbb{Z}^2\) is the product of two copies of the integer interval \(\{-h, \dots, h\}\), that is, the set of lattice points \((x, y)\) with \(\max(|x|, |y|) \le h\).

public def maxNormBall (h : ℕ) : Finset (ℤ × ℤ) :=
  Finset.Icc (-(h : ℤ)) h ×ˢ Finset.Icc (-(h : ℤ)) h

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of B_h.

Used by 2

Used byNumber of points in the max-norm ball · Velocity formula for the (a, b)-knight

TheoremPiece distance from a minimal fold#✓fully proved

Let \(A \subset \mathbb{Z}^2\) be a finite set, let \(p \in \mathbb{Z}^2\) be nonzero and let \(n \ge 1\) be a natural number. If \(p\) lies in the \(n\)-fold sumset \(nA = \{a_1 + \dots + a_n : a_1, \dots, a_n \in A\}\), and every natural number \(h \ge 1\) with \(p \in hA\) satisfies \(n \le h\), then the piece distance of \(p\) for \(A\) is \(n\).

public theorem pieceDistance_eq_of_mem_of_forall
    (A : Finset (ℤ × ℤ)) (p : ℤ × ℤ) (n : ℕ)
    (hp : p ≠ 0) (hn : 1 ≤ n) (hmem : p ∈ n • A)
    (hmin : ∀ h : ℕ, 1 ≤ h → p ∈ h • A → n ≤ h) :
    pieceDistance A p = n

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of A(x,y).

Uses 1 · Used by 4

Statement usesPiece distance on the integer lattice

Used byKing distance is the max norm · The usual knight reaches (1, 1) in two moves · The knight reaches \((1,2)\) in one move · The knight needs three moves to reach \((1,0)\)

TheoremKing distance is the max norm#✓fully proved

For every lattice point \(p = (x, y) \in \mathbb{Z}^2\), the piece distance of \(p\) for the king's move set \(K\) is \(\max(|x|, |y|)\).

public theorem pieceDistance_kingMoves (p : ℤ × ℤ) :
    pieceDistance kingMoves p = max p.1.natAbs p.2.natAbs

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definitions of A(x,y) and K.

Uses 3

Statement usesKing moves · Piece distance on the integer lattice

Proof usesPiece distance from a minimal fold

TheoremThe knight reaches \((1,2)\) in one move#✓fully proved

Let \(N \subseteq \mathbb{Z}^2\) be the move set of the usual knight, consisting of the eight vectors \((\pm 1, \pm 2)\) and \((\pm 2, \pm 1)\). The piece distance of the point \((1,2)\) for \(N\) is \(1\).

public theorem pieceDistance_knightMoves_one_two :
    pieceDistance (knightMoves 1 2) (1, 2) = 1

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of the usual knight following the definition of N_{a,b}.

Uses 3

Statement usesKnight moves · Piece distance on the integer lattice

Proof usesPiece distance from a minimal fold

TheoremThe knight needs three moves to reach \((1,0)\)#✓fully proved

Let \(N \subseteq \mathbb{Z}^2\) be the move set of the usual knight, consisting of the eight vectors \((\pm 1, \pm 2)\) and \((\pm 2, \pm 1)\). The piece distance of the point \((1,0)\) for \(N\) is \(3\).

public theorem pieceDistance_knightMoves_one_zero :
    pieceDistance (knightMoves 1 2) (1, 0) = 3

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), characteristic value for the usual knight.

Uses 3

Statement usesKnight moves · Piece distance on the integer lattice

Proof usesPiece distance from a minimal fold

TheoremThe usual knight reaches (1, 1) in two moves#✓fully proved

For the usual knight's move set \(N_{1,2} = \{(\pm 1, \pm 2), (\pm 2, \pm 1)\}\), the piece distance of the point \((1, 1)\) is \(2\).

public theorem pieceDistance_knightMoves_one_one :
    pieceDistance (knightMoves 1 2) (1, 1) = 2

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), characteristic value for the usual knight.

Uses 3

Statement usesKnight moves · Piece distance on the integer lattice

Proof usesPiece distance from a minimal fold

TheoremThe knight's distance to the origin is zero#✓fully proved

Let \(N \subseteq \mathbb{Z}^2\) be the move set of the usual knight, consisting of the eight vectors \((\pm 1, \pm 2)\) and \((\pm 2, \pm 1)\). The piece distance of the origin \((0,0)\) for \(N\) is \(0\).

This holds by the definition of piece distance, which sets the distance at the origin to \(0\).

public theorem pieceDistance_knightMoves_zero_zero :
    pieceDistance (knightMoves 1 2) (0, 0) = 0

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of A(0,0).

Uses 2

Statement usesKnight moves · Piece distance on the integer lattice

TheoremNumber of points in the max-norm ball#✓fully proved

For every natural number \(h\), the max-norm ball \(B_h = \{(x, y) \in \mathbb{Z}^2 : \max(|x|, |y|) \le h\}\) has exactly \((2h+1)^2\) points.

public theorem card_maxNormBall (h : ℕ) : (maxNormBall h).card = (2 * h + 1) ^ 2

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), definition of B_h.

Uses 1

Statement usesMax-norm ball

TheoremUniform bound for knight distance on a box#●ready to prove

There is an absolute constant \(M \in \mathbb{R}\) such that for all natural numbers \(a\) and \(b\) with \(1 \le a < b\), \(\gcd(a, b) = 1\) and \(a + b\) odd, every lattice point \((x, y) \in \mathbb{Z}^2\) with \(\max(|x|, |y|) \le a + b\) has piece distance at most \(Mb\) for the \((a,b)\)-knight's move set \(N_{a,b} = \{(\pm a, \pm b), (\pm b, \pm a)\}\).

public theorem_wanted knight_distance_uniform_on_box :
    ∃ M : ℝ, ∀ a b : ℕ,
      1 ≤ a → a < b → Nat.Coprime a b → Odd (a + b) →
      ∀ p : ℤ × ℤ,
        max |p.1| |p.2| ≤ ((a + b : ℕ) : ℤ) →
        (pieceDistance (knightMoves (a : ℤ) (b : ℤ)) p : ℝ) ≤ M * b

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), Lemma 2.1.

Uses 2

Statement usesKnight moves · Piece distance on the integer lattice

TheoremKnight distance asymptotics#●ready to prove

There is an absolute constant \(M \in \mathbb{R}\) with the following property. Let \(a\) and \(b\) be natural numbers with \(1 \le a < b\), \(\gcd(a, b) = 1\) and \(a + b\) odd, let \(N_{a,b} = \{(\pm a, \pm b), (\pm b, \pm a)\}\) be the \((a,b)\)-knight's move set, and for \(p \in \mathbb{Z}^2\) let \(d_{a,b}(p)\) be the piece distance of \(p\) for \(N_{a,b}\). Then for all integers \(x\) and \(y\) with \(0 \le y \le x\): if \(by \le ax\), then \(|d_{a,b}(x, y) - x/b| \le Mb\); and if \(ax < by\), then \(|d_{a,b}(x, y) - (x + y)/(a + b)| \le Mb\).

public theorem_wanted knight_distance_asymptotics :
    ∃ M : ℝ, ∀ (a b : ℕ) (x y : ℤ),
      1 ≤ a → a < b → Nat.Coprime a b → Odd (a + b) →
      0 ≤ y → y ≤ x →
      (((b : ℤ) * y ≤ (a : ℤ) * x →
          |(pieceDistance (knightMoves (a : ℤ) (b : ℤ)) (x, y) : ℝ) -
              (x : ℝ) / (b : ℝ)| ≤ M * b) ∧
        ((a : ℤ) * x < (b : ℤ) * y →
          |(pieceDistance (knightMoves (a : ℤ) (b : ℤ)) (x, y) : ℝ) -
              ((x : ℝ) + (y : ℝ)) / ((a : ℝ) + (b : ℝ))| ≤ M * b))

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), Theorem 1.1.

Uses 2

Statement usesKnight moves · Piece distance on the integer lattice

TheoremVelocity formula for the (a, b)-knight#●ready to prove

Let \(a\) and \(b\) be natural numbers with \(1 \le a < b\), \(\gcd(a, b) = 1\) and \(a + b\) odd, let \(N_{a,b} = \{(\pm a, \pm b), (\pm b, \pm a)\}\) be the \((a,b)\)-knight's move set, and for \(p \in \mathbb{Z}^2\) let \(d_{a,b}(p)\) be the piece distance of \(p\) for \(N_{a,b}\). For a natural number \(h\), let \(B_h = \{(x, y) \in \mathbb{Z}^2 : \max(|x|, |y|) \le h\}\) be the max-norm ball and let \(\bar{d}(h) = |B_h|^{-1} \sum_{p \in B_h} d_{a,b}(p)\) be the average of \(d_{a,b}\) over \(B_h\). Then

\[\lim_{h \to \infty} \frac{2h}{3} \, \bar{d}(h)^{-1} = \frac{2(a+b)b^2}{a^2 + 3b^2}.\]

public theorem_wanted knight_velocity_formula (a b : ℕ)
    (ha : 1 ≤ a) (hab : a < b) (hcoprime : Nat.Coprime a b)
    (hodd : Odd (a + b)) :
    Filter.Tendsto
      (fun h : ℕ =>
        (2 * (h : ℝ) / 3) *
          (((∑ p ∈ maxNormBall h,
              (pieceDistance (knightMoves (a : ℤ) (b : ℤ)) p : ℝ)) /
            ((maxNormBall h).card : ℝ))⁻¹))
      Filter.atTop
      (nhds
        (2 * ((a : ℝ) + (b : ℝ)) * (b : ℝ) ^ 2 /
          ((a : ℝ) ^ 2 + 3 * (b : ℝ) ^ 2)))

Sources

• Christian Táfula, Knights Are 24/13 Times Faster than the King, The Fibonacci Quarterly 62(3) (2024), Theorem 1.3.

Uses 3

Statement usesKnight moves · Max-norm ball · Piece distance on the integer lattice

11 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.