Section 5.1, paragraph 2Weak mastery = moving to a P-position at every decision history consistent with the agent's own play

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

We use standard impartial-game terminology: a $P$ -position is losing for the player to move, and an $N$ -position is winning. For NIM, Theorem 4.4 says that $P$ -positions are exactly the positions with nim-sum $0$ . Equivalently, weak mastery requires the agent to move to a $P$ -position at every one of its decision histories consistent with its own earlier actions, starting from an initial position winnable in its designated role. This distinction allows a simple strategy to master a family without solving positions it never encounters under its own play; Appendix D gives examples.

Generated from paper_jmlr.tex, lines 460–461.

2 Explain this

This paragraph restates weak mastery in game-theoretic terms. In NIM the losing positions for the player to move ( $P$ -positions) are exactly those with nim-sum zero. A strategy weakly masters a family exactly when, starting from any position its role can win, it moves to a $P$ -position at every decision point that its own earlier play can lead to, whatever the opponent does.

That lets a simple strategy master a family without solving positions it never meets. The pairing strategy in Appendix D is the standard example.

3 How this is formalised

Mastery.secure_iff_guarantee: winning against every legal opponent is equivalent to the history condition "on every consistent history at the agent's turn, the prescribed action exists and is legal". An absent or illegal action is therefore a loss, never a vacuous success.
Mastery.weakMastery_iff_optimal: weak mastery holds iff, from every winnable initial board, at every consistent history at the agent's turn the strategy plays a legal move to nim-sum zero.
Mastery.roleWinnable_first: the first player can win from $P_0$ iff its nim-sum is nonzero (the second player iff it is zero).

