Maximum Nim

DefinitionMinimum excludant of a finite set#✓fully proved

For a finite set \(s\) of natural numbers, \(\operatorname{mex}(s)\) is the least natural number that does not belong to \(s\).

public def maximumNimMex (s : Finset ℕ) : ℕ :=
  Nat.find (show ∃ m, m ∉ s by
    let M := (insert 0 s).max' (by simp)
    refine ⟨M + 1, ?_⟩
    intro h
    have hle : M + 1 ≤ M := Finset.le_max' (insert 0 s) (M + 1) (by simp [h])
    omega)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Used by 6

Used byGrundy numbers of Maximum Nim · Grundy number of a pile of five in halving Maximum Nim · Grundy number of a pile of four in halving Maximum Nim · Grundy number of a pile of three in halving Maximum Nim · Recursive formula for Maximum Nim Grundy numbers · Characterization of the minimum excludant

TheoremCharacterization of the minimum excludant#✓fully proved

Let \(s\) be a finite set of natural numbers and \(m\) a natural number. Then \(\operatorname{mex}(s)\), the least natural number not in \(s\), equals \(m\) if and only if \(m \notin s\) and every natural number \(n < m\) lies in \(s\).

public theorem maximumNimMex_eq_iff (s : Finset ℕ) (m : ℕ) :
    maximumNimMex s = m ↔ m ∉ s ∧ ∀ n < m, n ∈ s

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Uses 1 · Used by 3

Statement usesMinimum excludant of a finite set

Used byGrundy number of a pile of five in halving Maximum Nim · Grundy number of a pile of four in halving Maximum Nim · Grundy number of a pile of three in halving Maximum Nim

DefinitionGrundy numbers of Maximum Nim#✓fully proved

For a rule function \(f : \mathbb{N} \to \mathbb{N}\), the Grundy number \(G_f(x)\) of a pile of \(x\) stones in Maximum Nim is defined by recursion on \(x\) as the mex (least natural number not in the set) of \(\{G_f(x - u) : 1 \le u \le \min(f(x), x)\}\), the Grundy numbers of the positions reachable from \(x\) by removing \(u\) stones.

Taking \(\min(f(x), x)\) makes the definition total; under the source's hypotheses on \(f\), which include \(f(0) = 0\), it does not change the legal moves.

public def maximumNimGrundy (f : ℕ → ℕ) (x : ℕ) : ℕ :=
  maximumNimMex <|
    (Finset.Icc 1 (min (f x) x)).attach.image fun u =>
      maximumNimGrundy f (x - u.1)
termination_by x
decreasing_by
  have hu := u.property
  simp only [Finset.mem_Icc] at hu
  omega

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Uses 1 · Used by 15

Statement usesMinimum excludant of a finite set

Used byJosephus elimination positions as Maximum Nim Grundy numbers · Maximum Nim Grundy numbers at multiples of the divisor · Grundy number of a pile of five in halving Maximum Nim · Grundy number of a pile of four in halving Maximum Nim · Grundy number of a pile of three in halving Maximum Nim · Recursive formula for Maximum Nim Grundy numbers · Maximum Nim Grundy numbers at non-multiples of the divisor · Grundy number where the rule function increases · Grundy number where the rule function is flat · Grundy value zero characterizes P-positions in Maximum Nim · Floor-rule Maximum Nim: Grundy reduction when \(n = kt + u\) · Floor-rule Maximum Nim: one-step Grundy reduction when k = nt + h · Floor-rule Maximum Nim: t-step Grundy reduction when k = nt + h · Floor-rule Maximum Nim: (t+1)-step Grundy reduction when k = nt + h · Floor-rule Maximum Nim: positions below k have Grundy number zero

TheoremRecursive formula for Maximum Nim Grundy numbers#✓fully proved

For every rule function \(f : \mathbb{N} \to \mathbb{N}\) and every pile size \(x \in \mathbb{N}\), the Grundy number \(G_f(x)\) of a pile of \(x\) stones in Maximum Nim with rule function \(f\) equals the mex (least natural number not in the set) of \(\{G_f(x - u) : 1 \le u \le \min(f(x), x)\}\).

public theorem maximumNimGrundy_eq (f : ℕ → ℕ) (x : ℕ) :
    maximumNimGrundy f x =
      maximumNimMex ((Finset.Icc 1 (min (f x) x)).attach.image fun u =>
        maximumNimGrundy f (x - u.1))

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Uses 2

Statement usesGrundy numbers of Maximum Nim · Minimum excludant of a finite set

TheoremGrundy number of a pile of five in halving Maximum Nim#✓fully proved

