Smith's remoteness function

DefinitionSmith's remoteness function#✓fully proved

For an impartial game \(G\), the remoteness \(R(p)\) of a position \(p\) of \(G\) is defined by well-founded recursion along moves; the options of \(p\) are the positions reachable from \(p\) in one move. If \(p\) has no options, then \(R(p) = 0\). Otherwise, if some option \(q\) of \(p\) has \(R(q)\) even, then \(R(p)\) is \(1\) plus the least even value of \(R(q)\) over the options \(q\) of \(p\); if every option \(q\) of \(p\) has \(R(q)\) odd, then \(R(p)\) is \(1\) plus the largest value of \(R(q)\) over the options \(q\) of \(p\).

noncomputable def smithRemoteness (G : ImpartialGame) : G.Pos → ℕ :=
  (wfRel G).fix fun p ih =>
    let V := (G.moves p).attach.image fun q => ih q.1 q.2
    if hE : (V.filter Even).Nonempty then 1 + (V.filter Even).min' hE
    else if hV : V.Nonempty then 1 + V.max' hV else 0

Sources

• C. A. B. Smith, Graphs and composite games, J. Combin. Theory 1 (1966), 51–81; as recalled in Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.3.

Uses 1 · Used by 13

Statement usesImpartial game

Used byContinued fractions with maximal optimal play in Euclid · Positions of a Calkin–Wilf row with maximal optimal play in Euclid · Golden-ratio bounds for N-positions of maximal remoteness above 1 · Golden-ratio bounds for N-positions of maximal remoteness below 1 · Golden-ratio bounds for P-positions of maximal remoteness · Maximal-remoteness paths alternate in pairs · Basic-vector value equals Smith's remoteness (Lemma 4) · Theorem 2 (the M-rule realizes Smith's remoteness) · Remoteness of exact slow k-NIM from a list of piles · \(m\)-critical positions of exact slow \(k\)-NIM · The empty position is \(0\)-critical · Recursion for Smith's remoteness · Smith's remoteness vanishes at terminal positions

TheoremRecursion for Smith's remoteness#✓fully proved

Let \(G\) be an impartial game, \(p\) a position of \(G\), and \(R\) the set of remotenesses of the options of \(p\) (the positions reachable from \(p\) in one move). If \(R\) contains an even number, the remoteness of \(p\) is \(1\) plus the least even element of \(R\); otherwise, if \(R\) is nonempty, it is \(1\) plus the largest element of \(R\); and if \(R\) is empty, it is \(0\).

theorem smithRemoteness_eq (G : ImpartialGame) (p : G.Pos) :
    smithRemoteness G p =
      if hE : (((G.moves p).image (smithRemoteness G)).filter Even).Nonempty then
        1 + (((G.moves p).image (smithRemoteness G)).filter Even).min' hE
      else if hV : ((G.moves p).image (smithRemoteness G)).Nonempty then
        1 + ((G.moves p).image (smithRemoteness G)).max' hV
      else 0

Sources

• C. A. B. Smith, Graphs and composite games, J. Combin. Theory 1 (1966), 51–81.

Uses 2 · Used by 1

Statement usesImpartial game · Smith's remoteness function

Used bySmith's remoteness vanishes at terminal positions

TheoremSmith's remoteness vanishes at terminal positions#✓fully proved

In an impartial game, the remoteness of a terminal position (a position with no moves) is \(0\).

theorem smithRemoteness_of_moves_eq_empty (G : ImpartialGame) (p : G.Pos)
    (h : G.moves p = ∅) : smithRemoteness G p = 0

Sources

• C. A. B. Smith, Graphs and composite games, J. Combin. Theory 1 (1966), 51–81.

Uses 3 · Used by 1

Statement usesImpartial game · Smith's remoteness function

Proof usesRecursion for Smith's remoteness

Used byThe empty position is \(0\)-critical

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.