WholeGame

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 ThresholdInst23/- Phase 5, task 3: whole-game strategies driven by the actual implementations.4   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   A. TWO-FRAME RESTORATION.  The player stores its last established zero-nim-sum7      board Q.  After any legal opponent move Q → Q' it evaluates the compiled8      fixed-scale network for the LOCAL binary restoration circuit on the two frames9      (Q, Q'), decodes the output wires to (i, v), plays Q' → Q'.set i v and stores that10      board.  `TwoFrameWins` is a new, explicitly stateful game predicate (the strategy11      needs the predecessor, so the history-free NimGame.Wins does not apply directly);12      `twoFrame_sound` connects it to NimGame's Lose.  No claim is made about finding an13      initial move from an arbitrary winning position.14   B. MULTI-HEAD.  Rollouts are executed with the compiled π_j networks (one network15      evaluation per simulated game move); their terminal parities feed the compiled16      multi-head network; the resulting history-free selector wins against every legal17      opponent (NimGame.Wins) from every nonzero position.18   C. RECURRENT REPLAY.  The compiled threshold controller is driven by the explicit19      protocol rows SEP rows SEP (the ENVIRONMENT supplies the replay of the same board;20      it is an input-protocol assumption, not hidden memory), its emitted move is applied21      to the board, the internal state persists across decisions, and a reset token22      starts each game from an arbitrary bit state. -/2324namespace NimAudit25namespace WholeGame2627open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit28  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet2930theorem move_length {p q : List Nat} (h : Move p q) : q.length = p.length := by31  obtain ⟨pre, x, post, y, rfl, rfl, _⟩ := h; simp3233/-! ## A. Two-frame restoration with a stored predecessor -/3435/-- The player's reply: evaluate the compiled restoration network on (Q, Q'), decode its36    output wires and apply the decoded move to Q'.  Index width r = log₂N + 1. -/37def restReply (B : Nat) (Q Q' : List Nat) : Option (List Nat) :=38  applyM Q' (netBinSem (restNet B Q'.length (Q'.length.log2 + 1)) Q'.length (Q'.length.log2 + 1) B39    (LocalRestore.tf B Q'.length Q Q'))4041/-- Stateful two-frame game predicate (opponent to move at the stored board Q): every42    legal opponent move is answered by a legal reply, the reply's board becomes the new43    stored board, and play continues.  Being inductive, every such play is finite; at a44    terminal stored board the opponent cannot move and loses. -/45inductive TwoFrameWins (reply : List Nat → List Nat → Option (List Nat)) : List Nat → Prop46  | intro (Q : List Nat) :47      (∀ Q', Move Q Q' → (reply Q Q').isSome = true) →48      (∀ Q' R, Move Q Q' → reply Q Q' = some R → Move Q' R) →49      (∀ Q' R, Move Q Q' → reply Q Q' = some R → TwoFrameWins reply R) →50      TwoFrameWins reply Q5152/-- Soundness for the game semantics: the opponent, to move at the stored board, loses. -/53theorem twoFrame_sound {reply : List Nat → List Nat → Option (List Nat)} {Q : List Nat}54    (h : TwoFrameWins reply Q) : Lose Q := by55  induction h with56  | intro Q hsome hmove _ ih =>57    refine Lose.intro Q (fun Q' hm => ?_)58    cases hr : reply Q Q' with59    | none => have := hsome Q' hm; rw [hr] at this; cases this60    | some R => exact Win.intro Q' R (hmove Q' R hm hr) (ih Q' R hm hr)6162/-- ONE STEP: from a stored board with the zero invariant and any legal opponent move,63    the network reply is legal, equals NimGame.restore, and the new stored board keeps64    the length, the bit width and the zero invariant. -/65theorem restReply_step {B : Nat} {Q Q' : List Nat} (hw : Width B Q) (h0 : nimSum Q = 0) (hm : Move Q Q') :66    ∃ R, restReply B Q Q' = some R ∧ restore Q Q' = some R ∧ Move Q' R ∧ nimSum R = 0 ∧67      R.length = Q.length ∧ Width B R := by68  have hl := move_length hm69  have hw' := width_move hw hm70  obtain ⟨i, v, h1, h2, h3, h4⟩ := restNet_correct (B := B) (N := Q'.length) (r := Q'.length.log2 + 1)71    (width_log _) (by omega) rfl hw hw' h0 hm72  refine ⟨Q'.set i v, ?_, h2, h3, h4, by rw [move_length h3, hl], width_move hw' h3⟩73  unfold restReply; rw [h1]; rfl7475/-- TWO-FRAME WHOLE-GAME THEOREM: from an established zero-nim-sum stored board (opponent76    to move), the network-driven two-frame player answers every legal opponent move77    legally, keeps the zero invariant, the board length and the bit width, and every play78    terminates with the player making the last move.  Includes terminal and empty79    boards (no opponent move exists). -/80theorem twoFrame_wins {B : Nat} : ∀ (Q : List Nat), Width B Q → nimSum Q = 0 →81    TwoFrameWins (restReply B) Q := by82  intro Q83  induction Q using (measure List.sum).wf.induction with84  | h Q ih =>85    intro hw h086    refine TwoFrameWins.intro Q (fun Q' hm => ?_) (fun Q' R hm hR => ?_) (fun Q' R hm hR => ?_)87    · obtain ⟨R, h1, _⟩ := restReply_step hw h0 hm88      rw [h1]; rfl89    · obtain ⟨R', h1, _, h3, _⟩ := restReply_step hw h0 hm90      rw [h1] at hR; cases hR; exact h391    · obtain ⟨R', h1, _, h3, h4, _, h6⟩ := restReply_step hw h0 hm92      have hRR : R' = R := by rw [h1] at hR; exact Option.some.inj hR93      subst hRR94      refine ih R' ?_ h6 h495      have := move_sum_lt hm; have := move_sum_lt h396      show R'.sum < Q.sum; omega9798/-- Edge case: at a terminal (e.g. empty) stored board the opponent has no move. -/99theorem twoFrame_terminal {B : Nat} {Q : List Nat} (hw : Width B Q) (ht : Terminal Q) :100    TwoFrameWins (restReply B) Q ∧ ∀ Q', ¬ Move Q Q' :=101  ⟨twoFrame_wins Q hw (terminal_nimSum_zero ht), (terminal_iff_no_move Q).1 ht⟩102103theorem twoFrame_lose {B : Nat} {Q : List Nat} (hw : Width B Q) (h0 : nimSum Q = 0) : Lose Q :=104  twoFrame_sound (reply := restReply B) (twoFrame_wins Q hw h0)105106/-! ## B. Multi-head strategy with network-executed rollouts -/107108/-- Index width used for N heaps. -/109def rIdx (N : Nat) : Nat := N.log2 + 1110111/-- One π_j step executed by the compiled policy network. -/112def polStepN (B j : Nat) (P : List Nat) : Option (List Nat) :=113  applyM P (netBinSem (polNet B P.length j (rIdx P.length)) P.length (rIdx P.length) B (boardBits B P))114115theorem polStepN_eq {B j : Nat} {P : List Nat} (hw : Width B P) : polStepN B j P = policyStep j P :=116  polNet_correct (r := rIdx P.length) (width_log _) rfl hw117118theorem policyStep_move {j : Nat} {p q : List Nat} (h : policyStep j p = some q) : Move p q := by119  obtain ⟨pre, x, post, d, hp, hq, hd, hdx, _⟩ := policyMove_legal (policyStep_some h)120  exact ⟨pre, x, post, x - d, hp, hq, by omega⟩121122/-- A rollout executed by the policy network: one network evaluation per simulated game123    move; the result is the number of simulated moves. -/124def rollMoves (B j : Nat) : Nat → List Nat → Nat125  | 0, _ => 0126  | f + 1, P => match polStepN B j P with127    | none => 0128    | some Q => rollMoves B j f Q + 1129130theorem rolloutMoves_some {j : Nat} {p q : List Nat} (h : policyStep j p = some q) :131    rolloutMoves j p = rolloutMoves j q + 1 := by132  rw [rolloutMoves]; split <;> simp_all133134theorem rolloutMoves_none {j : Nat} {p : List Nat} (h : policyStep j p = none) : rolloutMoves j p = 0 := by135  rw [rolloutMoves]; split <;> simp_all136137/-- The network-executed rollout performs exactly the structured rollout. -/138theorem rollMoves_eq {B j : Nat} : ∀ (f : Nat) (P : List Nat), Width B P → P.sum ≤ f →139    rollMoves B j (f + 1) P = rolloutMoves j P140  | f, P, hw, hf => by141    simp only [rollMoves, polStepN_eq hw]142    cases h : policyStep j P with143    | none => rw [rolloutMoves_none h]144    | some Q =>145      simp only146      have hm := policyStep_move h147      have hlt := move_sum_lt hm148      rw [rolloutMoves_some h]149      cases f with150      | zero => omega151      | succ f => rw [rollMoves_eq f Q (width_move hw hm) (by omega)]152153/-- The rollout outcome observed by the player (first player wins iff odd). -/154def rollOut (B j : Nat) (P : List Nat) : Bool := (rollMoves B j (P.sum + 1) P).testBit 0155156theorem rollOut_eq {B j : Nat} {P : List Nat} (hw : Width B P) : rollOut B j P = rolloutWinner j P := by157  rw [rollOut, rollMoves_eq P.sum P hw (Nat.le_refl _), rolloutWinner_eq]158159/-- The multi-head player: run the B network rollouts, feed their outcomes and the board160    to the compiled multi-head network, decode its output wires and apply the move. -/161def mhSelect (B : Nat) (P : List Nat) : Option (List Nat) :=162  applyM P (netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B163    (obsIn B P.length P (fun j => rollOut B j P)))164165theorem mhSelect_eq {B : Nat} {P : List Nat} (hw : Width B P) : mhSelect B P = ctrlSel P := by166  have ho : (fun j => rollOut B j P) = outcomes P := by funext j; exact rollOut_eq hw167  unfold mhSelect ctrlSel168  rw [ho, mhNet_correct (r := rIdx P.length) (width_log _) rfl hw]169  cases decisionMove P <;> rfl170171theorem wins_congr {B : Nat} {sel sel' : List Nat → Option (List Nat)}172    (h : ∀ Q, Width B Q → sel Q = sel' Q) {P : List Nat} (hw : Width B P) (hP : Wins sel' P) :173    Wins sel P := by174  induction hP with175  | intro p q hsel hm _ ih =>176    refine Wins.intro p q (by rw [h p hw, hsel]) hm (fun r hr => ih r hr ?_)177    exact width_move (width_move hw hm) hr178179/-- MULTI-HEAD WHOLE-GAME THEOREM: from every nonzero position of bit width B, the player180    driven by network-executed rollouts and the compiled multi-head network wins against181    every legal opponent. -/182theorem mhSelect_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (mhSelect B) P :=183  wins_congr (fun Q hQ => mhSelect_eq hQ) hw (ctrl_wins P h)184185/-- Terminal behaviour: the player halts exactly on terminal boards, and every selected186    move is legal and keeps the bit width. -/187theorem mhSelect_terminal {B : Nat} {P : List Nat} (hw : Width B P) :188    (mhSelect B P = none ↔ Terminal P) ∧189    (∀ R, mhSelect B P = some R → Move P R ∧ Width B R) := by190  rw [mhSelect_eq hw]191  obtain ⟨h1, h2, _⟩ := decision_correct P192  refine ⟨?_, fun R hR => ?_⟩193  · unfold ctrlSel; rw [← h1]; cases decisionMove P <;> simp194  · unfold ctrlSel at hR195    cases hd : decisionMove P with196    | none => rw [hd] at hR; cases hR197    | some m =>198      obtain ⟨i, v⟩ := m199      rw [hd] at hR; simp only [Option.map_some, Option.some.injEq] at hR; subst hR200      obtain ⟨x, _, _, hmv⟩ := h2 i v hd201      exact ⟨hmv, width_move hw hmv⟩202203/-- ROLLOUT COST: the B network rollouts perform exactly totalRolloutMoves B P simulated204    game moves (one network evaluation each), at most B·Σ heaps ≤ B·N·(2^B − 1). -/205theorem mhSelect_cost {B : Nat} {P : List Nat} (hw : Width B P) :206    ((List.range B).map (fun j => rollMoves B j (P.sum + 1) P)).sum = totalRolloutMoves B P ∧207    totalRolloutMoves B P ≤ B * P.sum ∧ B * P.sum ≤ B * (P.length * (2 ^ B - 1)) := by208  have e : ((List.range B).map (fun j => rollMoves B j (P.sum + 1) P)) =209      (List.range B).map (fun j => rolloutMoves j P) :=210    List.map_congr_left (fun j _ => rollMoves_eq P.sum P hw (Nat.le_refl _))211  refine ⟨by rw [e]; rfl, ?_, ?_⟩212  · unfold totalRolloutMoves213    have := sum_map_le_mem (l := List.range B) (f := fun j => rolloutMoves j P) (g := fun _ => P.sum)214      (fun j _ => by215        show rolloutMoves j P ≤ P.sum216        rw [rolloutMoves_eq]; unfold rolloutCount217        have h := sum_map_le_mem (l := P) (f := heapCount j) (g := id) (fun h _ => heapCount_le j h)218        simpa using h)219    rw [List.map_const', List.sum_replicate_nat, List.length_range] at this220    exact this221  · apply Nat.mul_le_mul_left222    have h : ∀ x ∈ P, x ≤ 2 ^ B - 1 := fun x hx => by have := hw x hx; omega223    have := sum_map_le_mem (l := P) (f := id) (g := fun _ => 2 ^ B - 1) h224    simp [List.map_const', List.sum_replicate_nat] at this225    simpa [Nat.mul_comm] using this226227/-! ## C. Recurrent replay strategy with the threshold controller -/228229/-- The first move output in a list of controller outputs. -/230def moveOf : List COut → Option (Nat × Nat)231  | [] => none232  | COut.move m :: _ => m233  | COut.summary _ _ :: rest => moveOf rest234235/-- One decision: feed rows, SEP, the same rows again (replay supplied by the environment),236    SEP to the threshold controller; return the new state vector and the emitted move. -/237def decide (B r : Nat) (v : Nat → Bool) (P : List Nat) : (Nat → Bool) × Option (Nat × Nat) :=238  ((trun B r v (dtoks P)).1, moveOf (trun B r v (dtoks P)).2)239240/-- Machine state after a decision on board P. -/241def afterState (P : List Nat) : CState := ⟨false, 0, nimSum P, true, nimSum P, 0, none, none⟩242243theorem decide_spec {B r N : Nat} (hN : N < 2 ^ r) {s : CState} (hs : Idle s) (hf : Fits B N s)244    {P : List Nat} (hP : P.length = N) (hw : Width B P) :245    decide B r (sbits B r s) P = (sbits B r (afterState P), decisionMove P) ∧246    (∀ st ∈ crunStates s (dtoks P), FitsR B r st) := by247  have hstream : stream [P] = dtoks P := by simp [stream]248  have hfits := stream_fits s hs hf [P] (by simp [hP, hw])249  rw [hstream] at hfits250  have hall := allDec_of_fits (B := B) hN s (dtoks P) hfits (by251    rw [← hstream]; exact tok_bound_stream [P] (by simp [hw]))252  have hrun := trun_refines s (dtoks P) hall253  have hdec := crun_decision s hs P254  refine ⟨?_, fun st hst => ?_⟩255  · unfold decide; rw [hrun, hdec]; rfl256  · obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hfits st hst257    exact ⟨h1, h2, h3, by omega, fun i v hiv => ⟨by have := (h5 i v hiv).1; omega, (h5 i v hiv).2⟩,258      fun i v hiv => ⟨by have := (h6 i v hiv).1; omega, (h6 i v hiv).2⟩⟩259260theorem afterState_ok {B N : Nat} {P : List Nat} (hw : Width B P) :261    Idle (afterState P) ∧ Fits B N (afterState P) := by262  have h := nimSum_lt hw263  refine ⟨⟨rfl, rfl, rfl, rfl, rfl⟩, ?_⟩264  refine ⟨Nat.two_pow_pos B, h, h, Nat.zero_le _, ?_, ?_⟩ <;> simp [afterState]265266/-- Stateful interaction predicate (player to move at P; the controller holds the267    canonical encoding of the semantic state s).  At each decision: every intermediate268    controller state fits the registers, the emitted move is applied to the board and is269    legal, the controller's new vector encodes `afterState P` (the stored summary feeds270    the next decision), and after every legal opponent reply the interaction continues. -/271inductive ReplayWins (B r : Nat) : CState → List Nat → Prop272  | intro (s : CState) (P R : List Nat) :273      (∀ st ∈ crunStates s (dtoks P), FitsR B r st) →274      applyM P (decide B r (sbits B r s) P).2 = some R → Move P R →275      (decide B r (sbits B r s) P).1 = sbits B r (afterState P) →276      (∀ P', Move R P' → ReplayWins B r (afterState P) P') → ReplayWins B r s P277278theorem replayWins_sound {B r : Nat} {s : CState} {P : List Nat} (h : ReplayWins B r s P) : Win P := by279  induction h with280  | intro s P R _ _ hm _ _ ih => exact Win.intro P R hm (Lose.intro R ih)281282/-- 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'303304/-- 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]⟩312313/-- 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⟩319320321/-! ## Axiom audit -/322323#print axioms move_length324#print axioms twoFrame_sound325#print axioms restReply_step326#print axioms twoFrame_wins327#print axioms twoFrame_terminal328#print axioms twoFrame_lose329#print axioms polStepN_eq330#print axioms policyStep_move331#print axioms rolloutMoves_some332#print axioms rolloutMoves_none333#print axioms rollMoves_eq334#print axioms rollOut_eq335#print axioms mhSelect_eq336#print axioms wins_congr337#print axioms mhSelect_wins338#print axioms mhSelect_terminal339#print axioms mhSelect_cost340#print axioms decide_spec341#print axioms afterState_ok342#print axioms replayWins_sound343#print axioms replay_wins344#print axioms replay_game345#print axioms replay_counts346end WholeGame347end NimAudit