In Maximum Nim with rule function \(f(x) = \lfloor x/2 \rfloor\), a pile of \(5\) stones has Grundy number \(1\).

public theorem maximumNimGrundy_div_two_five : maximumNimGrundy (· / 2) 5 = 1

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (characteristic values).

Uses 3

Statement usesGrundy numbers of Maximum Nim

Proof usesMinimum excludant of a finite set · Characterization of the minimum excludant

TheoremGrundy number of a pile of four in halving Maximum Nim#✓fully proved

In Maximum Nim with rule function \(f(x) = \lfloor x/2 \rfloor\), a pile of \(4\) stones has Grundy number \(2\).

public theorem maximumNimGrundy_div_two_four : maximumNimGrundy (· / 2) 4 = 2

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (characteristic values).

Uses 3

Statement usesGrundy numbers of Maximum Nim

Proof usesMinimum excludant of a finite set · Characterization of the minimum excludant

TheoremGrundy number of a pile of three in halving Maximum Nim#✓fully proved

In Maximum Nim with rule function \(f(x) = \lfloor x/2 \rfloor\), a pile of \(3\) stones has Grundy number \(0\).

public theorem maximumNimGrundy_div_two_three : maximumNimGrundy (· / 2) 3 = 0

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (characteristic values).

Uses 3

Statement usesGrundy numbers of Maximum Nim

Proof usesMinimum excludant of a finite set · Characterization of the minimum excludant

DefinitionThe Maximum Nim game#✓fully proved

For a rule function \(f : \mathbb{N} \to \mathbb{N}\), the Maximum Nim game with rule \(f\) is the impartial game whose positions are the pile sizes \(x \in \mathbb{N}\), in which the moves from \(x\) go to \(x - u\) for each \(u\) with \(1 \le u \le \min(f(x), x)\). The rank of a position is the pile size itself, and the starting position is the empty pile \(0\).

public def maximumNimGame (f : ℕ → ℕ) : SpragueGrundy.ImpartialGame where
  Pos := ℕ
  eqDec := inferInstance
  moves := fun x => (Finset.Icc 1 (min (f x) x)).image (fun u => x - u)
  rank := id
  rank_lt := by
    intro x y h
    simp only [Finset.mem_image, Finset.mem_Icc] at h
    obtain ⟨u, ⟨h1, h2⟩, rfl⟩ := h
    simp only [id_eq]
    omega
  start := 0

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Uses 1 · Used by 2

Statement usesImpartial game

Used byP-positions of Maximum Nim · Grundy value zero characterizes P-positions in Maximum Nim

TheoremP-positions of Maximum Nim#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) be a rule function and let \(x\) be a pile size. The position \(x\) of the Maximum Nim game with rule \(f\) is a P-position if and only if, for every \(u\) with \(1 \le u \le \min(f(x), x)\), the position \(x - u\) is not a P-position.

public theorem maximumNimGame_isP_iff (f : ℕ → ℕ) (x : ℕ) :
    SpragueGrundy.IsP (maximumNimGame f) x ↔
      ∀ u, 1 ≤ u → u ≤ min (f x) x → ¬SpragueGrundy.IsP (maximumNimGame f) (x - u)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 2.

Uses 4

Statement usesP-positions · The Maximum Nim game

Proof usesImpartial game · Recursive characterization of P-positions

DefinitionThe Maximum Nim map \(h_k\)#✓fully proved

For natural numbers \(k\) and \(x\), let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\). The paper takes \(k \ge 2\); for \(k \le 1\) the definition gives \(h_k(x) = x + 1\), because \(k - 1\) is truncated to \(0\) and \(\lfloor x/0 \rfloor\) is taken to be \(0\).

public def maximumNimH (k x : ℕ) : ℕ := x + x / (k - 1) + 1

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Definition 3.1.

Used by 10

Used byJosephus survivor via iteration from zero · Josephus survivor via the shifted iteration · Logarithmic bounds for the Josephus iteration count · Linear bounds on h_k and their iterates · Logarithmic bounds on the iterates of h_k · Iterates of the Maximum Nim map \(h_k\) tend to infinity · The Maximum Nim map \(h_k\) is strictly increasing · The Maximum Nim map \(h_k\) exceeds its argument · The value \(h_3(2) = 4\) of the Maximum Nim map · The value \(h_3(0) = 1\) of the Maximum Nim map

TheoremThe value \(h_3(0) = 1\) of the Maximum Nim map#✓fully proved

For the map \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) on the natural numbers, we have \(h_3(0) = 1\).

public theorem maximumNimH_three_zero : maximumNimH 3 0 = 1

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Definition 3.1.

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremThe value \(h_3(2) = 4\) of the Maximum Nim map#✓fully proved

