WeakMastery

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import Misc23/- Phase 8, part C: general weak mastery for Nim, its game semantics, and the checked4   instances.  Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   Paper target: Definition def:mastery (weak mastery relative to an initial position and a7   designated role; histories consistent with the agent's own preceding actions; families8   of initial positions) and Appendix app:weak (pairing strategy).910   C1  Roles, histories (most recent board first), whose turn it is, legal histories,11       policy-consistent histories (`Cons`): on the agent's turns only its own prescribed,12       legal action may occur; on the opponent's turns every legal move may occur.13       Strategies are history-dependent (`Strat := Hist → Option board`).  Plays of a14       strategy pair (`play`, with fuel) and termination by the stone-count decrease.15   C2  `Guarantee r σ P₀` (σ wins against EVERY legal opponent strategy from P₀ in role r),16       `RoleWinnable r P₀` (some strategy has that guarantee; characterised by the nim-sum),17       and `WeakMastery F r σ`.  The history characterisation `secure_iff_guarantee`:18       the guarantee holds iff on every policy-consistent history where it is the agent's19       turn the prescribed action exists and is legal.  So an absent or illegal action is20       a loss, never a vacuous success.21   C3  Bridges from NimGame.Wins (first player), Misc.SecondWins (second player) and22       WholeGame.TwoFrameWins (a history-dependent second-player strategy using the23       previous board).  Instances: the pairing strategy pairSel B (binary selector) and its24       compiled network version, the multi-head network player mhSelect B, and the25       network-driven two-frame restoration player restReply B.26   C4  Locality (`cons_congr`, `guarantee_congr`): strategies that agree on the27       policy-consistent agent-turn histories have the same guarantee.  Strong mastery28       implies weak mastery, and an explicit example is weakly but not strongly masterful. -/2930namespace NimAudit31namespace Mastery3233open Game Rollout Recurrent Misc WholeGame3435/-! ## C1. Roles, histories, turns -/3637inductive Role where38  | first39  | second40  deriving DecidableEq4142def Role.other : Role → Role43  | .first => .second44  | .second => .first4546theorem Role.other_ne (r : Role) : r.other ≠ r := by cases r <;> simp [Role.other]4748theorem Role.eq_other_of_ne {r s : Role} (h : s ≠ r) : s = r.other := by49  cases r <;> cases s <;> simp_all [Role.other]5051/-- A history: the boards so far, MOST RECENT FIRST; its last entry is the initial board. -/52abbrev Hist := List (List Nat)5354/-- A (history-dependent) strategy proposes the next board; `none` means no action. -/55abbrev Strat := Hist → Option (List Nat)5657/-- The current board. -/58def cur (h : Hist) : List Nat := h.headD []5960@[simp] theorem cur_cons (Q : List Nat) (h : Hist) : cur (Q :: h) = Q := rfl6162/-- 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 .second6465theorem mover_cons (Q : List Nat) (h : Hist) : mover (Q :: h) = (mover h).other := by66  unfold mover Role.other67  simp only [List.length_cons]68  by_cases h1 : h.length % 2 = 169  · rw [if_pos h1, if_neg (by omega)]70  · rw [if_neg h1, if_pos (by omega)]7172@[simp] theorem mover_init (P : List Nat) : mover [P] = .first := rfl7374theorem mover_cons_eq {r : Role} {Q : List Nat} {h : Hist} (hm : mover h ≠ r) : mover (Q :: h) = r := by75  rw [mover_cons]; have := Role.eq_other_of_ne hm76  rw [this]; cases r <;> rfl7778theorem mover_cons_ne {r : Role} {Q : List Nat} {h : Hist} (hm : mover h = r) : mover (Q :: h) ≠ r := by79  rw [mover_cons, hm]; exact Role.other_ne r8081/-- Legal histories from P₀: arbitrary legal actions by both players. -/82inductive Legal (P0 : List Nat) : Hist → Prop83  | init : Legal P0 [P0]84  | step {h : Hist} {Q : List Nat} : Legal P0 h → Move (cur h) Q → Legal P0 (Q :: h)8586/-- TERMINATION OF LEGAL PLAY: stones strictly decrease, so a legal history from P₀ has at87    most P₀.sum moves (length ≤ P₀.sum + 1), for both roles and every board, including an88    initially terminal one (length 1). -/89theorem legal_sum {P0 : List Nat} {h : Hist} (hl : Legal P0 h) : (cur h).sum + h.length ≤ P0.sum + 1 := by90  induction hl with91  | init => simp [cur]92  | step _ hm ih => have := move_sum_lt hm; simp only [cur_cons, List.length_cons]; omega9394theorem legal_length {P0 : List Nat} {h : Hist} (hl : Legal P0 h) : h.length ≤ P0.sum + 1 := by95  have := legal_sum hl; omega9697theorem legal_ne_nil {P0 : List Nat} {h : Hist} (hl : Legal P0 h) : h ≠ [] := by98  cases hl <;> simp99100/-- The initial board is the last entry. -/101theorem legal_last {P0 : List Nat} {h : Hist} (hl : Legal P0 h) : h.drop (h.length - 1) = [P0] := by102  induction hl with103  | init => rfl104  | @step h Q hl' _ ih =>105    have hpos : 1 ≤ h.length := by have := legal_ne_nil hl'; cases h <;> simp_all106    simp only [List.length_cons]107    rw [show h.length + 1 - 1 = (h.length - 1) + 1 by omega, List.drop_succ_cons, ih]108109/-- Every consecutive pair of a legal history is a legal move. -/110theorem legal_pair {P0 : List Nat} {h : Hist} (hl : Legal P0 h) :111    ∀ j (hj : j + 1 < h.length), Move (cur (h.drop (j + 1))) (h[j]'(by omega)) := by112  induction hl with113  | init => intro j hj; simp at hj114  | @step h Q hl' hm ih =>115    intro j hj116    cases j with117    | zero => simpa using hm118    | succ j =>119      simp only [List.length_cons] at hj120      simp only [List.drop_succ_cons, List.getElem_cons_succ]121      exact ih j (by omega)122123/-- 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)130131theorem cons_legal {r : Role} {σ : Strat} {P0 : List Nat} {h : Hist} (hc : Cons r σ P0 h) : Legal P0 h := by132  induction hc with133  | init => exact Legal.init134  | opp _ _ hm ih => exact Legal.step ih hm135  | own _ _ _ hm ih => exact Legal.step ih hm136137/-- On a consistent history every agent step in it was the prescribed action. -/138theorem cons_own {r : Role} {σ : Strat} {P0 : List Nat} {h : Hist} (hc : Cons r σ P0 h) :139    ∀ j (hj : j + 1 < h.length), mover (h.drop (j + 1)) = r → σ (h.drop (j + 1)) = some (h[j]'(by omega)) := by140  induction hc with141  | init => intro j hj; simp at hj142  | @opp h Q hc' hne _ ih =>143    intro j hj hmv144    cases j with145    | zero => simp only [List.drop_succ_cons, List.drop_zero] at hmv; exact absurd hmv hne146    | succ j =>147      simp only [List.length_cons] at hj148      simp only [List.drop_succ_cons, List.getElem_cons_succ] at hmv ⊢149      exact ih j (by omega) hmv150  | @own h Q hc' _ hσ _ ih =>151    intro j hj hmv152    cases j with153    | zero => simpa using hσ154    | succ j =>155      simp only [List.length_cons] at hj156      simp only [List.drop_succ_cons, List.getElem_cons_succ] at hmv ⊢157      exact ih j (by omega) hmv158159/-- 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) Q164165/-- NO VACUOUS SUCCESS (1): a secure consistent history can always be continued until the166    board is terminal: on the agent's turn by its own action, on the opponent's turn by any167    legal move. -/168theorem secure_extend {r : Role} {σ : Strat} {P0 : List Nat} (hs : Secure r σ P0) {h : Hist}169    (hc : Cons r σ P0 h) (hnt : ¬ Terminal (cur h)) : ∃ Q, Cons r σ P0 (Q :: h) := by170  by_cases hm : mover h = r171  · obtain ⟨Q, hQ, hmv⟩ := hs h hc hm172    exact ⟨Q, Cons.own hc hm hQ hmv⟩173  · have : ∃ Q, Move (cur h) Q := by174      apply Classical.byContradiction; intro hno175      exact hnt ((terminal_iff_no_move _).2 (fun Q hQ => hno ⟨Q, hQ⟩))176    obtain ⟨Q, hQ⟩ := this177    exact ⟨Q, Cons.opp hc hm hQ⟩178179/-- NO VACUOUS SUCCESS (2): under the guarantee every consistent history that reaches a180    terminal board does so with the OPPONENT to move: the opponent cannot move and loses. -/181theorem secure_terminal {r : Role} {σ : Strat} {P0 : List Nat} (hs : Secure r σ P0) {h : Hist}182    (hc : Cons r σ P0 h) (ht : Terminal (cur h)) : mover h ≠ r := by183  intro hm184  obtain ⟨Q, _, hmv⟩ := hs h hc hm185  exact (terminal_iff_no_move _).1 ht Q hmv186187/-! ### Plays of strategy pairs -/188189/-- Outcome of a play for the agent. -/190inductive Outcome where191  | agentWins192  | agentLoses193  | unfinished194  deriving DecidableEq195196/-- A legal opponent strategy: whenever a legal move exists it proposes a legal move. -/197def LegalOpp (τ : Strat) : Prop := ∀ h, (∃ Q, Move (cur h) Q) → ∃ Q, τ h = some Q ∧ Move (cur h) Q198199open Classical in200/-- The play of agent σ (role r) against opponent τ, with fuel.  A player who proposes no201    action or an illegal one loses at once; in particular the player to move at a terminal202    board loses (normal play).  Legal opponents never forfeit. -/203noncomputable def play (r : Role) (σ τ : Strat) : Nat → Hist → Outcome204  | 0, _ => .unfinished205  | f + 1, h =>206    if mover h = r then207      match σ h with208      | some Q => if Move (cur h) Q then play r σ τ f (Q :: h) else .agentLoses209      | none => .agentLoses210    else211      match τ h with212      | some Q => if Move (cur h) Q then play r σ τ f (Q :: h) else .agentWins213      | none => .agentWins214215section PlayLemmas216variable {r : Role} {σ τ : Strat}217218theorem play_own {f : Nat} {h : Hist} {Q : List Nat} (hm : mover h = r) (hσ : σ h = some Q)219    (hmv : Move (cur h) Q) : play r σ τ (f + 1) h = play r σ τ f (Q :: h) := by220  simp only [play, hm, if_true, hσ, hmv]221222theorem play_own_fail {f : Nat} {h : Hist} (hm : mover h = r) (hσ : ¬ ∃ Q, σ h = some Q ∧ Move (cur h) Q) :223    play r σ τ (f + 1) h = .agentLoses := by224  simp only [play, hm, if_true]225  cases hs : σ h with226  | none => rfl227  | some Q =>228    have : ¬ Move (cur h) Q := fun hmv => hσ ⟨Q, hs, hmv⟩229    simp only [this, if_false]230231theorem play_opp {f : Nat} {h : Hist} {Q : List Nat} (hm : mover h ≠ r) (hτ : τ h = some Q)232    (hmv : Move (cur h) Q) : play r σ τ (f + 1) h = play r σ τ f (Q :: h) := by233  simp only [play, hm, if_false, hτ, hmv, if_true]234235theorem play_opp_fail {f : Nat} {h : Hist} (hm : mover h ≠ r) (hτ : ¬ ∃ Q, τ h = some Q ∧ Move (cur h) Q) :236    play r σ τ (f + 1) h = .agentWins := by237  simp only [play, hm, if_false]238  cases hs : τ h with239  | none => rfl240  | some Q =>241    have : ¬ Move (cur h) Q := fun hmv => hτ ⟨Q, hs, hmv⟩242    simp only [this, if_false]243244/-- TERMINATION: with fuel above the stone count every play finishes. -/245theorem play_finishes : ∀ (f : Nat) (h : Hist), (cur h).sum < f → play r σ τ f h ≠ .unfinished246  | 0, _, hf => by omega247  | f + 1, h, hf => by248    by_cases hm : mover h = r249    · by_cases hσ : ∃ Q, σ h = some Q ∧ Move (cur h) Q250      · obtain ⟨Q, h1, h2⟩ := hσ251        rw [play_own hm h1 h2]252        have := move_sum_lt h2253        exact play_finishes f (Q :: h) (by simp only [cur_cons]; omega)254      · rw [play_own_fail hm hσ]; simp255    · by_cases hτ : ∃ Q, τ h = some Q ∧ Move (cur h) Q256      · obtain ⟨Q, h1, h2⟩ := hτ257        rw [play_opp hm h1 h2]258        have := move_sum_lt h2259        exact play_finishes f (Q :: h) (by simp only [cur_cons]; omega)260      · rw [play_opp_fail hm hτ]; simp261262/-- The outcome does not depend on the fuel once it exceeds the stone count. -/263theorem play_fuel : ∀ (f g : Nat) (h : Hist), (cur h).sum < f → (cur h).sum < g →264    play r σ τ f h = play r σ τ g h265  | 0, _, _, hf, _ => by omega266  | _ + 1, 0, _, _, hg => by omega267  | f + 1, g + 1, h, hf, hg => by268    by_cases hm : mover h = r269    · by_cases hσ : ∃ Q, σ h = some Q ∧ Move (cur h) Q270      · obtain ⟨Q, h1, h2⟩ := hσ271        rw [play_own hm h1 h2, play_own hm h1 h2]272        have := move_sum_lt h2273        exact play_fuel f g (Q :: h) (by simp only [cur_cons]; omega) (by simp only [cur_cons]; omega)274      · rw [play_own_fail hm hσ, play_own_fail hm hσ]275    · by_cases hτ : ∃ Q, τ h = some Q ∧ Move (cur h) Q276      · obtain ⟨Q, h1, h2⟩ := hτ277        rw [play_opp hm h1 h2, play_opp hm h1 h2]278        have := move_sum_lt h2279        exact play_fuel f g (Q :: h) (by simp only [cur_cons]; omega) (by simp only [cur_cons]; omega)280      · rw [play_opp_fail hm hτ, play_opp_fail hm hτ]281282end PlayLemmas283284/-- The agent wins the play from P₀ (fuel P₀.sum + 1 suffices, play_finishes). -/285def Beats (r : Role) (σ τ : Strat) (P0 : List Nat) : Prop := play r σ τ (P0.sum + 1) [P0] = .agentWins286287/-- σ wins from P₀ in role r against EVERY legal opponent strategy. -/288def Guarantee (r : Role) (σ : Strat) (P0 : List Nat) : Prop := ∀ τ, LegalOpp τ → Beats r σ τ P0289290/-- An initially terminal board: the first player (to move) loses whatever it does, and the291    second player wins against every opponent. -/292theorem terminal_start {P0 : List Nat} (ht : Terminal P0) (σ τ : Strat) :293    play .first σ τ (P0.sum + 1) [P0] = .agentLoses ∧ play .second σ τ (P0.sum + 1) [P0] = .agentWins := by294  have hno : ∀ Q, ¬ Move P0 Q := (terminal_iff_no_move P0).1 ht295  constructor296  · exact play_own_fail (by rfl) (fun ⟨Q, _, hm⟩ => hno Q hm)297  · exact play_opp_fail (by simp) (fun ⟨Q, _, hm⟩ => hno Q hm)298299/-! ## C2. The history characterisation of the guarantee -/300301theorem secure_play {r : Role} {σ τ : Strat} {P0 : List Nat} (hs : Secure r σ P0) :302    ∀ (f : Nat) (h : Hist), Cons r σ P0 h → (cur h).sum < f → play r σ τ f h = .agentWins303  | 0, _, _, hf => by omega304  | f + 1, h, hc, hf => by305    by_cases hm : mover h = r306    · obtain ⟨Q, h1, h2⟩ := hs h hc hm307      rw [play_own hm h1 h2]308      have := move_sum_lt h2309      exact secure_play hs f (Q :: h) (Cons.own hc hm h1 h2) (by simp only [cur_cons]; omega)310    · by_cases hτ : ∃ Q, τ h = some Q ∧ Move (cur h) Q311      · obtain ⟨Q, h1, h2⟩ := hτ312        rw [play_opp hm h1 h2]313        have := move_sum_lt h2314        exact secure_play hs f (Q :: h) (Cons.opp hc hm h2) (by simp only [cur_cons]; omega)315      · exact play_opp_fail hm hτ316317theorem secure_guarantee {r : Role} {σ : Strat} {P0 : List Nat} (hs : Secure r σ P0) : Guarantee r σ P0 :=318  fun _ _ => secure_play hs (P0.sum + 1) [P0] Cons.init (by simp [cur])319320/-- The opponent that follows a given history h on its proper prefixes and otherwise plays321    the default strategy d. -/322def followD (d : Strat) (h : Hist) (g : Hist) : Option (List Nat) :=323  if g.length < h.length ∧ h.drop (h.length - g.length) = g then h[h.length - g.length - 1]? else d g324325/-- Following h, with "remove one stone from the first nonempty heap" as default. -/326def follow (h : Hist) : Strat := followD (fun g => subFirstPos (cur g)) h327328theorem subFirstPos_move {P Q : List Nat} (h : subFirstPos P = some Q) : Move P Q := by329  obtain ⟨pre, x, post, rfl, hx, rfl⟩ := subFirstPos_some h330  exact ⟨pre, x, post, x - 1, rfl, rfl, by omega⟩331332theorem subFirstPos_isSome {P : List Nat} (h : ∃ Q, Move P Q) : ∃ Q, subFirstPos P = some Q := by333  cases hs : subFirstPos P with334  | some Q => exact ⟨Q, rfl⟩335  | none =>336    obtain ⟨Q, hQ⟩ := h337    exact absurd hQ ((terminal_iff_no_move P).1 (subFirstPos_none hs) Q)338339theorem subFirst_legal : LegalOpp (fun g => subFirstPos (cur g)) := by340  intro g hex341  obtain ⟨Q, hQ⟩ := subFirstPos_isSome hex342  exact ⟨Q, hQ, subFirstPos_move hQ⟩343344theorem followD_legal {P0 : List Nat} {h : Hist} (hl : Legal P0 h) {d : Strat} (hd : LegalOpp d) :345    LegalOpp (followD d h) := by346  intro g hex347  unfold followD348  by_cases hc : g.length < h.length ∧ h.drop (h.length - g.length) = g349  · rw [if_pos hc]350    have hpos : 1 ≤ h.length - g.length := by omega351    have hmv := legal_pair hl (h.length - g.length - 1) (by352      have : 0 < g.length := by353        obtain ⟨Q, hQ⟩ := hex354        cases g with355        | nil => obtain ⟨pre, x, post, y, hp, _, _⟩ := hQ; simp [cur] at hp356        | cons _ _ => simp357      omega)358    have hdrop : h.drop (h.length - g.length - 1 + 1) = g := by359      rw [show h.length - g.length - 1 + 1 = h.length - g.length by omega]; exact hc.2360    rw [hdrop] at hmv361    exact ⟨_, List.getElem?_eq_getElem (by omega), hmv⟩362  · rw [if_neg hc]; exact hd g hex363364theorem follow_legal {P0 : List Nat} {h : Hist} (hl : Legal P0 h) : LegalOpp (follow h) :=365  followD_legal hl subFirst_legal366367/-- The play against `followD d h` runs along h (whatever the default d). -/368theorem followD_play {r : Role} {σ : Strat} {P0 : List Nat} {h : Hist} (d : Strat) (hc : Cons r σ P0 h) :369    ∀ (j : Nat) (hj : j < h.length) (f : Nat),370      play r σ (followD d h) (f + j) (h.drop j) = play r σ (followD d h) f h371  | 0, _, f => by simp372  | j + 1, hj, f => by373    have hl := cons_legal hc374    have hmv := legal_pair hl j hj375    have hsplit : h.drop j = h[j] :: h.drop (j + 1) := List.drop_eq_getElem_cons (by omega)376    rw [show f + (j + 1) = (f + j) + 1 by omega]377    by_cases hm : mover (h.drop (j + 1)) = r378    · have hσ := cons_own hc j hj hm379      rw [play_own hm hσ hmv, ← hsplit]380      exact followD_play d hc j (by omega) f381    · have hτ : followD d h (h.drop (j + 1)) = some h[j] := by382        unfold followD383        have hlen : (h.drop (j + 1)).length = h.length - (j + 1) := List.length_drop384        rw [if_pos ⟨by omega, by rw [hlen, show h.length - (h.length - (j + 1)) = j + 1 by omega]⟩, hlen,385          show h.length - (h.length - (j + 1)) - 1 = j by omega]386        exact List.getElem?_eq_getElem (by omega)387      rw [play_opp hm hτ hmv, ← hsplit]388      exact followD_play d hc j (by omega) f389390theorem follow_play {r : Role} {σ : Strat} {P0 : List Nat} {h : Hist} (hc : Cons r σ P0 h) :391    ∀ (j : Nat) (hj : j < h.length) (f : Nat), play r σ (follow h) (f + j) (h.drop j) = play r σ (follow h) f h :=392  followD_play _ hc393394/-- Running a play from P₀ against `followD d h` up to the end of h. -/395theorem followD_reach {r : Role} {σ : Strat} {P0 : List Nat} {h : Hist} (d : Strat) (hc : Cons r σ P0 h) :396    play r σ (followD d h) (P0.sum + 1) [P0] =397      play r σ (followD d h) ((P0.sum + 1 - h.length) + 1) h := by398  have hl := cons_legal hc399  have hsum := legal_sum hl400  have hne := legal_ne_nil hl401  have hlen : 1 ≤ h.length := by cases h <;> simp_all402  have e := followD_play d hc (h.length - 1) (by omega) (P0.sum + 1 - (h.length - 1))403  rw [show P0.sum + 1 - (h.length - 1) + (h.length - 1) = P0.sum + 1 by omega, legal_last hl] at e404  rw [e, show P0.sum + 1 - (h.length - 1) = (P0.sum + 1 - h.length) + 1 by omega]405406/-- 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 hb416417/-! ### Winnable roles -/418419/-- 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 σ P0421422/-- The optimal opponent: move to nim-sum 0 when possible, otherwise any legal move. -/423def optOpp : Strat := fun h => selectMove (nimSum (cur h)) (cur h)424425theorem optOpp_legal : LegalOpp optOpp := by426  intro h hex427  cases hs : selectMove (nimSum (cur h)) (cur h) with428  | none =>429    obtain ⟨Q, hQ⟩ := hex430    exact absurd hQ ((terminal_iff_no_move _).1 ((selectMove_none_iff _ _).1 hs) Q)431  | some Q => exact ⟨Q, hs, selectMove_legal hs⟩432433/-- Against the optimal opponent the agent loses from every history where it faces nim-sum434    0 on its turn (or the opponent faces a nonzero nim-sum on its turn). -/435theorem optOpp_play {r : Role} {σ : Strat} : ∀ (f : Nat) (h : Hist), (cur h).sum < f →436    (mover h = r → nimSum (cur h) = 0) → (mover h ≠ r → nimSum (cur h) ≠ 0) →437    play r σ optOpp f h = .agentLoses438  | 0, _, hf, _, _ => by omega439  | f + 1, h, hf, h1, h2 => by440    by_cases hm : mover h = r441    · by_cases hσ : ∃ Q, σ h = some Q ∧ Move (cur h) Q442      · obtain ⟨Q, hQ, hmv⟩ := hσ443        rw [play_own hm hQ hmv]444        have := move_sum_lt hmv445        exact optOpp_play f (Q :: h) (by simp only [cur_cons]; omega)446          (fun hm' => absurd hm' (mover_cons_ne hm)) (fun _ => move_from_zero hmv (h1 hm))447      · exact play_own_fail hm hσ448    · obtain ⟨Q, hsel, hmv, hz⟩ := selectMove_zero (h2 hm)449      rw [play_opp hm (show optOpp h = some Q from hsel) hmv]450      have := move_sum_lt hmv451      exact optOpp_play f (Q :: h) (by simp only [cur_cons]; omega) (fun _ => hz)452        (fun hm' => absurd (mover_cons_eq hm) hm')453454/-- The same for any opponent that plays like optOpp on all histories of length ≥ k. -/455theorem optLike_play {r : Role} {σ τ : Strat} {k : Nat} (hτ : ∀ g : Hist, k ≤ g.length → τ g = optOpp g) :456    ∀ (f : Nat) (h : Hist), k ≤ h.length → (cur h).sum < f →457    (mover h = r → nimSum (cur h) = 0) → (mover h ≠ r → nimSum (cur h) ≠ 0) → play r σ τ f h = .agentLoses458  | 0, _, _, hf, _, _ => by omega459  | f + 1, h, hk, hf, h1, h2 => by460    by_cases hm : mover h = r461    · by_cases hσ : ∃ Q, σ h = some Q ∧ Move (cur h) Q462      · obtain ⟨Q, hQ, hmv⟩ := hσ463        rw [play_own hm hQ hmv]464        have := move_sum_lt hmv465        exact optLike_play hτ f (Q :: h) (by simp; omega) (by simp only [cur_cons]; omega)466          (fun hm' => absurd hm' (mover_cons_ne hm)) (fun _ => move_from_zero hmv (h1 hm))467      · exact play_own_fail hm hσ468    · obtain ⟨Q, hsel, hmv, hz⟩ := selectMove_zero (h2 hm)469      rw [play_opp hm (show τ h = some Q by rw [hτ h hk]; exact hsel) hmv]470      have := move_sum_lt hmv471      exact optLike_play hτ f (Q :: h) (by simp; omega) (by simp only [cur_cons]; omega) (fun _ => hz)472        (fun hm' => absurd (mover_cons_eq hm) hm')473474/-- THE GUARANTEE FORCES WINNING MOVES ON CONSISTENT HISTORIES: if σ wins from P₀ against475    every legal opponent, then at every policy-consistent history where it is to move it476    plays a legal move to a P-position (nim-sum 0).  (Otherwise the opponent that follows477    that history and then plays optimally wins.) -/478theorem guarantee_optimal {r : Role} {σ : Strat} {P0 : List Nat} (hg : Guarantee r σ P0) {h : Hist}479    (hc : Cons r σ P0 h) (hm : mover h = r) : ∃ Q, σ h = some Q ∧ Move (cur h) Q ∧ nimSum Q = 0 := by480  obtain ⟨Q, hQ, hmv⟩ := (secure_iff_guarantee r σ P0).2 hg h hc hm481  refine ⟨Q, hQ, hmv, Classical.byContradiction (fun hz => ?_)⟩482  have hl := cons_legal hc483  have hb := hg (followD optOpp h) (followD_legal hl optOpp_legal)484  unfold Beats at hb485  rw [followD_reach _ hc] at hb486  have hsum := legal_sum hl487  have hs := move_sum_lt hmv488  cases hf : P0.sum + 1 - h.length with489  | zero => omega490  | succ f =>491    rw [hf, play_own hm hQ hmv] at hb492    have hτ : ∀ g : Hist, h.length + 1 ≤ g.length → followD optOpp h g = optOpp g := by493      intro g hg'; unfold followD; rw [if_neg (by omega)]494    rw [optLike_play hτ (f + 1) (Q :: h) (by simp) (by simp only [cur_cons]; omega)495      (fun hm' => absurd hm' (mover_cons_ne hm)) (fun _ => hz)] at hb496    cases hb497498/-- The memoryless strategy defined by a board selector. -/499def ofSel (sel : List Nat → Option (List Nat)) : Strat := fun h => sel (cur h)500501/-- C3 BRIDGE (first player): a NimGame.Wins certificate gives the history guarantee. -/502theorem wins_secure {sel : List Nat → Option (List Nat)} {P0 : List Nat} (hw : Wins sel P0) :503    Secure .first (ofSel sel) P0 := by504  have inv : ∀ h, Cons .first (ofSel sel) P0 h →505      (mover h = .first → Wins sel (cur h)) ∧ (mover h ≠ .first → ∃ P, Wins sel P ∧ sel P = some (cur h) ∧506        ∀ R, Move (cur h) R → Wins sel R) := by507    intro h hc508    induction hc with509    | init => exact ⟨fun _ => hw, fun h => absurd rfl h⟩510    | @opp h Q hc' hne hmv ih =>511      obtain ⟨P, _, _, hall⟩ := (ih.2 hne)512      exact ⟨fun _ => hall Q hmv, fun h' => absurd (mover_cons_eq hne) h'⟩513    | @own h Q hc' hm hσ hmv ih =>514      have hW := ih.1 hm515      refine ⟨fun h' => absurd h' (mover_cons_ne hm), fun _ => ?_⟩516      cases hW with517      | intro p q hs hm' hall =>518        have hq : q = Q := by unfold ofSel at hσ; rw [hs] at hσ; exact Option.some.inj hσ519        subst hq520        exact ⟨cur h, Wins.intro _ q hs hm' hall, hs, hall⟩521  intro h hc hm522  have hW := (inv h hc).1 hm523  cases hW with524  | intro p q hs hm' _ => exact ⟨q, hs, hm'⟩525526/-- C3 BRIDGE (second player): a Misc.SecondWins certificate gives the history guarantee. -/527theorem secondWins_secure {sel : List Nat → Option (List Nat)} {P0 : List Nat} (hw : SecondWins sel P0) :528    Secure .second (ofSel sel) P0 := by529  have inv : ∀ h, Cons .second (ofSel sel) P0 h →530      (mover h ≠ .second → SecondWins sel (cur h)) ∧531      (mover h = .second → ∃ P, SecondWins sel P ∧ Move P (cur h)) := by532    intro h hc533    induction hc with534    | init => exact ⟨fun _ => hw, fun h => by simp at h⟩535    | @opp h Q hc' hne hmv ih =>536      exact ⟨fun h' => absurd (mover_cons_eq hne) h', fun _ => ⟨cur h, ih.1 hne, hmv⟩⟩537    | @own h Q hc' hm hσ hmv ih =>538      obtain ⟨P, hP, hPm⟩ := ih.2 hm539      refine ⟨fun _ => ?_, fun h' => absurd h' (mover_cons_ne hm)⟩540      cases hP with541      | intro _ _ _ hrest => exact hrest (cur h) Q hPm hσ542  intro h hc hm543  obtain ⟨P, hP, hPm⟩ := (inv h hc).2 hm544  cases hP with545  | intro _ hsome hmove _ =>546    cases hs : sel (cur h) with547    | none => have := hsome (cur h) hPm; rw [hs] at this; cases this548    | some Q => exact ⟨Q, hs, hmove (cur h) Q hPm hs⟩549550/-- The canonical second-player selector (restore nim-sum 0). -/551def zeroSel (Q : List Nat) : Option (List Nat) := selectMove (nimSum Q) Q552553theorem zeroSel_wins : ∀ P : List Nat, nimSum P = 0 → SecondWins zeroSel P := by554  intro P555  induction P using (measure List.sum).wf.induction with556  | h P ih =>557    intro h0558    have key : ∀ Q, Move P Q → ∃ R, zeroSel Q = some R ∧ Move Q R ∧ nimSum R = 0 :=559      fun Q hm => selectMove_zero (move_from_zero hm h0)560    refine SecondWins.intro P (fun Q hm => ?_) (fun Q R hm hR => ?_) (fun Q R hm hR => ?_)561    · obtain ⟨R, h1, _⟩ := key Q hm; rw [h1]; rfl562    · obtain ⟨R', h1, h2, _⟩ := key Q hm; rw [h1] at hR; cases hR; exact h2563    · obtain ⟨R', h1, h2, h3⟩ := key Q hm564      have e : R' = R := Option.some.inj (h1.symm.trans hR)565      subst e566      have := move_sum_lt hm; have := move_sum_lt h2567      exact ih R' (by show R'.sum < P.sum; omega) h3568569theorem le_sum_of_mem {x : Nat} : ∀ {P : List Nat}, x ∈ P → x ≤ P.sum570  | [], h => by simp at h571  | y :: P, h => by572    rcases List.mem_cons.mp h with rfl | h573    · simp574    · have := le_sum_of_mem h; simp; omega575576theorem width_sum (P : List Nat) : Width P.sum P :=577  fun x hx => Nat.lt_of_le_of_lt (le_sum_of_mem hx) Nat.lt_two_pow_self578579/-- 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))⟩591592theorem roleWinnable_second (P0 : List Nat) : RoleWinnable .second P0 ↔ nimSum P0 = 0 := by593  constructor594  · rintro ⟨σ, hg⟩595    apply Classical.byContradiction; intro h0596    have := hg optOpp optOpp_legal597    unfold Beats at this598    rw [optOpp_play (r := .second) (σ := σ) (P0.sum + 1) [P0] (by simp [cur]) (fun h => by simp at h)599      (fun _ => h0)] at this600    cases this601  · intro h602    exact ⟨ofSel zeroSel, secure_guarantee (secondWins_secure (zeroSel_wins P0 h))⟩603604theorem roleWinnable_game (P0 : List Nat) :605    (RoleWinnable .first P0 ↔ Win P0) ∧ (RoleWinnable .second P0 ↔ Lose P0) :=606  ⟨by rw [roleWinnable_first, win_iff], by rw [roleWinnable_second, lose_iff]⟩607608/-- Exactly one role is winnable from each board. -/609theorem roleWinnable_exclusive (P0 : List Nat) : RoleWinnable .first P0 ↔ ¬ RoleWinnable .second P0 := by610  rw [roleWinnable_first, roleWinnable_second]611612/-! ## C2. Weak mastery -/613614/-- 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 σ P0619620/-- Indexed families (e.g. by bit width B), with an index-dependent policy. -/621def WeakMasteryFam {ι : Type} (F : ι → List Nat → Prop) (r : Role) (σ : ι → Strat) : Prop :=622  ∀ i, WeakMastery (F i) r (σ i)623624/-- Unfolded form: in nim-sum terms and with the history guarantee. -/625theorem weakMastery_iff (F : List Nat → Prop) (r : Role) (σ : Strat) :626    WeakMastery F r σ ↔627      ∀ P0, F P0 → (if r = .first then nimSum P0 ≠ 0 else nimSum P0 = 0) → Secure r σ P0 := by628  have hw : ∀ P0, RoleWinnable r P0 ↔ (if r = .first then nimSum P0 ≠ 0 else nimSum P0 = 0) := by629    intro P0; cases r630    · simp [roleWinnable_first]631    · simp [roleWinnable_second]632  constructor633  · intro h P0 hF hc; exact (secure_iff_guarantee r σ P0).2 (h P0 hF ((hw P0).2 hc))634  · intro h P0 hF hc; exact (secure_iff_guarantee r σ P0).1 (h P0 hF ((hw P0).1 hc))635636/-- 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)643644theorem weakMastery_restrict (F : List Nat → Prop) (r : Role) (σ : Strat) :645    WeakMastery F r σ ↔ WeakMastery (fun P => F P ∧ RoleWinnable r P) r σ :=646  ⟨fun h P0 hF hw => h P0 hF.1 hw, fun h P0 hF hw => h P0 ⟨hF, hw⟩ hw⟩647648/-- 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⟩)659660/-! ## C3. Instances -/661662/-- PAIRING (second player): from every paired board of width B (all of which are663    P-positions, so the second role IS winnable), the binary mirror selector pairSel B664    wins against every legal opponent strategy. -/665theorem pairing_guarantee {B : Nat} {P0 : List Nat} (hp : Paired P0) (hw : Width B P0) :666    RoleWinnable .second P0 ∧ Guarantee .second (ofSel (pairSel B)) P0 :=667  ⟨(roleWinnable_second P0).2 (paired_lose hp hw).2,668   secure_guarantee (secondWins_secure (pairing_wins P0 hp hw))⟩669670theorem pairing_weak : WeakMasteryFam (fun B P => Paired P ∧ Width B P) .second (fun B => ofSel (pairSel B)) :=671  fun _ P0 hF _ => (pairing_guarantee hF.1 hF.2).2672673/-- For the first role the paired family is losing, so weak mastery there is vacuous. -/674theorem pairing_first_vacuous (B : Nat) (σ : Strat) : WeakMastery (fun P => Paired P ∧ Width B P) .first σ :=675  weakMastery_vacuous (fun P0 hF hw => (roleWinnable_first P0).1 hw (paired_lose hF.1 hF.2).2) σ676677/-- The compiled threshold network of the mirror selector, and its reply rule. -/678def pairNet (B N r : Nat) : List AC0.Layer := ThresholdInst.binNet (pairBin B N r)679def pairNetSel (B : Nat) (Q : List Nat) : Option (List Nat) :=680  SelectCircuit.applyM Q (ThresholdInst.netBinSem (pairNet B Q.length (rIdx Q.length)) Q.length (rIdx Q.length) B681    (CorrBridge.boardBits B Q))682683/-- The network reply rule IS the binary selector's rule, on every board. -/684theorem pairNetSel_eq (B : Nat) : pairNetSel B = pairSel B := by685  funext Q686  unfold pairNetSel pairSel pairNet687  rw [ThresholdInst.binNet_correct (pairBin B Q.length (rIdx Q.length))688    (by simp [pairBin, PriorityEncoder.encode]) (by simp [pairBin, PriorityEncoder.encode, pairR])]689690theorem pairing_net_weak :691    WeakMasteryFam (fun B P => Paired P ∧ Width B P) .second (fun B => ofSel (pairNetSel B)) := by692  intro B693  show WeakMastery _ _ (ofSel (pairNetSel B))694  rw [pairNetSel_eq]; exact pairing_weak B695696/-- The resources certified in phase 6 are for the same binary selector: depth, size and697    reads of pairBin B N r (N even, N ≤ 2^r), and the network compiled from it. -/698theorem pairing_resources (B N : Nat) (hN : N % 2 = 0) :699    PriorityEncoder.BinBound (pairBin B N (rIdx N)) N B (rIdx N) 10700      (4 * ((N + 2) * (N * (2 * pairF B + 1) + 1 + 2)) ^ 3) (B * N) ∧701    AC0.NetValid 1 (pairNet B N (rIdx N)) ∧ FiniteNet.Wired (B * N) (pairNet B N (rIdx N)) ∧702    (pairNet B N (rIdx N)).length ≤ 2 * 10 + 2 :=703  have hb := pairBin_bound B N (rIdx N) (Family.rIdx_width N) hN704  have hn := ThresholdInst.binNet_res hb705  ⟨hb, hn.1, hn.2.1, hn.2.2.1⟩706707/-- MULTI-HEAD (first player): the network-driven multi-head player is weakly masterful on708    every B-bit family for the first role. -/709theorem mh_weak : WeakMasteryFam (fun B P => Width B P) .first (fun B => ofSel (mhSelect B)) := by710  intro B P0 hw hwin711  exact secure_guarantee (wins_secure (mhSelect_wins hw ((roleWinnable_first P0).1 hwin)))712713/-- The history-dependent two-frame strategy: answer the opponent's move Q → Q' by714    reply Q Q' (Q = the board before the opponent's move). -/715def twoFrameStrat (reply : List Nat → List Nat → Option (List Nat)) : Strat716  | Q' :: Q :: _ => reply Q Q'717  | _ => none718719/-- C3 BRIDGE (stateful second player): WholeGame.TwoFrameWins gives the history720    guarantee.  The predecessor read by the strategy is, on consistent histories, the721    board established by the agent's own previous action (or P₀). -/722theorem twoFrame_secure {reply : List Nat → List Nat → Option (List Nat)} {P0 : List Nat}723    (hw : TwoFrameWins reply P0) : Secure .second (twoFrameStrat reply) P0 := by724  have inv : ∀ h, Cons .second (twoFrameStrat reply) P0 h →725      (mover h ≠ .second → TwoFrameWins reply (cur h)) ∧726      (mover h = .second → ∃ Q Q' t, h = Q' :: Q :: t ∧ TwoFrameWins reply Q ∧ Move Q Q') := by727    intro h hc728    induction hc with729    | init => exact ⟨fun _ => hw, fun h => by simp at h⟩730    | @opp h Q' hc' hne hmv ih =>731      refine ⟨fun h' => absurd (mover_cons_eq hne) h', fun _ => ?_⟩732      have hne' := legal_ne_nil (cons_legal hc')733      obtain ⟨Q, t, rfl⟩ : ∃ Q t, h = Q :: t := by cases h with734        | nil => exact absurd rfl hne'735        | cons Q t => exact ⟨Q, t, rfl⟩736      exact ⟨Q, Q', t, rfl, ih.1 hne, hmv⟩737    | @own h R hc' hm hσ hmv ih =>738      obtain ⟨Q, Q', t, rfl, hT, hQm⟩ := ih.2 hm739      refine ⟨fun _ => ?_, fun h' => absurd h' (mover_cons_ne hm)⟩740      cases hT with741      | intro _ _ _ hrest => exact hrest Q' R hQm hσ742  intro h hc hm743  obtain ⟨Q, Q', t, rfl, hT, hQm⟩ := (inv h hc).2 hm744  cases hT with745  | intro _ hsome hmove _ =>746    cases hs : reply Q Q' with747    | none => have := hsome Q' hQm; rw [hs] at this; cases this748    | some R => exact ⟨R, hs, hmove Q' R hQm hs⟩749750/-- TWO-FRAME RESTORATION (second player, history-dependent): the player that feeds the751    previous board and the current board to the compiled LOCAL restoration network is752    weakly masterful on every B-bit family for the second role. -/753theorem twoFrame_weak : WeakMasteryFam (fun B P => Width B P) .second (fun B => twoFrameStrat (restReply B)) := by754  intro B P0 hw hwin755  exact secure_guarantee (twoFrame_secure (twoFrame_wins P0 hw ((roleWinnable_second P0).1 hwin)))756757/-- STATE OF THE TWO-FRAME PLAYER: on every consistent history at the agent's turn, the758    predecessor it reads is either P₀ (first reply) or the board produced by its own759    previous action.  So the strategy needs one stored board (its last established board,760    as in WholeGame), not an oracle for the opponent's history. -/761theorem twoFrame_memory {reply : List Nat → List Nat → Option (List Nat)} {P0 : List Nat} {h : Hist}762    (hc : Cons .second (twoFrameStrat reply) P0 h) (hm : mover h = .second) :763    ∃ Q' Q t, h = Q' :: Q :: t ∧ ((t = [] ∧ Q = P0) ∨ twoFrameStrat reply t = some Q) := by764  cases hc with765  | init => simp at hm766  | own _ hm' _ _ => exact absurd hm (mover_cons_ne hm')767  | @opp g Q' hc' hne _ =>768    cases hc' with769    | init => exact ⟨Q', P0, [], rfl, Or.inl ⟨rfl, rfl⟩⟩770    | @opp t Q _ hne' _ => exact absurd (mover_cons_eq hne') hne771    | @own t Q _ _ hσ _ => exact ⟨Q', Q, t, rfl, Or.inr hσ⟩772773/-! ## C4. Locality, strong versus weak mastery -/774775/-- LOCALITY: if σ' agrees with σ on every σ-consistent history at the agent's turn, the two776    strategies have exactly the same consistent histories. -/777theorem cons_congr {r : Role} {σ σ' : Strat} {P0 : List Nat}778    (hag : ∀ h, Cons r σ P0 h → mover h = r → σ' h = σ h) (h : Hist) :779    Cons r σ P0 h ↔ Cons r σ' P0 h := by780  constructor781  · intro hc782    induction hc with783    | init => exact Cons.init784    | opp _ hne hmv ih => exact Cons.opp ih hne hmv785    | @own h Q hc' hm hσ hmv ih => exact Cons.own ih hm (by rw [hag h hc' hm]; exact hσ) hmv786  · intro hc787    induction hc with788    | init => exact Cons.init789    | opp _ hne hmv ih => exact Cons.opp ih hne hmv790    | @own h Q hc' hm hσ hmv ih => exact Cons.own ih hm (by rw [← hag h ih hm]; exact hσ) hmv791792/-- LOCALITY OF THE GUARANTEE: changing a policy only at histories that are not reachable793    consistently with its own preceding actions (for instance after a counterfactual agent794    mistake) does not affect its winning guarantee. -/795theorem guarantee_congr {r : Role} {σ σ' : Strat} {P0 : List Nat}796    (hag : ∀ h, Cons r σ P0 h → mover h = r → σ' h = σ h) :797    Guarantee r σ P0 ↔ Guarantee r σ' P0 := by798  rw [← secure_iff_guarantee, ← secure_iff_guarantee]799  constructor800  · intro hs h hc hm801    have hc' := (cons_congr hag h).2 hc802    rw [hag h hc' hm]; exact hs h hc' hm803  · intro hs h hc hm804    rw [← hag h hc hm]; exact hs h ((cons_congr hag h).1 hc) hm805806theorem weakMastery_congr {F : List Nat → Prop} {r : Role} {σ σ' : Strat}807    (hag : ∀ P0, F P0 → RoleWinnable r P0 → ∀ h, Cons r σ P0 h → mover h = r → σ' h = σ h) :808    WeakMastery F r σ ↔ WeakMastery F r σ' :=809  ⟨fun hw P0 hF hr => (guarantee_congr (hag P0 hF hr)).1 (hw P0 hF hr),810   fun hw P0 hF hr => (guarantee_congr (hag P0 hF hr)).2 (hw P0 hF hr)⟩811812/-- 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 = 0818819theorem 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⟩838839theorem legal_width {B : Nat} {P0 : List Nat} {h : Hist} (hl : Legal P0 h) (hw : Width B P0) :840    Width B (cur h) := by841  induction hl with842  | init => exact hw843  | step _ hm ih => exact width_move ih hm844845/-- The multi-head player is in fact STRONGLY masterful on B-bit families, for both roles. -/846theorem mh_strong (B : Nat) (r : Role) : StrongMastery (fun P => Width B P) r (ofSel (mhSelect B)) := by847  intro P0 hw h hl _ hnz848  have hwh : Width B (cur h) := legal_width hl hw849  obtain ⟨i, v, hd, hz⟩ := (Controller.decision_correct (cur h)).2.2 hnz850  obtain ⟨x, _, _, hmv⟩ := (Controller.decision_correct (cur h)).2.1 i v hd851  refine ⟨(cur h).set i v, ?_, hmv, hz⟩852  unfold ofSel; rw [mhSelect_eq hwh]; simp [Controller.ctrlSel, hd]853854/-- 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 none857858theorem 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⟩⟩877878/-- … 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 hQ886887/-! ## Axiom checks -/888#print axioms Role.other_ne889#print axioms Role.eq_other_of_ne890#print axioms cur_cons891#print axioms mover_cons892#print axioms mover_init893#print axioms mover_cons_eq894#print axioms mover_cons_ne895#print axioms legal_sum896#print axioms legal_length897#print axioms legal_ne_nil898#print axioms legal_last899#print axioms legal_pair900#print axioms cons_legal901#print axioms cons_own902#print axioms secure_extend903#print axioms secure_terminal904#print axioms play_own905#print axioms play_own_fail906#print axioms play_opp907#print axioms play_opp_fail908#print axioms play_finishes909#print axioms play_fuel910#print axioms terminal_start911#print axioms secure_play912#print axioms secure_guarantee913#print axioms subFirstPos_move914#print axioms subFirstPos_isSome915#print axioms subFirst_legal916#print axioms followD_legal917#print axioms follow_legal918#print axioms followD_play919#print axioms follow_play920#print axioms followD_reach921#print axioms secure_iff_guarantee922#print axioms optOpp_legal923#print axioms optOpp_play924#print axioms optLike_play925#print axioms guarantee_optimal926#print axioms wins_secure927#print axioms secondWins_secure928#print axioms zeroSel_wins929#print axioms le_sum_of_mem930#print axioms width_sum931#print axioms roleWinnable_first932#print axioms roleWinnable_second933#print axioms roleWinnable_game934#print axioms roleWinnable_exclusive935#print axioms weakMastery_iff936#print axioms weakMastery_vacuous937#print axioms weakMastery_restrict938#print axioms weakMastery_iff_optimal939#print axioms pairing_guarantee940#print axioms pairing_weak941#print axioms pairing_first_vacuous942#print axioms pairNetSel_eq943#print axioms pairing_net_weak944#print axioms pairing_resources945#print axioms mh_weak946#print axioms twoFrame_secure947#print axioms twoFrame_weak948#print axioms twoFrame_memory949#print axioms cons_congr950#print axioms guarantee_congr951#print axioms weakMastery_congr952#print axioms strong_weak953#print axioms legal_width954#print axioms mh_strong955#print axioms sep3_weak956#print axioms sep3_not_strong957958end Mastery959end NimAudit