Coverage record
Paper anchor	`sec-mastery-notions-p2` (website anchor; the manuscript has no label here)
Displayed as	Section 5.1, paragraph 2
Claim	Weak mastery = moving to a P-position at every decision history consistent with the agent's own play
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 460–461; SHA-256 of the normalised block source `277a6851ee46eef1…`
Lean declarations	`NimAudit.Mastery.secure_iff_guarantee` (WeakMastery, lines 406–415, file `4c83e573f527…`) `NimAudit.Mastery.weakMastery_iff_optimal` (WeakMastery, lines 648–658, file `4c83e573f527…`) `NimAudit.Mastery.roleWinnable_first` (WeakMastery, lines 579–590, file `4c83e573f527…`)
Depends on	Definition 5.1, Theorem 4.4
Audited correspondence rows	`def:mastery`
Explanations	`explain/c-weak-mastery-histories`, `formal/c-weak-mastery-histories`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Mastery.secure_iff_guarantee`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 406–415) · file SHA-256 4c83e573f527989c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

C2, HISTORY CHARACTERISATION: σ wins from P₀ in role r against every legal opponent iff on every policy-consistent history at the agent's turn its prescribed action exists and is legal.

Statement as elaborated and printed by Lean 4.26.0

∀ (r : NimAudit.Mastery.Role) (σ : NimAudit.Mastery.Strat) (P0 : List ℕ),
  NimAudit.Mastery.Secure r σ P0 ↔ NimAudit.Mastery.Guarantee r σ P0

Exact source text, lines 406–415

406/-- C2, HISTORY CHARACTERISATION: σ wins from P₀ in role r against every legal opponent iff407    on every policy-consistent history at the agent's turn its prescribed action exists and408    is legal. -/409theorem secure_iff_guarantee (r : Role) (σ : Strat) (P0 : List Nat) : Secure r σ P0 ↔ Guarantee r σ P0 := by410  refine ⟨secure_guarantee, fun hg h hc hm => ?_⟩411  apply Classical.byContradiction; intro hfail412  have hb := hg (follow h) (follow_legal (cons_legal hc))413  unfold Beats follow at hb414  rw [followD_reach _ hc, play_own_fail hm hfail] at hb415  cases hb

Project declarations in the statement: Mastery.Guarantee, Mastery.Role, Mastery.Secure, Mastery.Strat

Project declarations used by the proof or definition body

Game.Move, Mastery.Beats, Mastery.Cons, Mastery.Guarantee, Mastery.Hist, Mastery.Outcome, Mastery.Outcome.agentLoses, Mastery.Outcome.agentWins, Mastery.Outcome.casesOn, Mastery.Role, Mastery.Secure, Mastery.Strat, Mastery.cons_legal, Mastery.cur, Mastery.follow, Mastery.followD, Mastery.followD_reach, Mastery.follow_legal, Mastery.mover, Mastery.play, Mastery.play_own_fail, Mastery.secure_guarantee, Rollout.subFirstPos

theorem `Mastery.weakMastery_iff_optimal`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 648–658) · file SHA-256 4c83e573f527989c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

WEAK MASTERY = WINNING MOVES ON POLICY-CONSISTENT HISTORIES: σ is weakly masterful for F and r iff, from every winnable initial board of F, at every history consistent with σ's own preceding actions where σ is to move, σ plays a legal move to a P-position. Contrast StrongMastery below, which asks this on ALL legal histories.

Statement as elaborated and printed by Lean 4.26.0

∀ (F : List ℕ → Prop) (r : NimAudit.Mastery.Role) (σ : NimAudit.Mastery.Strat),
  NimAudit.Mastery.WeakMastery F r σ ↔
    ∀ (P0 : List ℕ),
      F P0 →
        NimAudit.Mastery.RoleWinnable r P0 →
          ∀ (h : NimAudit.Mastery.Hist),
            NimAudit.Mastery.Cons r σ P0 h →
              NimAudit.Mastery.mover h = r →
                ∃ Q,
                  σ h = some Q ∧
                    NimAudit.Game.Move (NimAudit.Mastery.cur h) Q ∧ NimAudit.nimSum Q = 0

Exact source text, lines 648–658

648/-- WEAK MASTERY = WINNING MOVES ON POLICY-CONSISTENT HISTORIES: σ is weakly masterful for F649    and r iff, from every winnable initial board of F, at every history consistent with σ's650    own preceding actions where σ is to move, σ plays a legal move to a P-position.  Contrast651    StrongMastery below, which asks this on ALL legal histories. -/652theorem weakMastery_iff_optimal (F : List Nat → Prop) (r : Role) (σ : Strat) :653    WeakMastery F r σ ↔ ∀ P0, F P0 → RoleWinnable r P0 → ∀ h, Cons r σ P0 h → mover h = r →654      ∃ Q, σ h = some Q ∧ Move (cur h) Q ∧ nimSum Q = 0 := by655  constructor656  · intro hw P0 hF hr h hc hm; exact guarantee_optimal (hw P0 hF hr) hc hm657  · intro h P0 hF hr658    exact secure_guarantee (fun g hc hm => let ⟨Q, h1, h2, _⟩ := h P0 hF hr g hc hm; ⟨Q, h1, h2⟩)

Project declarations in the statement: Game.Move, Mastery.Cons, Mastery.Hist, Mastery.Role, Mastery.RoleWinnable, Mastery.Strat, Mastery.WeakMastery, Mastery.cur, Mastery.mover, nimSum

Project declarations used by the proof or definition body

Game.Move, Mastery.Cons, Mastery.Hist, Mastery.Role, Mastery.RoleWinnable, Mastery.Strat, Mastery.WeakMastery, Mastery.cur, Mastery.guarantee_optimal, Mastery.mover, Mastery.secure_guarantee, nimSum

theorem `Mastery.roleWinnable_first`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 579–590) · file SHA-256 4c83e573f527989c… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

WHICH ROLE IS WINNABLE: the first player has a winning strategy iff nim(P₀) ≠ 0, the second iff nim(P₀) = 0 (i.e. iff P₀ is an N- resp. P-position).

Statement as elaborated and printed by Lean 4.26.0

∀ (P0 : List ℕ),
  NimAudit.Mastery.RoleWinnable NimAudit.Mastery.Role.first P0 ↔ NimAudit.nimSum P0 ≠ 0

Exact source text, lines 579–590

579/-- WHICH ROLE IS WINNABLE: the first player has a winning strategy iff nim(P₀) ≠ 0, the580    second iff nim(P₀) = 0 (i.e. iff P₀ is an N- resp. P-position). -/581theorem roleWinnable_first (P0 : List Nat) : RoleWinnable .first P0 ↔ nimSum P0 ≠ 0 := by582  constructor583  · rintro ⟨σ, hg⟩ h0584    have := hg optOpp optOpp_legal585    unfold Beats at this586    rw [optOpp_play (r := .first) (σ := σ) (P0.sum + 1) [P0] (by simp [cur]) (fun _ => h0)587      (fun h => absurd rfl h)] at this588    cases this589  · intro h590    exact ⟨ofSel (agent P0.sum), secure_guarantee (wins_secure (agent_wins P0 (width_sum P0) h))⟩

Project declarations in the statement: Mastery.Role.first, Mastery.RoleWinnable, nimSum

Project declarations used by the proof or definition body

Game.agent, Game.agent_wins, Mastery.Beats, Mastery.Guarantee, Mastery.Outcome, Mastery.Outcome.agentLoses, Mastery.Outcome.agentWins, Mastery.Outcome.casesOn, Mastery.Role, Mastery.Role.first, Mastery.RoleWinnable, Mastery.Strat, Mastery.cur, Mastery.mover, Mastery.ofSel, Mastery.optOpp, Mastery.optOpp_legal, Mastery.optOpp_play, Mastery.play, Mastery.secure_guarantee, Mastery.width_sum, Mastery.wins_secure, nimSum

Definitions these statements use

def `Mastery.Guarantee`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 287–288) · file SHA-256 4c83e573f527989c…

σ wins from P₀ in role r against EVERY legal opponent strategy.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 287–288

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

Project declarations in the statement: Mastery.Role, Mastery.Strat

Project declarations used by the proof or definition body

Mastery.Beats, Mastery.LegalOpp, Mastery.Role, Mastery.Strat

inductive `Mastery.Role`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 37–40) · file SHA-256 4c83e573f527989c…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 37–40

37inductive Role where38  | first39  | second40  deriving DecidableEq

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Mastery.Secure`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 159–163) · file SHA-256 4c83e573f527989c…