For the map \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) on the natural numbers, we have \(h_3(2) = 4\).

public theorem maximumNimH_three_two : maximumNimH 3 2 = 4

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Definition 3.1.

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

DefinitionFuel-bounded Josephus simulation#✓fully proved

For natural numbers \(k\) and \(s\) (the starting position), a fuel \(f\) and a list \(c\) of natural numbers (the current circle), the simulation returns the empty list when \(f = 0\) or \(c\) is empty. Otherwise, with \(L\) the length of \(c\) and \(i = (s + k - 1) \bmod L\), where the subtraction is truncated at \(0\), it returns the entry of \(c\) at zero-based position \(i\) followed by the result of the simulation with the same \(k\), starting position \(i\) and fuel \(f - 1\) on the list obtained from \(c\) by deleting the entry at position \(i\).

public def josephusEliminationOrderAux (k start : ℕ) : ℕ → List ℕ → List ℕ
  | 0, _ => []
  | _ + 1, [] => []
  | fuel + 1, circle =>
      let i := (start + k - 1) % circle.length
      circle.getD i 0 :: josephusEliminationOrderAux k i fuel (circle.eraseIdx i)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem).

Used by 4

Used byJosephus elimination order · The survivor is the last entry of the Josephus elimination order · Length of the Josephus elimination order · The Josephus elimination order is a permutation of the circle

DefinitionJosephus elimination order#✓fully proved

For natural numbers \(k\) and \(n\), place \(1, \dots, n\) in order on a circle and repeatedly remove one entry. When \(L\) entries remain and the current position is \(s\) (zero-based, initially \(s = 0\)), the entry at zero-based position \(i = (s + k - 1) \bmod L\) is removed, where the subtraction is truncated at \(0\), and \(i\) becomes the current position, so the next count starts at the entry after the removed one. The Josephus elimination order with step \(k\) on the circle \(1, \dots, n\) is the list of all \(n\) entries in the order of their removal.

For \(k \ge 1\) this is the classical process that removes every \(k\)-th remaining entry; the last entry of the list is the survivor.

public def josephusEliminationOrder (k n : ℕ) : List ℕ :=
  josephusEliminationOrderAux k 0 n (List.range' 1 n)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem).

Uses 1 · Used by 6

Statement usesFuel-bounded Josephus simulation

Used byThe survivor is the last entry of the Josephus elimination order · Length of the Josephus elimination order · The Josephus elimination order is a permutation of the circle · Josephus elimination order for ten people and step three · Josephus elimination order for three people and step two · Josephus elimination positions as Maximum Nim Grundy numbers

TheoremJosephus elimination order for ten people and step three#✓fully proved

The Josephus elimination order with step \(3\) on the circle \(1, \dots, 10\) is \(3, 6, 9, 2, 7, 1, 8, 5, 10, 4\): the entries are removed in the order \(3, 6, 9, 2, 7, 1, 8, 5, 10\), and the survivor \(4\) comes last.

public theorem josephusEliminationOrder_three_ten :
    josephusEliminationOrder 3 10 = [3, 6, 9, 2, 7, 1, 8, 5, 10, 4]

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem example).

Uses 1

Statement usesJosephus elimination order

TheoremJosephus elimination order for three people and step two#✓fully proved

The Josephus elimination order with step \(2\) on the circle \(1, 2, 3\) is \(2, 1, 3\): the entry \(2\) is removed first, then the entry \(1\), and the survivor \(3\) comes last.

public theorem josephusEliminationOrder_two_three :
    josephusEliminationOrder 2 3 = [2, 1, 3]

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (characteristic values).

Uses 1

Statement usesJosephus elimination order

TheoremLength of the Josephus elimination order#✓fully proved

For all natural numbers \(k\) and \(n\), the Josephus elimination order with step \(k\) on the circle \(1, \dots, n\) has exactly \(n\) entries.

public theorem josephusEliminationOrder_length (k n : ℕ) :
    (josephusEliminationOrder k n).length = n

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem).

Uses 2

Statement usesJosephus elimination order

Proof usesFuel-bounded Josephus simulation

TheoremThe Josephus elimination order is a permutation of the circle#✓fully proved

For all natural numbers \(k\) and \(n\), the Josephus elimination order with step \(k\) on the circle \(1, \dots, n\) is a permutation of the list \(1, 2, \dots, n\); in particular, each of \(1, \dots, n\) occurs in it exactly once.

