Appendix D, paragraph 1From (3), taking all stones weakly masters the position but is not strong mastery

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

1 Paper text

The distinction from strong mastery is substantive. From the single heap $(3)$ , a strategy that takes all three stones wins immediately, irrespective of what it would do elsewhere. It therefore weakly masters that initial position as first player. If it has no prescribed move at $(1)$ , however, it fails strong mastery: arbitrary legal play can reach $(3)\to(2)\to(1)$ with the first player to move. That history is excluded by its own initial action. The general definition and this separation are checked in Lean.

Generated from paper_jmlr.tex, lines 1566–1566.

2 Explain this

From the single heap $(3)$ , the strategy "take all three stones" wins at once, so it weakly masters $(3)$ as first player, whatever it would do elsewhere. But it prescribes nothing at $(1)$ , and arbitrary legal play can reach $(3)\to(2)\to(1)$ with the first player to move. Strong mastery requires a winning move there, so this strategy is not strongly masterful. That history is excluded from weak mastery because it contradicts the strategy's own first move.

3 How this is formalised

Mastery.sep3 is the strategy "at $(3)$ play $(0)$ , otherwise nothing". Mastery.sep3_weak: it is weakly masterful for the family $\{(3)\}$ and the first role. Mastery.sep3_not_strong: it is not strongly masterful (after the counterfactual $3\to2$ and $2\to1$ it has no move at the $N$ -position $(1)$ ). Mastery.strong_weak: strong mastery always implies weak mastery.

