Chocolate bar games

DefinitionNS property#✓fully proved

A function \(h : \mathbb{N} \to \mathbb{N}\) has the NS property if it is monotone (weakly increasing) and, for all \(z, z' \in \mathbb{N}\) and every natural number \(i \ge 1\), \(\lfloor z / 2^i \rfloor = \lfloor z' / 2^i \rfloor\) implies \(\lfloor h(z) / 2^{i-1} \rfloor = \lfloor h(z') / 2^{i-1} \rfloor\).

public def HasNSProperty (h : ℕ → ℕ) : Prop :=
  Monotone h ∧ ∀ z z' i : ℕ, 0 < i → z / 2 ^ i = z' / 2 ^ i →
    h z / 2 ^ (i - 1) = h z' / 2 ^ (i - 1)
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definition 11 (text of arXiv:2207.09134v1, NS property in Section 2).
Used by 17
Used byMex step for chocolate bars with many functions · Mex step for chocolate bars with one function · Mex step for chocolate bars with two functions · Nim-sum Grundy numbers of chocolate bars with four functions · Nim-sum Grundy numbers of chocolate bars with two functions · Constant functions have the NS property · Halving functions have the NS property · Constant extension preserves the NS property · The NS property characterises nim-sum Grundy numbers of two-dimensional chocolate bars · Nim-sum sets under clamping by functions with the NS property · Nim-sum image identity for one NS function · Nim-sum image identity for two NS functions · Indicator functions with the NS property · Quotients of a truncated NS function by powers of two · Sections of the Nim pass indicator with the NS property · The identity function lacks the NS property · NS property of sections and the three-dimensional chocolate bar

TheoremConstant functions have the NS property#✓fully proved

For every natural number \(c\), the constant function \(\mathbb{N} \to \mathbb{N}\) with value \(c\) has the NS property.

public theorem hasNSProperty_const (c : ℕ) : HasNSProperty fun _ ↦ c
Sources
  • characteristic lemma for the NS property of Miyadera, Manabe and Singh, INTEGERS 25 (2025), Article G3, Definition 11.
Uses 1
Statement usesNS property

TheoremThe identity function lacks the NS property#✓fully proved

The identity function on the natural numbers does not have the NS property: \(\lfloor 0/2 \rfloor = \lfloor 1/2 \rfloor\), but \(0 \ne 1\).

public theorem not_hasNSProperty_id : ¬ HasNSProperty id
Sources
  • characteristic lemma for the NS property of Miyadera, Manabe and Singh, INTEGERS 25 (2025), Article G3, Definition 11.
Uses 1
Statement usesNS property

TheoremConstant extension preserves the NS property#●ready to prove

Let \(z \in \mathbb{N}\) and let \(h : \mathbb{N} \to \mathbb{N}\) satisfy \(h(a) \le h(b)\) whenever \(a \le b \le z\), and \(\lfloor h(a) / 2^{i-1} \rfloor = \lfloor h(b) / 2^{i-1} \rfloor\) whenever \(a, b \le z\), \(i \ge 1\) and \(\lfloor a / 2^i \rfloor = \lfloor b / 2^i \rfloor\). Then the function sending \(x\) to \(h(x)\) for \(x \le z\) and to \(h(z)\) for \(x > z\) has the NS property.

public theorem_wanted hasNSProperty_extend_const (z : ℕ) (h : ℕ → ℕ)
    (hmono : ∀ a b, a ≤ b → b ≤ z → h a ≤ h b)
    (hns : ∀ a b i : ℕ, a ≤ z → b ≤ z → 0 < i → a / 2 ^ i = b / 2 ^ i →
      h a / 2 ^ (i - 1) = h b / 2 ^ (i - 1)) :
    HasNSProperty fun x ↦ if x ≤ z then h x else h z
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 1.
Uses 1
Statement usesNS property

TheoremTaking a minimum preserves quotients by powers of two#●ready to prove

Let \(a, b, c, k \in \mathbb{N}\). If \(\lfloor a / 2^k \rfloor = \lfloor b / 2^k \rfloor\), then \(\lfloor \min(a, c) / 2^k \rfloor = \lfloor \min(b, c) / 2^k \rfloor\).

public theorem_wanted min_div_two_pow_eq_of_div_two_pow_eq {a b k : ℕ}
    (hab : a / 2 ^ k = b / 2 ^ k) (c : ℕ) :
    min a c / 2 ^ k = min b c / 2 ^ k
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 2 (i).

TheoremQuotients of a truncated NS function by powers of two#●ready to prove

Let \(h : \mathbb{N} \to \mathbb{N}\) have the NS property and let \(z, z', k \in \mathbb{N}\) with \(k \ge 1\) and \(\lfloor z' / 2^k \rfloor = \lfloor z / 2^k \rfloor\). Then for every \(y \in \mathbb{N}\), \(\lfloor \min(h(z'), y) / 2^{k-1} \rfloor = \lfloor \min(h(z), y) / 2^{k-1} \rfloor\).

public theorem_wanted HasNSProperty.min_div_two_pow_eq {h : ℕ → ℕ} (hh : HasNSProperty h)
    {z z' k : ℕ} (hk : 0 < k) (hz : z' / 2 ^ k = z / 2 ^ k) (y : ℕ) :
    min (h z') y / 2 ^ (k - 1) = min (h z) y / 2 ^ (k - 1)
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 2 (ii).
Uses 1
Statement usesNS property

TheoremMex step for chocolate bars with one function#●ready to prove

Let \(g : \mathbb{N} \to \mathbb{N}\) have the NS property, and let \(x, z, c\) be natural numbers with \(x \le g(z)\) and \(c < x \oplus z\), where \(\oplus\) is nim-sum (bitwise exclusive or). Then \(c = u \oplus z\) for some \(u < x\), or \(c = \min(g(w), x) \oplus w\) for some \(w < z\).

public theorem_wanted HasNSProperty.exists_of_lt_xor {g : ℕ → ℕ} (hg : HasNSProperty g)
    {x z c : ℕ} (hx : x ≤ g z) (hc : c < x ^^^ z) :
    (∃ u < x, c = u ^^^ z) ∨ ∃ w < z, c = min (g w) x ^^^ w
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 3 (a).
Uses 1
Statement usesNS property

TheoremMex step for chocolate bars with two functions#●ready to prove

Let \(g, h : \mathbb{N} \to \mathbb{N}\) have the NS property, and let \(x, y, z, c\) be natural numbers with \(x \le g(z)\), \(y \le h(z)\) and \(c < x \oplus y \oplus z\), where \(\oplus\) is nim-sum (bitwise exclusive or). Then \(c = u \oplus y \oplus z\) for some \(u < x\), or \(c = x \oplus v \oplus z\) for some \(v < y\), or \(c = \min(g(w), x) \oplus \min(h(w), y) \oplus w\) for some \(w < z\).

public theorem_wanted HasNSProperty.exists_of_lt_xor_xor {g h : ℕ → ℕ}
    (hg : HasNSProperty g) (hh : HasNSProperty h) {x y z c : ℕ} (hx : x ≤ g z)
    (hy : y ≤ h z) (hc : c < x ^^^ y ^^^ z) :
    (∃ u < x, c = u ^^^ y ^^^ z) ∨ (∃ v < y, c = x ^^^ v ^^^ z) ∨
      ∃ w < z, c = min (g w) x ^^^ min (h w) y ^^^ w
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 3 (b).
Uses 1
Statement usesNS property

TheoremMex step for chocolate bars with many functions#●ready to prove

Let \(m\) be a natural number, let \(f_1, \dots, f_m : \mathbb{N} \to \mathbb{N}\) have the NS property, and let \(x_1, \dots, x_m, z, c\) be natural numbers with \(x_t \le f_t(z)\) for all \(t\) and \(c < x_1 \oplus \cdots \oplus x_m \oplus z\), where \(\oplus\) is nim-sum (bitwise exclusive or). Then either there are an index \(i\) and some \(u < x_i\) such that \(c\) is the nim-sum \(x_1 \oplus \cdots \oplus x_m \oplus z\) with \(x_i\) replaced by \(u\), or there is some \(w < z\) with \(c = \min(x_1, f_1(w)) \oplus \cdots \oplus \min(x_m, f_m(w)) \oplus w\).

public theorem_wanted exists_of_lt_foldl_xor {m : ℕ} {f : Fin m → ℕ → ℕ}
    (hf : ∀ t, HasNSProperty (f t)) {x : Fin m → ℕ} {z c : ℕ} (hx : ∀ t, x t ≤ f t z)
    (hc : c < (List.ofFn x).foldl (· ^^^ ·) 0 ^^^ z) :
    (∃ i, ∃ u < x i, c = (List.ofFn (Function.update x i u)).foldl (· ^^^ ·) 0 ^^^ z) ∨
      ∃ w < z, c = (List.ofFn fun t ↦ min (x t) (f t w)).foldl (· ^^^ ·) 0 ^^^ w
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 4.
Uses 1
Statement usesNS property

TheoremNim-sum image identity for two NS functions#●ready to prove

Let \(g, h : \mathbb{N} \to \mathbb{N}\) have the NS property and let \(x, y, z \in \mathbb{N}\) with \(x \le g(z)\) and \(y \le h(z)\). Writing \(\oplus\) for the nim-sum (bitwise exclusive or) of natural numbers, the sets \(\{x \oplus y \oplus w : w < z\}\) and \(\{\min(g(w), x) \oplus \min(h(w), y) \oplus w : w < z\}\) are equal, where \(w\) ranges over the natural numbers.

public theorem_wanted HasNSProperty.image_xor_xor_eq {g h : ℕ → ℕ} (hg : HasNSProperty g)
    (hh : HasNSProperty h) {x y z : ℕ} (hx : x ≤ g z) (hy : y ≤ h z) :
    {c | ∃ w < z, c = x ^^^ y ^^^ w} = {c | ∃ w' < z, c = min (g w') x ^^^ min (h w') y ^^^ w'}
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 5, equation (19).
Uses 1
Statement usesNS property

TheoremNim-sum image identity for one NS function#●ready to prove

Let \(g : \mathbb{N} \to \mathbb{N}\) have the NS property and let \(x, z \in \mathbb{N}\) with \(x \le g(z)\). Writing \(\oplus\) for the nim-sum (bitwise exclusive or) of natural numbers, the sets \(\{x \oplus w : w < z\}\) and \(\{\min(g(w), x) \oplus w : w < z\}\) are equal, where \(w\) ranges over the natural numbers.

public theorem_wanted HasNSProperty.image_xor_eq {g : ℕ → ℕ} (hg : HasNSProperty g)
    {x z : ℕ} (hx : x ≤ g z) :
    {c | ∃ w < z, c = x ^^^ w} = {c | ∃ w' < z, c = min (g w') x ^^^ w'}
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 5, equation (20).
Uses 1
Statement usesNS property

TheoremHalving functions have the NS property#●ready to prove

For every natural number \(m \ge 1\), the function \(x \mapsto \lfloor x / 2^m \rfloor\) on \(\mathbb{N}\) has the NS property.

public theorem_wanted hasNSProperty_div_two_pow {m : ℕ} (hm : 0 < m) :
    HasNSProperty fun x ↦ x / 2 ^ m
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 7.
Uses 1
Statement usesNS property

TheoremEqual quotients by a power of two lie in one dyadic block#●ready to prove

Let \(i\) be a natural number and let \(z < z'\) be natural numbers. Then \(\lfloor z / 2^i \rfloor = \lfloor z' / 2^i \rfloor\) if and only if there is a natural number \(d\) with \(d \cdot 2^i \le z\) and \(z' < (d + 1) \cdot 2^i\).

public theorem_wanted div_two_pow_eq_iff_exists_block {z z' i : ℕ} (hzz' : z < z') :
    z / 2 ^ i = z' / 2 ^ i ↔ ∃ d, d * 2 ^ i ≤ z ∧ z' < (d + 1) * 2 ^ i
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 8 (a).

TheoremDyadic splitting of two numbers with different quotients#●ready to prove

Let \(z, z', i\) be natural numbers with \(\lfloor z / 2^i \rfloor < \lfloor z' / 2^i \rfloor\). Then there are natural numbers \(c\), \(s\) and \(t\) with \(s \ge i\), \(t < 2^s\), \(z = c \cdot 2^{s+1} + t\) and \(c \cdot 2^{s+1} + 2^s \le z'\).

public theorem_wanted exists_split_of_div_two_pow_lt {z z' i : ℕ}
    (h : z / 2 ^ i < z' / 2 ^ i) :
    ∃ c s t : ℕ, i ≤ s ∧ t < 2 ^ s ∧ z = c * 2 ^ (s + 1) + t ∧
      c * 2 ^ (s + 1) + 2 ^ s ≤ z'
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 8 (b).

TheoremIndicator functions with the NS property#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) be monotone, with \(f(x) \le 1\) for all \(x\) and \(f(x) = 1\) for some \(x\). Then \(f\) has the NS property if and only if there is an even \(m \in \mathbb{N}\) such that \(f\) is the indicator function of \(\{n \in \mathbb{N} : n \ge m\}\), that is, \(f(n) = 1\) for \(n \ge m\) and \(f(n) = 0\) for \(n < m\).

public theorem_wanted indicator_Ici_even_iff_hasNSProperty {f : ℕ → ℕ} (hf : Monotone f)
    (hle : ∀ x, f x ≤ 1) (hone : ∃ x, f x = 1) :
    (∃ m, Even m ∧ f = (Set.Ici m).indicator 1) ↔ HasNSProperty f
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 9.
Uses 1
Statement usesNS property

DefinitionGrundy number of a chocolate bar#✓fully proved

Let \(f_1, \dots, f_s : \mathbb{N} \to \mathbb{N}\). For coordinates \(x = (x_1, \dots, x_s) \in \mathbb{N}^s\) and a width \(z \in \mathbb{N}\), the position \((x, z)\) stands for the chocolate bar \(\mathrm{CB}(f_1, \dots, f_s, x_1, \dots, x_s, z)\), whose column at width \(w \le z\) extends \(\min(f_t(w), x_t) + 1\) cells along axis \(t\). A move either lowers one coordinate \(x_i\) to some \(u < x_i\), keeping the width \(z\), or cuts the width to some \(w < z\), which replaces every \(x_t\) by \(\min(x_t, f_t(w))\). The Grundy number of \((x, z)\) is the mex (least natural number not attained) of the Grundy numbers of the positions reachable from \((x, z)\) in one move. It is defined for all \((x, z)\); the bars themselves are the positions with \(x_t \le f_t(z)\) for all \(t\).

MetaMathlibExt.chocolateBarGrundy · 15 lines 
public noncomputable def chocolateBarGrundy {s : ℕ} (f : Fin s → ℕ → ℕ) (x : Fin s → ℕ)
    (z : ℕ) : ℕ :=
  sInf {m | (∀ i u, u < x i → chocolateBarGrundy f (Function.update x i u) z ≠ m) ∧
    ∀ w, w < z → chocolateBarGrundy f (fun t ↦ min (x t) (f t w)) w ≠ m}
termination_by z + ∑ t, x t
decreasing_by
  · have hlt : ∑ t, Function.update x i u t < ∑ t, x t := by
      refine Finset.sum_lt_sum (fun j _ ↦ ?_) ⟨i, Finset.mem_univ _, by simpa⟩
      by_cases hj : j = i
      · subst hj; simp only [Function.update_self]; omega
      · simp [Function.update_of_ne hj]
    omega
  · have hle : ∑ t, min (x t) (f t w) ≤ ∑ t, x t :=
      Finset.sum_le_sum fun _ _ ↦ min_le_left _ _
    omega
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definitions 2, 8, 9 and 10 (two functions) and Section 4, before Theorem 5 (four functions).
Used by 5
Used byMex recursion for the Grundy number of a chocolate bar · The single bitter square has Grundy number zero · Nim-sum Grundy numbers of chocolate bars with four functions · Nim-sum Grundy numbers of chocolate bars with two functions · The NS property characterises nim-sum Grundy numbers of two-dimensional chocolate bars

TheoremMex recursion for the Grundy number of a chocolate bar#✓fully proved

Let \(f_1, \dots, f_s\) be functions \(\mathbb{N} \to \mathbb{N}\) and write \(G(x, z)\) for the Grundy number of the chocolate bar with coordinates \(x = (x_1, \dots, x_s) \in \mathbb{N}^s\) and width \(z \in \mathbb{N}\). For all \(x\) and \(z\), \(G(x, z)\) is the least natural number \(m\) such that \(m \ne G(x', z)\) for every \(x'\) obtained from \(x\) by replacing one coordinate \(x_i\) with some \(u < x_i\), and \(m \ne G(x^{(w)}, w)\) for every \(w < z\), where \(x^{(w)}_t = \min(x_t, f_t(w))\) for all \(t\).

public theorem chocolateBarGrundy_eq {s : ℕ} (f : Fin s → ℕ → ℕ) (x : Fin s → ℕ) (z : ℕ) :
    chocolateBarGrundy f x z =
      sInf {m | (∀ i u, u < x i → chocolateBarGrundy f (Function.update x i u) z ≠ m) ∧
        ∀ w, w < z → chocolateBarGrundy f (fun t ↦ min (x t) (f t w)) w ≠ m}
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definitions 9 and 10.
Uses 1 · Used by 1
Statement usesGrundy number of a chocolate bar
Used byThe single bitter square has Grundy number zero

TheoremThe single bitter square has Grundy number zero#✓fully proved

For all functions \(f_1, \dots, f_s : \mathbb{N} \to \mathbb{N}\), the chocolate bar \(\mathrm{CB}(f_1, \dots, f_s, 0, \dots, 0, 0)\), whose coordinates and width are all \(0\), has Grundy number \(0\): it is a single bitter square and has no move.

public theorem chocolateBarGrundy_zero {s : ℕ} (f : Fin s → ℕ → ℕ) :
    chocolateBarGrundy f (fun _ ↦ 0) 0 = 0
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definitions 9 and 10.
Uses 2
Statement usesGrundy number of a chocolate bar
Proof usesMex recursion for the Grundy number of a chocolate bar

DefinitionGrundy number of a chocolate bar with a height function#✓fully proved

Let \(s \in \mathbb{N}\) and \(F : \mathbb{N}^s \to \mathbb{N}\). The \((s + 1)\)-dimensional chocolate bar \(\mathrm{CB}(F, x_1, \dots, x_s, y)\) has, at each \(u = (u_1, \dots, u_s)\) with \(u_t \le x_t\) for all \(t\), a column of height \(\min(F(u), y) + 1\). A move either lowers one coordinate \(x_i\) to some \(a < x_i\), which clamps the height to \(\min(F(x'), y)\) for the new position \(x'\), or lowers the height \(y\) to some \(v < y\). The Grundy number of \(\mathrm{CB}(F, x_1, \dots, x_s, y)\) is the mex (least natural number not attained) of the Grundy numbers of the positions reachable in one move. It is defined for all \(x \in \mathbb{N}^s\) and \(y \in \mathbb{N}\); the bars themselves are the positions with \(y \le F(x)\).

MetaMathlibExt.heightChocolateBarGrundy · 15 lines 
public noncomputable def heightChocolateBarGrundy {s : ℕ} (F : (Fin s → ℕ) → ℕ)
    (x : Fin s → ℕ) (y : ℕ) : ℕ :=
  sInf {m | (∀ i u, u < x i → heightChocolateBarGrundy F (Function.update x i u)
      (min (F (Function.update x i u)) y) ≠ m) ∧
    ∀ v, v < y → heightChocolateBarGrundy F x v ≠ m}
termination_by (∑ t, x t) + y
decreasing_by
  · have hlt : ∑ t, Function.update x i u t < ∑ t, x t := by
      refine Finset.sum_lt_sum (fun j _ ↦ ?_) ⟨i, Finset.mem_univ _, by simpa⟩
      by_cases hj : j = i
      · subst hj; simp only [Function.update_self]; omega
      · simp [Function.update_of_ne hj]
    have := min_le_right (F (Function.update x i u)) y
    omega
  · omega
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definitions 15, 16 and 17 (and Definition 13 with second function 0).
Used by 6
Used byP-positions of a three-dimensional chocolate bar with floor-quotient height · Mex recursion for chocolate bars with a height function · The single bitter cube has Grundy number zero · Height-one chocolate bars with nim-sum Grundy numbers · Nim with a restricted pass · NS property of sections and the three-dimensional chocolate bar

TheoremMex recursion for chocolate bars with a height function#✓fully proved

Let \(s \in \mathbb{N}\) and \(F : \mathbb{N}^s \to \mathbb{N}\), and write \(G(x, y)\) for the Grundy number of the chocolate bar \(\mathrm{CB}(F, x_1, \dots, x_s, y)\). For all \(x \in \mathbb{N}^s\) and \(y \in \mathbb{N}\), \(G(x, y)\) is the least natural number \(m\) such that \(m \ne G(x', \min(F(x'), y))\) for every \(x'\) obtained from \(x\) by lowering one coordinate \(x_i\) to some \(u < x_i\), and \(m \ne G(x, v)\) for every \(v < y\).

public theorem heightChocolateBarGrundy_eq {s : ℕ} (F : (Fin s → ℕ) → ℕ) (x : Fin s → ℕ)
    (y : ℕ) :
    heightChocolateBarGrundy F x y =
      sInf {m | (∀ i u, u < x i → heightChocolateBarGrundy F (Function.update x i u)
          (min (F (Function.update x i u)) y) ≠ m) ∧
        ∀ v, v < y → heightChocolateBarGrundy F x v ≠ m}
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definition 17.
Uses 1 · Used by 1
Statement usesGrundy number of a chocolate bar with a height function
Used byThe single bitter cube has Grundy number zero

TheoremThe single bitter cube has Grundy number zero#✓fully proved

For every \(s \in \mathbb{N}\) and every \(F : \mathbb{N}^s \to \mathbb{N}\), the chocolate bar \(\mathrm{CB}(F, 0, \dots, 0, 0)\) has no move, so its Grundy number is \(0\).

public theorem heightChocolateBarGrundy_zero {s : ℕ} (F : (Fin s → ℕ) → ℕ) :
    heightChocolateBarGrundy F (fun _ ↦ 0) 0 = 0
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Definition 17.
Uses 2
Statement usesGrundy number of a chocolate bar with a height function
Proof usesMex recursion for chocolate bars with a height function

DefinitionPass indicator of Nim with a restricted pass#✓fully proved

For \(s\) piles with thresholds \(m_0, \dots, m_{s-1}\) and pile sizes \(x_0, \dots, x_{s-1}\) (natural numbers), the pass indicator is \(1\) if \(m_j \le x_j\) for some pile \(j\) (the pass may be used), and \(0\) if \(x_j < m_j\) for every pile \(j\).

public def nimPassIndicator {s : ℕ} (m x : Fin s → ℕ) : ℕ :=
  if ∃ j, m j ≤ x j then 1 else 0
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 10 and Corollary 2 (the function F).
Used by 4
Used byNim with a restricted pass · The Nim pass indicator is at most one · Sections of the Nim pass indicator with the NS property · The pass is unavailable from the empty position

TheoremThe Nim pass indicator is at most one#✓fully proved

For every \(s \in \mathbb{N}\) and all \(m, x \in \mathbb{N}^s\), the pass indicator of \(m\) at \(x\) is at most \(1\); that is, it takes values in \(\{0, 1\}\).

public theorem nimPassIndicator_le_one {s : ℕ} (m x : Fin s → ℕ) : nimPassIndicator m x ≤ 1
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 10 (the function F).
Uses 1
Statement usesPass indicator of Nim with a restricted pass

TheoremThe pass is unavailable from the empty position#✓fully proved

Let \(s \in \mathbb{N}\) and \(m \in \mathbb{N}^s\) with \(m_i > 0\) for every \(i < s\). Then the pass indicator of \(m\) takes the value \(0\) at the zero tuple \((0, \dots, 0)\).

public theorem nimPassIndicator_zero {s : ℕ} {m : Fin s → ℕ} (hm : ∀ i, 0 < m i) :
    nimPassIndicator m (fun _ ↦ 0) = 0
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 10 (the function F).
Uses 1
Statement usesPass indicator of Nim with a restricted pass

TheoremNim-sum sets under clamping by functions with the NS property#●ready to prove

Let \(m \in \mathbb{N}\), let \(f_0, \dots, f_{m-1} : \mathbb{N} \to \mathbb{N}\) have the NS property, and let \(x_0, \dots, x_{m-1}, z \in \mathbb{N}\) satisfy \(x_t \le f_t(z)\) for every \(t < m\). Then

\[ \{x_0 \oplus \cdots \oplus x_{m-1} \oplus w : w < z\} = \{\min(x_0, f_0(w)) \oplus \cdots \oplus \min(x_{m-1}, f_{m-1}(w)) \oplus w : w < z\}, \]

where \(\oplus\) denotes nim-sum (bitwise exclusive or).

The printed left-hand nim-sum carries a stray index \(j \ne i\) with \(i\) unbound; it is read as the full nim-sum, as in Lemma 5 (the case of two functions), which the proof generalises.

public theorem_wanted image_foldl_xor_eq_image_min {m : ℕ} {f : Fin m → ℕ → ℕ}
    (hf : ∀ t, HasNSProperty (f t)) {x : Fin m → ℕ} {z : ℕ} (hx : ∀ t, x t ≤ f t z) :
    {c | ∃ w < z, c = (List.ofFn x).foldl (· ^^^ ·) 0 ^^^ w} =
      {c | ∃ w < z, c = (List.ofFn fun t ↦ min (x t) (f t w)).foldl (· ^^^ ·) 0 ^^^ w}
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 6.
Uses 1
Statement usesNS property

TheoremThe NS property characterises nim-sum Grundy numbers of two-dimensional chocolate bars#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) be monotone. Then \(f\) has the NS property if and only if, for all \(x, z \in \mathbb{N}\) with \(x \le f(z)\), the chocolate bar \(\mathrm{CB}(f, 0, x, 0, z)\) of width \(z\) (first function \(f\), first coordinate \(x\), second function constantly \(0\), second coordinate \(0\)) has Grundy number \(x \oplus z\), where \(\oplus\) denotes nim-sum (bitwise exclusive or).

public theorem_wanted hasNSProperty_iff_chocolateBarGrundy_depth_zero {f : ℕ → ℕ}
    (hf : Monotone f) :
    HasNSProperty f ↔
      ∀ x z, x ≤ f z → chocolateBarGrundy ![f, fun _ ↦ 0] ![x, 0] z = x ^^^ z
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Theorem 2.
Uses 2
Statement usesNS property · Grundy number of a chocolate bar

TheoremNS property of sections and the three-dimensional chocolate bar#●ready to prove

Let \(F : \mathbb{N} \times \mathbb{N} \to \mathbb{N}\) be monotone for the componentwise order. Then the sections \(x \mapsto F(n, x)\) and \(w \mapsto F(w, n)\) have the NS property for every \(n \in \mathbb{N}\) if and only if, for all natural numbers \(w\), \(x\), \(y\) with \(y \le F(w, x)\), the Grundy number of the chocolate bar \(\mathrm{CB}(F, w, x, y)\), whose column at \((u, v)\) (with \(u \le w\), \(v \le x\)) has height \(\min(F(u, v), y) + 1\), equals the nim-sum \(w \oplus x \oplus y\) (bitwise exclusive or).

public theorem_wanted sections_hasNSProperty_iff_heightChocolateBarGrundy_eq_xor
    {F : ℕ → ℕ → ℕ} (hF : Monotone fun p : ℕ × ℕ ↦ F p.1 p.2) :
    ((∀ n, HasNSProperty (F n)) ∧ ∀ n, HasNSProperty fun w ↦ F w n) ↔
      ∀ w x y, y ≤ F w x →
        heightChocolateBarGrundy (fun v ↦ F (v 0) (v 1)) ![w, x] y = w ^^^ x ^^^ y
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Theorem 3.
Uses 2
Statement usesNS property · Grundy number of a chocolate bar with a height function

TheoremNim-sum Grundy numbers of chocolate bars with two functions#●ready to prove

Let \(g, h : \mathbb{N} \to \mathbb{N}\) be monotone. Then \(g\) and \(h\) both have the NS property if and only if, for all natural numbers \(x, y, z\) with \(x \le g(z)\) and \(y \le h(z)\), the Grundy number of the chocolate bar \(\mathrm{CB}(g, h, x, y, z)\) equals \(x \oplus y \oplus z\), where \(\oplus\) is nim-sum (bitwise exclusive or).

public theorem_wanted hasNSProperty_and_iff_chocolateBarGrundy_eq_xor {g h : ℕ → ℕ}
    (hg : Monotone g) (hh : Monotone h) :
    HasNSProperty g ∧ HasNSProperty h ↔
      ∀ x y z, x ≤ g z → y ≤ h z → chocolateBarGrundy ![g, h] ![x, y] z = x ^^^ y ^^^ z
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Theorem 4.
Uses 2
Statement usesNS property · Grundy number of a chocolate bar

TheoremNim-sum Grundy numbers of chocolate bars with four functions#●ready to prove

Let \(f_1, f_2, f_3, f_4 : \mathbb{N} \to \mathbb{N}\) be monotone. Then all four have the NS property if and only if, for all natural numbers \(x_1, x_2, x_3, x_4, z\) with \(x_t \le f_t(z)\) for every \(t\), the Grundy number of the chocolate bar \(\mathrm{CB}(f_1, f_2, f_3, f_4, x_1, x_2, x_3, x_4, z)\) equals \(x_1 \oplus x_2 \oplus x_3 \oplus x_4 \oplus z\), where \(\oplus\) is nim-sum (bitwise exclusive or).

public theorem_wanted forall_hasNSProperty_iff_chocolateBarGrundy_eq_xor_four
    {f : Fin 4 → ℕ → ℕ} (hf : ∀ t, Monotone (f t)) :
    (∀ t, HasNSProperty (f t)) ↔
      ∀ (x : Fin 4 → ℕ) z, (∀ t, x t ≤ f t z) →
        chocolateBarGrundy f x z = x 0 ^^^ x 1 ^^^ x 2 ^^^ x 3 ^^^ z
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Theorem 5.
Uses 2
Statement usesNS property · Grundy number of a chocolate bar

TheoremP-positions of a three-dimensional chocolate bar with floor-quotient height#●ready to prove

Let \(k\) be a natural number with \(k \equiv 3 \pmod 4\), and let \(F(w, x) = \lfloor (w + x) / k \rfloor\). For all \(w, x, y \in \mathbb{N}\) with \(y \le F(w, x)\), the three-dimensional chocolate bar \(\mathrm{CB}(F, w, x, y)\) has Grundy number \(0\) (is a P-position) if and only if \(w \oplus x \oplus y = 0\), where \(\oplus\) denotes nim-sum (bitwise exclusive or).

public theorem_wanted heightChocolateBarGrundy_add_div_eq_zero_iff {k : ℕ} (hk : k % 4 = 3)
    {w x y : ℕ} (hy : y ≤ (w + x) / k) :
    heightChocolateBarGrundy (fun v ↦ (v 0 + v 1) / k) ![w, x] y = 0 ↔ w ^^^ x ^^^ y = 0
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Theorem 8.
Uses 1
Statement usesGrundy number of a chocolate bar with a height function

TheoremHeight-one chocolate bars with nim-sum Grundy numbers#●ready to prove

Let \(s \in \mathbb{N}\) and let \(F : \mathbb{N}^s \to \mathbb{N}\) be monotone for the coordinatewise order, with \(F(x) \le 1\) for all \(x\). For \(x \in \mathbb{N}^s\), \(i < s\) and \(t \in \mathbb{N}\) write \(x[i \mapsto t]\) for \(x\) with its \(i\)-th coordinate replaced by \(t\), and suppose that for all \(x\) and \(i\) there is a \(t\) with \(F(x[i \mapsto t]) = 1\). Write \(\oplus\) for nim-sum. Then the following are equivalent: (a) for all \(x \in \mathbb{N}^s\) and \(i < s\) there is an even \(m \in \mathbb{N}\) (depending on \(x\) and \(i\)) such that \(F(x[i \mapsto t]) = 1\) for \(t \ge m\) and \(F(x[i \mapsto t]) = 0\) for \(t < m\); (b) for all \(x \in \mathbb{N}^s\) and \(y \in \mathbb{N}\) with \(y \le F(x)\), the Grundy number of the chocolate bar \(\mathrm{CB}(F, x_0, \dots, x_{s-1}, y)\) is \(x_0 \oplus \cdots \oplus x_{s-1} \oplus y\).

The hypothesis that every section takes the value \(1\) is that of Lemma 9, from which the corollary is derived.

public theorem_wanted indicator_sections_iff_heightChocolateBarGrundy_eq_xor {s : ℕ}
    {F : (Fin s → ℕ) → ℕ} (hF : Monotone F) (hle : ∀ x, F x ≤ 1)
    (hone : ∀ (x : Fin s → ℕ) i, ∃ t, F (Function.update x i t) = 1) :
    (∀ (x : Fin s → ℕ) i, ∃ m, Even m ∧
        (fun t ↦ F (Function.update x i t)) = (Set.Ici m).indicator 1) ↔
      ∀ x y, y ≤ F x → heightChocolateBarGrundy F x y = (List.ofFn x).foldl (· ^^^ ·) 0 ^^^ y
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Corollary 1.
Uses 1
Statement usesGrundy number of a chocolate bar with a height function

TheoremSections of the Nim pass indicator with the NS property#●ready to prove

Let \(s \in \mathbb{N}\) and \(m \in \mathbb{N}^s\) with \(m_i > 0\) for every \(i < s\), and let \(F : \mathbb{N}^s \to \mathbb{N}\) be the pass indicator of \(m\): \(F(x) = 1\) if \(m_j \le x_j\) for some \(j\), and \(F(x) = 0\) otherwise. For \(x \in \mathbb{N}^s\), \(i < s\) and \(t \in \mathbb{N}\) write \(x[i \mapsto t]\) for \(x\) with its \(i\)-th coordinate replaced by \(t\). Then the following are equivalent: (a) for all \(x \in \mathbb{N}^s\) and \(i < s\), the function \(t \mapsto F(x[i \mapsto t])\) has the NS property; (b) \(m_i\) is even for every \(i < s\).

public theorem_wanted nimPassIndicator_sections_hasNSProperty_iff {s : ℕ} {m : Fin s → ℕ}
    (hm : ∀ i, 0 < m i) :
    (∀ (x : Fin s → ℕ) i, HasNSProperty fun t ↦ nimPassIndicator m (Function.update x i t)) ↔
      ∀ i, Even (m i)
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Lemma 10.
Uses 2
Statement usesNS property · Pass indicator of Nim with a restricted pass

TheoremNim with a restricted pass#●ready to prove

Let \(s \in \mathbb{N}\) and \(m \in \mathbb{N}^s\) with \(m_i > 0\) for every \(i < s\), and let \(F : \mathbb{N}^s \to \mathbb{N}\) be the pass indicator of \(m\): \(F(x) = 1\) if \(m_j \le x_j\) for some \(j\), and \(F(x) = 0\) otherwise. Write \(\oplus\) for nim-sum. Then the following are equivalent: (a) for all \(x \in \mathbb{N}^s\) and \(p \in \mathbb{N}\) with \(p \le F(x)\), the Grundy number of the chocolate bar \(\mathrm{CB}(F, x_0, \dots, x_{s-1}, p)\) is \(x_0 \oplus \cdots \oplus x_{s-1} \oplus p\); (b) \(m_i\) is even for every \(i < s\).

The bar is Nim on \(s\) piles with a one-time pass usable only while \(F(x) = 1\): removing stones from a pile, reaching \(x'\), replaces \(p\) by \(\min(F(x'), p)\), and the pass lowers \(p\) from \(1\) to \(0\).

public theorem_wanted nimPassGrundy_eq_xor_iff {s : ℕ} {m : Fin s → ℕ} (hm : ∀ i, 0 < m i) :
    (∀ (x : Fin s → ℕ) p, p ≤ nimPassIndicator m x →
        heightChocolateBarGrundy (nimPassIndicator m) x p =
          (List.ofFn x).foldl (· ^^^ ·) 0 ^^^ p) ↔
      ∀ i, Even (m i)
Sources
  • Ryohei Miyadera, Hikaru Manabe and Aditi Singh, Generalizations of Two-Dimensional and Three-Dimensional Chocolate Bar Games, INTEGERS 25 (2025), Article G3, Corollary 2.
Uses 2
Statement usesGrundy number of a chocolate bar with a height function · Pass indicator of Nim with a restricted pass
12 fully proved21 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.