public theorem josephusEliminationOrder_perm (k n : ℕ) :
    List.Perm (josephusEliminationOrder k n) (List.range' 1 n)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem).

Uses 2

Statement usesJosephus elimination order

Proof usesFuel-bounded Josephus simulation

TheoremThe survivor is the last entry of the Josephus elimination order#✓fully proved

For natural numbers \(k \ge 1\) and \(n \ge 1\), the Josephus elimination order with step \(k\) on the circle \(1, \dots, n\) is nonempty and its last entry is \(J_k(n)\), the value at \(n\) of the Josephus function for elimination step \(k\).

public theorem josephusEliminationOrder_getLast? (k n : ℕ) (hk : 1 ≤ k) (hn : 1 ≤ n) :
    (josephusEliminationOrder k n).getLast? = some (josephus k n)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Section 3 (Josephus problem).

Uses 3

Statement usesJosephus survivor function · Josephus elimination order

Proof usesFuel-bounded Josephus simulation

TheoremGrundy value zero characterizes P-positions in Maximum Nim#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(0) = 0\) and \(f(m-1) \le f(m) \le f(m-1) + 1\) for every \(m \ge 1\). Then for every pile size \(x \in \mathbb{N}\), the Grundy number of \(x\) in Maximum Nim with rule function \(f\) is \(0\) if and only if \(x\) is a P-position (a previous-player win under normal play) of that game.

public theorem_wanted maximumNimGrundy_eq_zero_iff_isP (f : ℕ → ℕ) (hf0 : f 0 = 0)
    (hf : ∀ m, 1 ≤ m → f (m - 1) ≤ f m ∧ f m ≤ f (m - 1) + 1) (x : ℕ) :
    maximumNimGrundy f x = 0 ↔ SpragueGrundy.IsP (maximumNimGame f) x

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Theorem 1.

Uses 3

Statement usesP-positions · The Maximum Nim game · Grundy numbers of Maximum Nim

TheoremGrundy number where the rule function increases#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(0) = 0\) and \(f(m-1) \le f(m) \le f(m-1) + 1\) for every \(m \ge 1\), and let \(G\) be the Grundy number of Maximum Nim with rule function \(f\). If \(x \ge 1\) and \(f(x-1) < f(x)\), then \(G(x) = f(x)\).

public theorem_wanted maximumNimGrundy_eq_rule_of_lt (f : ℕ → ℕ) (hf0 : f 0 = 0)
    (hf : ∀ m, 1 ≤ m → f (m - 1) ≤ f m ∧ f m ≤ f (m - 1) + 1)
    (x : ℕ) (hx : 1 ≤ x) (hfx : f (x - 1) < f x) :
    maximumNimGrundy f x = f x

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 1(i).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremGrundy number where the rule function is flat#●ready to prove

Let \(f : \mathbb{N} \to \mathbb{N}\) satisfy \(f(0) = 0\) and \(f(m-1) \le f(m) \le f(m-1) + 1\) for every \(m \ge 1\), and let \(G\) be the Grundy number of Maximum Nim with rule function \(f\). If \(x \ge 1\) and \(f(x) = f(x-1)\), then \(G(x) = G(x - f(x) - 1)\).

Here \(x - f(x) - 1 \ge 0\), since the hypotheses give \(f(x) = f(x-1) \le x - 1\).

public theorem_wanted maximumNimGrundy_eq_sub_rule_succ (f : ℕ → ℕ) (hf0 : f 0 = 0)
    (hf : ∀ m, 1 ≤ m → f (m - 1) ≤ f m ∧ f m ≤ f (m - 1) + 1)
    (x : ℕ) (hx : 1 ≤ x) (hfx : f x = f (x - 1)) :
    maximumNimGrundy f x = maximumNimGrundy f (x - f x - 1)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 1(ii).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremFloor identity for non-multiples in Maximum Nim#●ready to prove

Let \(k \ge 2\) and \(x\) be natural numbers such that \(x\) is not a multiple of \(k\). Then \(x - \lfloor x/k \rfloor - 1 = \lfloor (k-1)x/k \rfloor\).

public theorem_wanted maximumNim_sub_div_sub_one_eq (k x : ℕ) (hk : 2 ≤ k)
    (hxk : ¬k ∣ x) :
    x - x / k - 1 = (k - 1) * x / k

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 2.

TheoremMaximum Nim Grundy numbers at multiples of the divisor#●ready to prove

Let \(k \ge 2\) and let \(G\) be the Grundy number of Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\). Every positive multiple \(x\) of \(k\) satisfies \(G(x) = x/k\).

public theorem_wanted maximumNimGrundy_div_eq_of_dvd (k x : ℕ) (hk : 2 ≤ k)
    (hx : 1 ≤ x) (hkx : k ∣ x) :
    maximumNimGrundy (· / k) x = x / k

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 3(i).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremMaximum Nim Grundy numbers at non-multiples of the divisor#●ready to prove