The history guarantee: on every policy-consistent history where it is the agent's turn, the prescribed action exists and is a legal move (in particular the agent is never to move at a terminal board).

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 159–163

159/-- The history guarantee: on every policy-consistent history where it is the agent's turn,160    the prescribed action exists and is a legal move (in particular the agent is never to161    move at a terminal board). -/162def Secure (r : Role) (σ : Strat) (P0 : List Nat) : Prop :=163  ∀ h, Cons r σ P0 h → mover h = r → ∃ Q, σ h = some Q ∧ Move (cur h) Q

Project declarations in the statement: Mastery.Role, Mastery.Strat

Project declarations used by the proof or definition body

Game.Move, Mastery.Cons, Mastery.Hist, Mastery.Role, Mastery.Strat, Mastery.cur, Mastery.mover

def `Mastery.Strat`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 54–55) · file SHA-256 4c83e573f527989c…

A (history-dependent) strategy proposes the next board; `none` means no action.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 54–55

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

Mastery.Hist

def `Game.Move`

Module NimGame (lean/phase2/NimGame.lean, lines 24–26) · file SHA-256 23df6bb87ecfd344…

An ordinary legal Nim move: exactly one heap strictly decreases.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop

Exact source text, lines 24–26

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Mastery.Cons`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 123–129) · file SHA-256 4c83e573f527989c…

Policy-consistent legal histories for the agent in role r using σ: on the agent's turns only its own prescribed legal action occurs; on the opponent's turns any legal move.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 123–129

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)

Project declarations in the statement: Mastery.Hist, Mastery.Role, Mastery.Strat

Project declarations used by the proof or definition body

Game.Move, Mastery.Hist, Mastery.Role, Mastery.Strat, Mastery.cur, Mastery.mover

def `Mastery.Hist`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 51–52) · file SHA-256 4c83e573f527989c…

A history: the boards so far, MOST RECENT FIRST; its last entry is the initial board.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 51–52

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Mastery.RoleWinnable`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 419–420) · file SHA-256 4c83e573f527989c…

The role r has a winning strategy from P₀ (existence, separate from any policy).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Mastery.Role → List ℕ → Prop

Exact source text, lines 419–420

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

Project declarations in the statement: Mastery.Role

Project declarations used by the proof or definition body

Mastery.Guarantee, Mastery.Role, Mastery.Strat

def `Mastery.WeakMastery`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 614–618) · file SHA-256 4c83e573f527989c…

WEAK MASTERY of policy σ for the family F of initial boards and the designated role r: from every initial board of the family from which the role has SOME winning strategy, σ itself wins against every legal opponent strategy.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 614–618

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

Project declarations in the statement: Mastery.Role, Mastery.Strat

Project declarations used by the proof or definition body

Mastery.Guarantee, Mastery.Role, Mastery.RoleWinnable, Mastery.Strat

def `Mastery.cur`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 57–58) · file SHA-256 4c83e573f527989c…

The current board.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Mastery.Hist → List ℕ

Exact source text, lines 57–58

57/-- The current board. -/58def cur (h : Hist) : List Nat := h.headD []

Project declarations in the statement: Mastery.Hist

Project declarations used by the proof or definition body

Mastery.Hist

def `Mastery.mover`

Module WeakMastery (lean/phase8/WeakMastery.lean, lines 62–63) · file SHA-256 4c83e573f527989c…

The player to move: the first player after an even number of moves (odd length).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Mastery.Hist → NimAudit.Mastery.Role

Exact source text, lines 62–63

62/-- The player to move: the first player after an even number of moves (odd length). -/63def mover (h : Hist) : Role := if h.length % 2 = 1 then .first else .second

Project declarations in the statement: Mastery.Hist, Mastery.Role

Project declarations used by the proof or definition body

Mastery.Hist, Mastery.Role, Mastery.Role.first, Mastery.Role.second

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

Module	File	Lines	Imports
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
WeakMastery	`lean/phase8/WeakMastery.lean`	959	Misc

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).

Section 5.1, paragraph 2Weak mastery = moving to a P-position at every decision history consistent with the agent's own play

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Mastery.secure_iff_guarantee

theorem Mastery.weakMastery_iff_optimal

theorem Mastery.roleWinnable_first

Definitions these statements use

def Mastery.Guarantee

inductive Mastery.Role

def Mastery.Secure

def Mastery.Strat

def Game.Move

inductive Mastery.Cons

def Mastery.Hist

def Mastery.RoleWinnable

def Mastery.WeakMastery

def Mastery.cur

def Mastery.mover

def nimSum

Full modules

theorem `Mastery.secure_iff_guarantee`

theorem `Mastery.weakMastery_iff_optimal`

theorem `Mastery.roleWinnable_first`

def `Mastery.Guarantee`

inductive `Mastery.Role`

def `Mastery.Secure`

def `Mastery.Strat`

def `Game.Move`

inductive `Mastery.Cons`

def `Mastery.Hist`

def `Mastery.RoleWinnable`

def `Mastery.WeakMastery`

def `Mastery.cur`

def `Mastery.mover`

def `nimSum`