Section 5.5, “From a summary to a move”Replay protocol rows,SEP,rows,SEP: 2N+2 updates, 4+5B+3r state bits, a legal winning move

274/-- REPLAY EXTRACTION IS CORRECT.  With sigma = nim(P) from the first scan:275    the replay move is none iff P is terminal; every move is legal; and if276    sigma ≠ 0 the move reaches nim-sum zero. -/277theorem replay_correct (P : List Nat) :278    (replayMove (nimSum P) P = none ↔ Terminal P) ∧279    (∀ i v, replayMove (nimSum P) P = some (i, v) → ∃ x, P[i]? = some x ∧ v < x) ∧280    (nimSum P ≠ 0 → ∃ i v, replayMove (nimSum P) P = some (i, v) ∧ nimSum (P.set i v) = 0) := by281  rw [replayMove_eq]282  refine ⟨?_, ?_, ?_⟩283  · constructor284    · intro h285      unfold firstSome at h286      split at h287      · cases h288      · exact decIdx_none h289    · intro ht290      rw [terminal_nimSum_zero ht]291      simp [selFor, firstSome, decIdx_terminal ht]292  · intro i v h293    unfold firstSome at h294    split at h295    · next m hm =>296      cases h297      unfold selFor at hm298      split at hm299      · cases hm300      · obtain ⟨x, hx, rfl, hlt⟩ := cancelIdx_some hm301        exact ⟨x, hx, hlt⟩302    · obtain ⟨x, hx, rfl, hlt⟩ := decIdx_some h303      exact ⟨x, hx, by omega⟩304  · intro h0305    obtain ⟨pre, x, post, hp, hlt, _⟩ := exists_decreasing_heap P h0306    cases hc : cancelIdx (nimSum P) P with307    | none => exact absurd hlt (cancelIdx_none hc x (by rw [hp]; simp))308    | some m =>309      obtain ⟨i, v⟩ := m310      obtain ⟨y, hy, rfl, _⟩ := cancelIdx_some hc311      refine ⟨i, y ^^^ nimSum P, ?_, ?_⟩312      · simp [selFor, h0, hc, firstSome]313      · rw [nimSum_set _ hy, Nat.xor_assoc, xor_cancel_left]314        exact Nat.xor_self _

132/-- ONE DECISION: from an idle state, the controller emits the summary and then the133    move computed by replay FROM THE STORED SUMMARY, and returns to an idle state that134    retains the summary. -/135theorem crun_decision (s : CState) (hs : Idle s) (P : List Nat) :136    crun s (dtoks P) =137      (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩,138       [COut.summary (nimSum P) (if s.valid then some (s.prev ^^^ nimSum P) else none),139        COut.move (replayMove (nimSum P) P)]) := by140  obtain ⟨hm, ha, hi, hsel, hf⟩ := hs141  unfold dtoks142  rw [crun_append, crun_append, crun_append, crun_scan_rows s hm]143  simp only [crun, cstep, Bool.false_eq_true, if_false, ha, Nat.zero_xor, Option.toList]144  rw [crun_replay_rows _ rfl]145  simp only [crun, cstep, if_true, Option.toList, List.nil_append, List.append_nil,146    List.cons_append, List.singleton_append]147  unfold replayMove148  simp

223/-- WINNING AGAINST EVERY LEGAL OPPONENT (checked game semantics): from every board224    with nonzero nim-sum, the controller's decisions win. -/225theorem ctrl_wins (P : List Nat) (h : nimSum P ≠ 0) : Wins ctrlSel P := by226  obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h227  obtain ⟨x, hx, hlt, hm⟩ := (decision_correct P).2.1 i v hd228  refine Wins.intro P (P.set i v) (by simp [ctrlSel, hd]) hm ?_229  intro r hr230  have h1 := move_sum_lt hm231  have h2 := move_sum_lt hr232  exact ctrl_wins r (move_from_zero hr hz)233termination_by P.sum