Let \(k \ge 2\) and let \(G\) be the Grundy number of Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\). If \(x\) is a natural number not divisible by \(k\), then \(G(x) = G(\lfloor (k-1)x/k \rfloor)\).

public theorem_wanted maximumNimGrundy_eq_F_of_not_dvd (k x : ℕ) (hk : 2 ≤ k)
     (hkx : ¬k ∣ x) :
    maximumNimGrundy (· / k) x = maximumNimGrundy (· / k) ((k - 1) * x / k)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 3(ii).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremFloor-rule Maximum Nim: positions below k have Grundy number zero#●ready to prove

For every natural number \(k \ge 2\) and every natural number \(j\) with \(1 \le j \le k\), a pile of \(k - j\) stones has Grundy number \(0\) in Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\).

public theorem_wanted maximumNimGrundy_sub_eq_zero (k j : ℕ) (hk : 2 ≤ k)
    (hj : 1 ≤ j) (hjk : j ≤ k) :
    maximumNimGrundy (· / k) (k - j) = 0

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 3(iii).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremA Maximum Nim non-divisibility lemma for \(s < t\)#●ready to prove

Let \(k, n, t, h, s, i\) be natural numbers with \(h \ge 1\), \(k = nt + h\), \(h \le n\) and \(s < t\). If \(1 \le i \le n\), then \(k\) does not divide \(n(k - s) - i\).

The hypotheses force \(n \ge 1\), \(s < k\) and \(i \le n(k - s)\), so both subtractions are ordinary differences of natural numbers.

public theorem_wanted maximumNim_not_dvd_mul_sub_of_lt (k n t h s i : ℕ)
    (hh : 1 ≤ h)
    (hdecomp : k = n * t + h) (hhn : h ≤ n) (hst : s < t)
    (hi : 1 ≤ i) (hin : i ≤ n) :
    ¬k ∣ n * (k - s) - i

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 4(i).

TheoremA Maximum Nim non-divisibility lemma for \(i \ne h\)#●ready to prove

Let \(k, n, t, h, i\) be natural numbers with \(t \ge 1\), \(h \ge 1\), \(k = nt + h\) and \(h \le n\). If \(1 \le i \le n\) and \(i \ne h\), then \(k\) does not divide \(n(k - t) - i\).

The hypotheses force \(n \ge 1\), \(t \le k\) and \(i \le n(k - t)\), so both subtractions are ordinary differences of natural numbers.

public theorem_wanted maximumNim_not_dvd_mul_sub_of_ne (k n t h i : ℕ)
    (ht : 1 ≤ t) (hh : 1 ≤ h)
    (hdecomp : k = n * t + h) (hhn : h ≤ n)
    (hi : 1 ≤ i) (hin : i ≤ n) (hih : i ≠ h) :
    ¬k ∣ n * (k - t) - i

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 4(ii).

TheoremFloor-rule Maximum Nim: Grundy reduction when \(n = kt + u\)#●ready to prove

Let \(k\), \(t\), \(u\) and \(n\) be natural numbers with \(k \ge 2\), \(t \ge 1\), \(u \le k - 1\) and \(n = kt + u\). Write \(G(x)\) for the Grundy number of a pile of \(x\) stones in Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\). Then for every natural number \(i\) with \(1 \le i \le n\) that is not divisible by \(k\),

\[G(nk - i) = G\bigl((n - t)k - (u + i - \lfloor i/k \rfloor)\bigr).\]

The hypotheses force \(i \le nk\) and \(u + i - \lfloor i/k \rfloor \le (n - t)k\), so all subtractions are ordinary differences of natural numbers. The right side is read with the parentheses shown; read without them, as in the extracted statement, the equality is false.

public theorem_wanted maximumNimGrundy_mul_sub_eq_decomposition (k n t u i : ℕ)
    (hk : 2 ≤ k) (ht : 1 ≤ t)
    (hdecomp : n = k * t + u) (huk : u ≤ k - 1)
    (hi : 1 ≤ i) (hin : i ≤ n) (hki : ¬k ∣ i) :
    maximumNimGrundy (· / k) (n * k - i) =
      maximumNimGrundy (· / k) ((n - t) * k - (u + i - i / k))

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 5(i).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremFloor-rule Maximum Nim: one-step Grundy reduction when k = nt + h#●ready to prove

