Definition 5.1Strong, weak and restoration mastery

The paper uses three standards of "playing NIM well".

• Strong mastery: at every winning position where it is to move, the agent chooses a winning move, including positions that only arise after mistakes by either player.
• Weak mastery (relative to an initial position and a role): if that role can win from the start, the agent's own strategy wins against every opponent. Positions that the agent's own play never reaches do not matter.
• Restoration mastery: whenever the opponent moves away from a zero-nim-sum position, the agent moves back to nim-sum zero.

Example of the difference. From the single heap $(3)$, the strategy "take all three stones" wins at once, so it weakly masters $(3)$ as first player. It says nothing about $(1)$, which strong mastery would require after $(3)\to(2)\to(1)$ (see Appendix D).

Caveats spelled out in the definition. Strategies may use the whole history. Opponent moves are legal; a missing or illegal agent move counts as a loss. If the designated role is losing from the initial position, weak mastery asks nothing at all: it is vacuous there.

Histories and strategies. A history (Mastery.Hist) is the list of boards so far, most recent first; a strategy (Mastery.Strat) maps a history to a proposed next board or to "no action".

Consistency. Mastery.Cons defines the histories consistent with the agent's own play from an initial board $P_0$ in role $r$: on the agent's turns only its own prescribed legal action occurs; on the opponent's turns every legal move may occur.

The notions.

• Mastery.Guarantee: the strategy wins from $P_0$ in role $r$ against every legal opponent strategy (plays are finite because stones decrease).
• Mastery.WeakMastery $F\ r\ \sigma$: from every initial board in the family $F$ from which role $r$ has some winning strategy (Mastery.RoleWinnable), $\sigma$ has the guarantee.
• Mastery.StrongMastery $F\ r\ \sigma$: at every legal history from $F$ (arbitrary actions by both players) where the agent is to move at a nonzero nim-sum, $\sigma$ moves to nim-sum zero.
• Restoration: Game.restore_correct shows that the two-frame restoration selector has this property under its promise.

Vacuity, made explicit. Mastery.weakMastery_vacuous: on a family of boards from which the role is losing, every strategy, even one that never moves, is weakly masterful. Strong mastery implies weak mastery (Mastery.strong_weak), and the separation example is Appendix D, paragraph 1.

Principal declarations

(List ℕ → Prop) → NimAudit.Mastery.Role → NimAudit.Mastery.Strat → Prop

812/-- Strong mastery (Definition def:mastery, first clause) relative to F and r: at EVERY813    legal history (arbitrary actions by both players) with the agent to move at an814    N-position, σ plays a move to a P-position. -/815def StrongMastery (F : List Nat → Prop) (r : Role) (σ : Strat) : Prop :=816  ∀ P0, F P0 → ∀ h, Legal P0 h → mover h = r → nimSum (cur h) ≠ 0 →817    ∃ Q, σ h = some Q ∧ Move (cur h) Q ∧ nimSum Q = 0

(List ℕ → Prop) → NimAudit.Mastery.Role → NimAudit.Mastery.Strat → Prop

614/-- WEAK MASTERY of policy σ for the family F of initial boards and the designated role r:615    from every initial board of the family from which the role has SOME winning strategy,616    σ itself wins against every legal opponent strategy. -/617def WeakMastery (F : List Nat → Prop) (r : Role) (σ : Strat) : Prop :=618  ∀ P0, F P0 → RoleWinnable r P0 → Guarantee r σ P0

NimAudit.Mastery.Role → NimAudit.Mastery.Strat → List ℕ → Prop

287/-- σ wins from P₀ in role r against EVERY legal opponent strategy. -/288def Guarantee (r : Role) (σ : Strat) (P0 : List Nat) : Prop := ∀ τ, LegalOpp τ → Beats r σ τ P0

NimAudit.Mastery.Role → NimAudit.Mastery.Strat → List ℕ → NimAudit.Mastery.Hist → Prop

