Periodicity of finite octal games

### What is the conjecture

“Finite octal games” are the take‑and‑break impartial games coded by a finite octal string. The open conjecture asks whether the Sprague‑Grundy (nim‑)sequence of every such game becomes eventually periodic.

Sources: https://arxiv.org/abs/1803.02621

### Prerequisites needed

Building blocks (from Mathlib)

- Nat – basic arithmetic, inequalities, recursion.
- List ℕ / Finset ℕ – finite containers to store the octal code (a list of digits 0‑7).
- Nat.testBit, Nat.shiftRight, Nat.land – bit‑operations needed to read the binary expansion of each octal digit.
- Ordinal – the underlying type for Grundy values; provides mex, succ, lt.
- Mathlib.SetTheory.Nimber.Basic – type Nimber, nim‑addition (+), and nim‑multiplication (*).
- Mathlib.SetTheory.Game.Nim – definition of impartial Nim heaps (pgame.nim), the class [Impartial], the function - pgame.grundy_value (the Sprague‑Grundy value), and the theorem pgame.equiv_nim_grundy_value.
- Mathlib.Data.Nat.ModPow – modular arithmetic when reasoning about periods (e.g., n + p).
- Mathlib.Tactic – standard proof tactics (simp, linarith, omega) that will be useful for the periodicity predicate.

Missing pieces (to be added for the conjecture)

- Octal‑game definition: This recursive definition must translate each digit’s binary expansion into the allowed “remove k beans and split the remainder into the prescribed sub‑heaps”.
Impartiality lemma: proof that octalGame code satisfies the [Impartial] class, so the Sprague‑Grundy machinery applies.
- Grundy‑sequence wrapper: A convenient name for the sequence of Grundy values.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else