Let \(n\), \(t\), \(h\) be natural numbers with \(t \ge 1\) and \(1 \le h \le n\), and let \(k = nt + h\). Write \(G(x)\) for the Grundy number of a pile of \(x\) stones in Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\), and let \(F(x) = \lfloor (k-1)x/k \rfloor\). Then for every natural number \(i\) with \(1 \le i \le n\),

\[G(nk - i) = G(F(nk - i)) = G(n(k - 1) - i).\]

public theorem_wanted maximumNimGrundy_mul_sub_eq_F_eq_pred (k n t h i : ℕ)
    (ht : 1 ≤ t) (hh : 1 ≤ h)
    (hdecomp : k = n * t + h) (hhn : h ≤ n) (hi : 1 ≤ i) (hin : i ≤ n) :
    maximumNimGrundy (· / k) (n * k - i) =
        maximumNimGrundy (· / k) ((k - 1) * (n * k - i) / k) ∧
      maximumNimGrundy (· / k) ((k - 1) * (n * k - i) / k) =
        maximumNimGrundy (· / k) (n * (k - 1) - i)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 5(ii.1).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremFloor-rule Maximum Nim: t-step Grundy reduction when k = nt + h#●ready to prove

Let \(n\), \(t\), \(h\) be natural numbers with \(t \ge 1\) and \(1 \le h \le n\), and let \(k = nt + h\). Write \(G(x)\) for the Grundy number of a pile of \(x\) stones in Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\), let \(F(x) = \lfloor (k-1)x/k \rfloor\), and let \(F^t\) be the \(t\)-fold iterate of \(F\). Then for every natural number \(i\) with \(1 \le i \le n\),

\[G(nk - i) = G(F^t(nk - i)) = G(n(k - t) - i).\]

public theorem_wanted maximumNimGrundy_mul_sub_eq_iterate_F (k n t h i : ℕ)
    (ht : 1 ≤ t) (hh : 1 ≤ h)
    (hdecomp : k = n * t + h) (hhn : h ≤ n) (hi : 1 ≤ i) (hin : i ≤ n) :
    let F := fun x => (k - 1) * x / k
    maximumNimGrundy (· / k) (n * k - i) =
        maximumNimGrundy (· / k) (Nat.iterate F t (n * k - i)) ∧
      maximumNimGrundy (· / k) (Nat.iterate F t (n * k - i)) =
        maximumNimGrundy (· / k) (n * (k - t) - i)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 5(ii.2).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremFloor-rule Maximum Nim: (t+1)-step Grundy reduction when k = nt + h#●ready to prove

Let \(n\), \(t\), \(h\) be natural numbers with \(t \ge 1\) and \(1 \le h \le n\), and let \(k = nt + h\). Write \(G(x)\) for the Grundy number of a pile of \(x\) stones in Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\), let \(F(x) = \lfloor (k-1)x/k \rfloor\), and let \(F^{t+1}\) be the \((t+1)\)-fold iterate of \(F\). Then for every natural number \(i\) with \(1 \le i \le h - 1\),

\[G(nk - i) = G(F^{t+1}(nk - i)) = G((n - 1)k - (n - h + i)).\]

public theorem_wanted maximumNimGrundy_mul_sub_eq_succ_iterate_F (k n t h i : ℕ)
    (ht : 1 ≤ t) (hh : 1 ≤ h)
    (hdecomp : k = n * t + h) (hhn : h ≤ n) (hi : 1 ≤ i) (hih : i ≤ h - 1) :
    let F := fun x => (k - 1) * x / k
    maximumNimGrundy (· / k) (n * k - i) =
        maximumNimGrundy (· / k) (Nat.iterate F (t + 1) (n * k - i)) ∧
      maximumNimGrundy (· / k) (Nat.iterate F (t + 1) (n * k - i)) =
        maximumNimGrundy (· / k) ((n - 1) * k - (n - h + i))

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 5(ii.3).

Uses 1

Statement usesGrundy numbers of Maximum Nim

TheoremThe Maximum Nim map \(h_k\) is strictly increasing#●ready to prove