123/-- Policy-consistent legal histories for the agent in role r using σ: on the agent's turns124    only its own prescribed legal action occurs; on the opponent's turns any legal move. -/125inductive Cons (r : Role) (σ : Strat) (P0 : List Nat) : Hist → Prop126  | init : Cons r σ P0 [P0]127  | opp {h : Hist} {Q : List Nat} : Cons r σ P0 h → mover h ≠ r → Move (cur h) Q → Cons r σ P0 (Q :: h)128  | own {h : Hist} {Q : List Nat} : Cons r σ P0 h → mover h = r → σ h = some Q → Move (cur h) Q →129      Cons r σ P0 (Q :: h)

∀ {F : List ℕ → Prop} {r : NimAudit.Mastery.Role},
  (∀ (P0 : List ℕ), F P0 → ¬NimAudit.Mastery.RoleWinnable r P0) →
    ∀ (σ : NimAudit.Mastery.Strat), NimAudit.Mastery.WeakMastery F r σ

636/-- THE CONDITIONAL CASE MADE EXPLICIT: at an initial board from which the role is losing637    there is nothing to check, so on a family of losing boards EVERY policy (even one that638    never moves) is weakly masterful.  Weak mastery is informative only where the role is639    winnable. -/640theorem weakMastery_vacuous {F : List Nat → Prop} {r : Role} (hF : ∀ P0, F P0 → ¬ RoleWinnable r P0)641    (σ : Strat) : WeakMastery F r σ :=642  fun P0 h1 h2 => absurd h2 (hF P0 h1)

∀ {Q Q' : List ℕ},
  NimAudit.nimSum Q = 0 →
    NimAudit.Game.Move Q Q' →
      ∃ R, NimAudit.Game.restore Q Q' = some R ∧ NimAudit.Game.Move Q' R ∧ NimAudit.nimSum R = 0

412theorem restore_correct {Q Q' : List Nat} (h0 : nimSum Q = 0) (hm : Move Q Q') :413    ∃ R, restore Q Q' = some R ∧ Move Q' R ∧ nimSum R = 0 := by414  have hne := move_from_zero hm h0415  have hd : nimSum Q ^^^ nimSum Q' = nimSum Q' := by rw [h0, Nat.zero_xor]416  obtain ⟨R, hsel, hmR, hR⟩ := selectMove_zero hne417  refine ⟨R, ?_, hmR, hR⟩418  unfold restore419  rw [hd]420  simp only [selectMove, hne, if_false] at hsel421  split at hsel422  · next q' hq' => cases hsel; exact hq'423  · next _ hnone =>424    obtain ⟨pre, x, post, hp, hlt, _⟩ := exists_decreasing_heap Q' hne425    exact absurd hlt (cancelFirst_none hnone x (by rw [hp]; simp))

Definitions these statements use

Type

51/-- A history: the boards so far, MOST RECENT FIRST; its last entry is the initial board. -/52abbrev Hist := List (List Nat)

Type

54/-- A (history-dependent) strategy proposes the next board; `none` means no action. -/55abbrev Strat := Hist → Option (List Nat)

NimAudit.Mastery.Role → List ℕ → Prop

419/-- The role r has a winning strategy from P₀ (existence, separate from any policy). -/420def RoleWinnable (r : Role) (P0 : List Nat) : Prop := ∃ σ : Strat, Guarantee r σ P0

Type

37inductive Role where38  | first39  | second40  deriving DecidableEq

List ℕ → List ℕ → Prop

24/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x

List ℕ → List ℕ → Option (List ℕ)

407/-- Two-frame restoration selector (paper Prop. restore / Thm search-gap (iii)):408    from the predecessor Q and current board Q', cancel delta = nim(Q) XOR nim(Q'). -/409def restore (Q Q' : List Nat) : Option (List Nat) :=410  cancelFirst (nimSum Q ^^^ nimSum Q') Q'

List ℕ → ℕ

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

Full modules

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).