Coverage record
Paper anchor	`app:weak-p1` (website anchor; the manuscript has no label here)
Displayed as	Appendix D, paragraph 1
Claim	From (3), taking all stones weakly masters the position but is not strong mastery
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1566–1566; SHA-256 of the normalised block source `5203245c88a18003…`
Lean declarations	`NimAudit.Mastery.sep3_weak` (WeakMastery, lines 858–876, file `4c83e573f527…`) `NimAudit.Mastery.sep3_not_strong` (WeakMastery, lines 878–885, file `4c83e573f527…`) `NimAudit.Mastery.strong_weak` (WeakMastery, lines 819–837, file `4c83e573f527…`)
Audited correspondence rows	`app:weak`
Explanations	`explain/c-weak-vs-strong`, `formal/c-weak-vs-strong`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Mastery.sep3_weak`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Mastery.WeakMastery (fun P => P = [3]) NimAudit.Mastery.Role.first NimAudit.Mastery.sep3

Exact source text, lines 858–876

858theorem sep3_weak : WeakMastery (fun P => P = [3]) .first sep3 := by859  intro P0 hP _860  subst hP861  refine secure_guarantee (fun h hc hm => ?_)862  have key : ∀ h, Cons .first sep3 [3] h → (mover h = .first → h = [[3]]) ∧ (mover h ≠ .first → Terminal (cur h)) := by863    intro h hc864    induction hc with865    | init => exact ⟨fun _ => rfl, fun h => absurd rfl h⟩866    | @opp h Q hc' hne hmv ih =>867      exact absurd hmv ((terminal_iff_no_move _).1 (ih.2 hne) Q)868    | @own h Q hc' hm' hσ hmv ih =>869      have e := ih.1 hm'870      subst e871      have hQ : Q = [0] := by simp [sep3, cur] at hσ; exact hσ.symm872      subst hQ873      exact ⟨fun h' => absurd h' (mover_cons_ne hm'), fun _ => by intro x hx; simpa using hx⟩874  have e := (key h hc).1 hm875  subst e876  exact ⟨[0], by simp [sep3, cur], ⟨[], 3, [], 0, rfl, rfl, by omega⟩⟩

Project declarations in the statement: Mastery.Role.first, Mastery.WeakMastery, Mastery.sep3

Project declarations used by the proof or definition body

Game.Move, Game.Terminal, Game.terminal_iff_no_move, Mastery.Cons, Mastery.Cons.rec, Mastery.Guarantee, Mastery.Hist, Mastery.Role, Mastery.Role.first, Mastery.RoleWinnable, Mastery.cur, Mastery.mover, Mastery.mover_cons_ne, Mastery.secure_guarantee, Mastery.sep3

theorem `Mastery.sep3_not_strong`

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

… but it is not strongly masterful: after the counterfactual agent mistake 3 → 2 and the reply 2 → 1, the agent is to move at the N-position (1) and its policy has no move.

Statement as elaborated and printed by Lean 4.26.0

¬NimAudit.Mastery.StrongMastery (fun P => P = [3]) NimAudit.Mastery.Role.first NimAudit.Mastery.sep3

Exact source text, lines 878–885

878/-- … but it is not strongly masterful: after the counterfactual agent mistake 3 → 2 and the879    reply 2 → 1, the agent is to move at the N-position (1) and its policy has no move. -/880theorem sep3_not_strong : ¬ StrongMastery (fun P => P = [3]) .first sep3 := by881  intro hs882  have hl : Legal [3] [[1], [2], [3]] :=883    Legal.step (Legal.step Legal.init ⟨[], 3, [], 2, rfl, rfl, by omega⟩) ⟨[], 2, [], 1, rfl, rfl, by omega⟩884  obtain ⟨Q, hQ, _⟩ := hs [3] rfl _ hl rfl (by decide)885  simp [sep3, cur] at hQ

Project declarations in the statement: Mastery.Role.first, Mastery.StrongMastery, Mastery.sep3

Project declarations used by the proof or definition body

Game.Move, Mastery.Legal, Mastery.Legal.init, Mastery.Legal.step, Mastery.Role, Mastery.Role.first, Mastery.StrongMastery, Mastery.cur, Mastery.mover, Mastery.sep3, nimSum

theorem `Mastery.strong_weak`

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

Statement as elaborated and printed by Lean 4.26.0

∀ {F : List ℕ → Prop} {r : NimAudit.Mastery.Role} {σ : NimAudit.Mastery.Strat},
  NimAudit.Mastery.StrongMastery F r σ → NimAudit.Mastery.WeakMastery F r σ

Exact source text, lines 819–837

819theorem strong_weak {F : List Nat → Prop} {r : Role} {σ : Strat} (hs : StrongMastery F r σ) :820    WeakMastery F r σ := by821  intro P0 hF hwin822  have inv : ∀ h, Cons r σ P0 h → (mover h = r → nimSum (cur h) ≠ 0) ∧ (mover h ≠ r → nimSum (cur h) = 0) := by823    intro h hc824    induction hc with825    | init =>826      cases r827      · exact ⟨fun _ => (roleWinnable_first P0).1 hwin, fun h => absurd rfl h⟩828      · exact ⟨fun h => by simp at h, fun _ => (roleWinnable_second P0).1 hwin⟩829    | @opp h Q hc' hne hmv ih =>830      exact ⟨fun _ => move_from_zero hmv (ih.2 hne), fun h' => absurd (mover_cons_eq hne) h'⟩831    | @own h Q hc' hm hσ hmv ih =>832      obtain ⟨Q', h1, _, h3⟩ := hs P0 hF h (cons_legal hc') hm (ih.1 hm)833      rw [hσ] at h1; cases h1834      exact ⟨fun h' => absurd h' (mover_cons_ne hm), fun _ => h3⟩835  refine secure_guarantee (fun h hc hm => ?_)836  obtain ⟨Q, h1, h2, _⟩ := hs P0 hF h (cons_legal hc) hm ((inv h hc).1 hm)837  exact ⟨Q, h1, h2⟩

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

Project declarations used by the proof or definition body

Game.Move, Game.move_from_zero, Mastery.Cons, Mastery.Cons.rec, Mastery.Hist, Mastery.Role, Mastery.Role.casesOn, Mastery.Role.first, Mastery.Role.second, Mastery.RoleWinnable, Mastery.Strat, Mastery.StrongMastery, Mastery.cons_legal, Mastery.cur, Mastery.mover, Mastery.mover_cons_eq, Mastery.mover_cons_ne, Mastery.roleWinnable_first, Mastery.roleWinnable_second, Mastery.secure_guarantee, nimSum

Definitions these statements use

def `Mastery.sep3`

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

SEPARATION EXAMPLE: from (3) the first player takes all three stones; the policy is undefined everywhere else.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Mastery.Strat

Exact source text, lines 854–856

854/-- SEPARATION EXAMPLE: from (3) the first player takes all three stones; the policy is855    undefined everywhere else. -/856def sep3 : Strat := fun h => if cur h = [3] then some [0] else none

Project declarations in the statement: Mastery.Strat

Project declarations used by the proof or definition body

Mastery.Hist, Mastery.cur

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.StrongMastery`

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

Strong mastery (Definition def:mastery, first clause) relative to F and r: at EVERY legal history (arbitrary actions by both players) with the agent to move at an N-position, σ plays a move to a P-position.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 812–817

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

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

Project declarations used by the proof or definition body

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

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

Full modules

Module	File	Lines	Imports
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).

Appendix D, paragraph 1From (3), taking all stones weakly masters the position but is not strong mastery

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Mastery.sep3_weak

theorem Mastery.sep3_not_strong

theorem Mastery.strong_weak

Definitions these statements use

def Mastery.sep3

def Mastery.WeakMastery

def Mastery.StrongMastery

inductive Mastery.Role

def Mastery.Strat

Full modules

theorem `Mastery.sep3_weak`

theorem `Mastery.sep3_not_strong`

theorem `Mastery.strong_weak`

def `Mastery.sep3`

def `Mastery.WeakMastery`

def `Mastery.StrongMastery`

inductive `Mastery.Role`

def `Mastery.Strat`