Let \(k \ge 2\) be a natural number and let \(h_k\) be the map \(x \mapsto x + \lfloor x/(k-1) \rfloor + 1\) on the natural numbers. For all natural numbers \(x\) and \(x'\) with \(x < x'\), we have \(h_k(x) < h_k(x')\).

public theorem_wanted maximumNimH_strictMono (k x x' : ℕ) (hk : 2 ≤ k) (hxx' : x < x') :
    maximumNimH k x < maximumNimH k x'

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 6(i).

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremThe Maximum Nim map \(h_k\) exceeds its argument#●ready to prove

Let \(k \ge 2\) be a natural number and let \(h_k\) be the map \(x \mapsto x + \lfloor x/(k-1) \rfloor + 1\) on the natural numbers. Every natural number \(x\) satisfies \(x < x + 1 \le h_k(x)\).

public theorem_wanted maximumNimH_succ_le (k x : ℕ) (hk : 2 ≤ k) :
    x < x + 1 ∧ x + 1 ≤ maximumNimH k x

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 6(ii).

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremIterates of the Maximum Nim map \(h_k\) tend to infinity#●ready to prove

Let \(k \ge 2\) be a natural number and let \(h_k\) be the map \(x \mapsto x + \lfloor x/(k-1) \rfloor + 1\) on the natural numbers. For every natural number \(x_0\), the iterates \(h_k^p(x_0)\) tend to infinity as \(p \to \infty\).

public theorem_wanted maximumNimH_iterate_tendsto_atTop (k x₀ : ℕ) (hk : 2 ≤ k) :
    Filter.Tendsto (fun p => Nat.iterate (maximumNimH k) p x₀)
      Filter.atTop Filter.atTop

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 6(iii).

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremLinear bounds on h_k and their iterates#●ready to prove

Let \(k \ge 2\) be a natural number, let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) on natural numbers, and define the real maps \(h_k^-(x) = x + \frac{x}{k-1}\) and \(h_k^+(x) = x + \frac{x}{k-1} + 1\). Writing \(g^p\) for the \(p\)-fold iterate of a map \(g\), for all natural numbers \(p\) and \(x\): (i) \((h_k^-)^p(x) = \left(\frac{k}{k-1}\right)^p x\), (ii) \((h_k^+)^p(x) = \left(\frac{k}{k-1}\right)^p (x + k - 1) - (k - 1)\), and (iii) \(h_k^-(x) \le h_k(x) \le h_k^+(x)\).

public theorem_wanted maximumNimH_iterate_bounds (k : ℕ) (hk : 2 ≤ k) :
    let hMinus : ℝ → ℝ := fun x => x + x / ((k : ℝ) - 1)
    let hPlus : ℝ → ℝ := fun x => x + x / ((k : ℝ) - 1) + 1
    (∀ (p x : ℕ), Nat.iterate hMinus p x = ((k : ℝ) / (k - 1)) ^ p * x) ∧
    (∀ (p x : ℕ), Nat.iterate hPlus p x = ((k : ℝ) / (k - 1)) ^ p * (x + k - 1) - (k - 1)) ∧
    (∀ x : ℕ, hMinus x ≤ maximumNimH k x ∧ (maximumNimH k x : ℝ) ≤ hPlus x)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 7.

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremJosephus elimination positions as Maximum Nim Grundy numbers#●ready to prove

Let \(k \ge 2\) and \(1 \le m \le n\). Write \(o_n(m)\) for the position, counting from \(1\), at which \(m\) appears in the Josephus elimination order of the circle \(1, \dots, n\) in which every \(k\)-th person is removed and the survivor is listed last, and write \(G\) for the Grundy number of Maximum Nim with rule function \(f(y) = \lfloor y/k \rfloor\). Then \(n - o_n(m) = G(nk - m)\).

public theorem_wanted josephus_position_complement_eq_maximumNimGrundy (k n m : ℕ)
    (hk : 2 ≤ k) (hm : 1 ≤ m) (hmn : m ≤ n) :
    n - ((josephusEliminationOrder k n).idxOf m + 1) =
      maximumNimGrundy (· / k) (n * k - m)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Theorem 2.

Uses 2

Statement usesJosephus elimination order · Grundy numbers of Maximum Nim

TheoremJosephus survivor via iteration from zero#●ready to prove

Let \(k \ge 2\) and \(n \ge 1\) be natural numbers, let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) for natural numbers \(x\), and write \(h_k^p\) for the \(p\)-th iterate of \(h_k\). Then there is a natural number \(p \ge 1\) with \(h_k^{p-1}(0) < n(k-1) \le h_k^p(0)\) and \(J_k(n) = nk - h_k^p(0)\), where \(J_k\) is the Josephus function for elimination step \(k\).

public theorem_wanted josephus_eq_mul_sub_iterate_maximumNimH_zero (k n : ℕ)
    (hk : 2 ≤ k) (hn : 1 ≤ n) :
    ∃ p, 1 ≤ p ∧
      Nat.iterate (maximumNimH k) (p - 1) 0 < n * (k - 1) ∧
      n * (k - 1) ≤ Nat.iterate (maximumNimH k) p 0 ∧
      josephus k n = n * k - Nat.iterate (maximumNimH k) p 0

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Theorem 3.

Uses 2

Statement usesJosephus survivor function · The Maximum Nim map \(h_k\)

TheoremJosephus survivor via the shifted iteration#●ready to prove

Let \(k \ge 2\) and \(n \ge 2\) be natural numbers, let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) for natural numbers \(x\), and write \(h_k^p\) for the \(p\)-th iterate of \(h_k\). Then there is a natural number \(p \ge 1\) with \(h_k^{p-1}(k-1) < n(k-1) \le h_k^p(k-1)\) and \(J_k(n) = nk - h_k^p(k-1)\), where \(J_k\) is the Josephus function for elimination step \(k\).