324/-- REACHABLE-STATE BOUNDS: along a well-formed stream of boards of N heaps below 2^B,325    started from an idle fitting state, EVERY visited state has acc, prev, sig < 2^B,326    counter ≤ N, and selected/fallback moves with index < N and value < 2^B.  With327    N < 2^r, every register fits its r- or B-bit field; the counter never overflows. -/328theorem stream_fits {B N : Nat} (s : CState) (hs : Idle s) (hf : Fits B N s) (Ps : List (List Nat))329    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) : ∀ st ∈ crunStates s (stream Ps), Fits B N st := by330  induction Ps generalizing s with331  | nil => intro st h; simp [stream, crunStates] at h; subst h; exact hf332  | cons P Ps ih =>333    have e : stream (P :: Ps) = dtoks P ++ stream Ps := by simp [stream]334    rw [e]335    intro st h336    obtain ⟨hlenP, hwP⟩ := hP P (by simp)337    rcases crunStates_append s _ _ st h with h1 | h1338    · -- inside the decision339      unfold dtoks at h1340      rcases crunStates_append s _ _ st h1 with h2 | h2341      · rcases crunStates_append s _ _ st h2 with h3 | h3342        · rcases crunStates_append s _ _ st h3 with h4 | h4343          · exact scan_rows_fit s hs.1 hf P hwP st h4344          · rw [crun_scan_rows s hs.1] at h4345            simp only [crunStates, cstep, Bool.false_eq_true, if_false, List.mem_cons,346              List.mem_singleton] at h4347            have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)348            rcases h4 with rfl | rfl | h4349            · exact ⟨ha, hf.2.1, hf.2.2.1, hf.2.2.2.1, hf.2.2.2.2.1, hf.2.2.2.2.2⟩350            · exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩351            · simp at h4352        · rw [crun_append, crun_scan_rows s hs.1] at h3353          simp only [crun, cstep, Bool.false_eq_true, if_false] at h3354          have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)355          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P356            (by simp [hlenP]) hwP st h3357      · rw [crun_append, crun_append, crun_scan_rows s hs.1] at h2358        simp only [crun, cstep, Bool.false_eq_true, if_false] at h2359        have ha : s.acc ^^^ nimSum P < 2 ^ B := Nat.xor_lt_two_pow hf.1 (nimSum_lt hwP)360        generalize hS1 : (⟨true, 0, s.acc ^^^ nimSum P, true, s.acc ^^^ nimSum P, 0, none, none⟩ :361          CState) = S1 at h2362        have hS1m : S1.replayMode = true := by rw [← hS1]363        simp only [crunStates, List.mem_cons, List.mem_singleton] at h2364        rcases h2 with rfl | rfl | h2365        · subst hS1366          exact replay_rows_fit _ rfl ⟨Nat.two_pow_pos B, ha, ha⟩ (by simp) (by simp) P367            (by simp [hlenP]) hwP _ (crun_mem_states _ _)368        · rw [crun_replay_rows _ hS1m]369          subst hS1370          simp only [cstep, if_true]371          exact ⟨Nat.two_pow_pos B, ha, ha, Nat.zero_le _, by simp, by simp⟩372        · simp at h2373    · rw [crun_decision s hs P] at h1374      have hidle : Idle (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=375        ⟨rfl, rfl, rfl, rfl, rfl⟩376      have hfit : Fits B N (⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩ : CState) :=377        ⟨Nat.two_pow_pos B, nimSum_lt hwP, nimSum_lt hwP, Nat.zero_le _, by simp, by simp⟩378      exact ih _ hidle hfit (fun Q hQ => hP Q (by simp [hQ])) st h1

263/-- Memory and update counts are those of the bit-level controller: 4 + 5B + 3r state264    bits (7 + 5B + 3·log₂N with r = log₂N + 1), 2N + 2 network updates per decision,265    one extra update per reset token. -/266theorem ctrl_counts (B N : Nat) (P : List Nat) :267    stateWidth B (N.log2 + 1) = 7 + 5 * B + 3 * N.log2 ∧ N < 2 ^ (N.log2 + 1) ∧268    (dtoks P).length = 2 * P.length + 2 :=269  ⟨(counter_width (B := B) N).2, (counter_width (B := B) N).1, dtoks_length P⟩

313/-- Update accounting: each decision uses exactly 2N + 2 controller updates; a game adds314    one reset update; the state has 4 + 5B + 3r bits (7 + 5B + 3·log₂N for r = log₂N + 1). -/315theorem replay_counts (B N : Nat) (P : List Nat) (hP : P.length = N) :316    (dtoks P).length = 2 * N + 2 ∧ (Tok.reset :: dtoks P).length = 2 * N + 3 ∧317    stateWidth B (N.log2 + 1) = 7 + 5 * B + 3 * N.log2 := by318  refine ⟨by rw [dtoks_length, hP], by simp [dtoks_length, hP], (counter_width (B := B) N).2⟩

282/-- RECURRENT WHOLE-GAME THEOREM: with N < 2^r heaps of width B, from any idle controller283    state whose registers fit (the initial state, and every state reached after earlier284    decisions), the threshold controller driven by the replay protocol wins from every285    nonzero position against every legal opponent; the move applied is exactly the286    emitted one; all controller states over the whole interaction fit the registers. -/287theorem replay_wins {B r N : Nat} (hN : N < 2 ^ r) : ∀ (P : List Nat), P.length = N → Width B P →288    nimSum P ≠ 0 → ∀ s, Idle s → Fits B N s → ReplayWins B r s P := by289  intro P290  induction P using (measure List.sum).wf.induction with291  | h P ih =>292    intro hP hw h0 s hs hf293    obtain ⟨hdec, hfit⟩ := decide_spec hN hs hf hP hw294    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0295    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd296    refine ReplayWins.intro s P (P.set i v) hfit (by rw [hdec, hd]; rfl) hmv (by rw [hdec]) ?_297    intro P' hm'298    have hlt1 := move_sum_lt hmv299    have hlt2 := move_sum_lt hm'300    obtain ⟨hidle, hfit'⟩ := afterState_ok (N := N) hw301    exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])302      (width_move (width_move hw hmv) hm') (move_from_zero hm' hz) _ hidle hfit'

304/-- GAME START from an arbitrary bit state: one reset token produces the encoding of the305    initial state, from which the replay strategy wins. -/306theorem replay_game {B r N : Nat} (hN : N < 2 ^ r) (v : Nat → Bool) {P : List Nat} (hP : P.length = N)307    (hw : Width B P) (h0 : nimSum P ≠ 0) :308    (tstep B r v Tok.reset).1 = sbits B r cinit ∧ ReplayWins B r cinit P := by309  refine ⟨by rw [tstep_reset], ?_⟩310  exact replay_wins hN P hP hw h0 cinit cinit_idle311    ⟨Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.zero_le _, by simp [cinit], by simp [cinit]⟩