The hypothesis \(n \ge 2\) is needed: for \(n = 1\) every \(p \ge 1\) has \(h_k^{p-1}(k-1) \ge k - 1 = n(k-1)\), so no such \(p\) exists.

public theorem_wanted josephus_eq_mul_sub_iterate_maximumNimH_pred (k n : ℕ)
    (hk : 2 ≤ k) (hn : 2 ≤ n) :
    ∃ p, 1 ≤ p ∧
      Nat.iterate (maximumNimH k) (p - 1) (k - 1) < n * (k - 1) ∧
      n * (k - 1) ≤ Nat.iterate (maximumNimH k) p (k - 1) ∧
      josephus k n = n * k - Nat.iterate (maximumNimH k) p (k - 1)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Corollary 1.

Uses 2

Statement usesJosephus survivor function · The Maximum Nim map \(h_k\)

TheoremLogarithmic bounds on the iterates of h_k#●ready to prove

Let \(k \ge 2\) and \(n \ge 1\) be natural numbers, let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) on natural numbers, write \(h_k^p\) for its \(p\)-fold iterate, and let

\[v = \frac{\log n}{\log k - \log(k-1)}, \qquad w = \frac{\log(n+1) - \log 2}{\log k - \log(k-1)},\]

where \(\log\) is the natural logarithm. Then

\[h_k^{\lfloor w \rfloor}(k-1) \le n(k-1) \le h_k^{\lceil v \rceil}(k-1).\]

public theorem_wanted maximumNimH_iterate_floor_le_mul_le_iterate_ceil (k n : ℕ)
    (hk : 2 ≤ k) (hn : 1 ≤ n) :
    let v : ℝ := Real.log n / (Real.log k - Real.log (k - 1))
    let w : ℝ := (Real.log (n + 1) - Real.log 2) / (Real.log k - Real.log (k - 1))
    Nat.iterate (maximumNimH k) (Nat.floor w) (k - 1) ≤ n * (k - 1) ∧
      n * (k - 1) ≤ Nat.iterate (maximumNimH k) (Nat.ceil v) (k - 1)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Lemma 8.

Uses 1

Statement usesThe Maximum Nim map \(h_k\)

TheoremLogarithmic bounds for the Josephus iteration count#●ready to prove

Let \(k \ge 2\) and \(n \ge 2\) be natural numbers, let \(h_k(x) = x + \lfloor x/(k-1) \rfloor + 1\) for natural numbers \(x\), write \(h_k^p\) for the \(p\)-th iterate of \(h_k\), and define the real numbers \(v = \log n / (\log k - \log(k-1))\) and \(w = (\log(n+1) - \log 2) / (\log k - \log(k-1))\), where \(\log\) is the natural logarithm. Then there is a natural number \(p \ge 1\) with \(\lfloor w \rfloor \le p \le \lceil v \rceil\) and \(J_k(n) = nk - h_k^p(k-1)\), where \(J_k\) is the Josephus function for elimination step \(k\).

The hypothesis \(n \ge 2\) is needed: for \(n = 1\) we have \(v = 0\), so \(\lceil v \rceil = 0\) and no \(p \ge 1\) satisfies \(p \le \lceil v \rceil\).

public theorem_wanted josephus_eq_mul_sub_iterate_maximumNimH_between_log_bounds
    (k n : ℕ) (hk : 2 ≤ k) (hn : 2 ≤ n) :
    let v : ℝ := Real.log n / (Real.log k - Real.log (k - 1))
    let w : ℝ := (Real.log (n + 1) - Real.log 2) / (Real.log k - Real.log (k - 1))
    ∃ p, 1 ≤ p ∧ Nat.floor w ≤ p ∧ p ≤ Nat.ceil v ∧
      josephus k n = n * k - Nat.iterate (maximumNimH k) p (k - 1)

Sources

• Shoei Takahashi, Hikaru Manabe, Ryohei Miyadera, Maximum Nim and the Josephus Problem, INTEGERS 24 (2024), Article G5, Theorem 4.

Uses 2

Statement usesJosephus survivor function · The Maximum Nim map \(h_k\)

19 fully proved22 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.