BoardStore

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 Bypass23/- Phase 6, Priority 3b: the board-storage (one-pass) alternative of Section4   sec:recurrent-bypass, at bit level.  Written by Claude (10 October 2026).5   Lean 4.26.0, core/Std only.67   REGISTERS (finite, B·N + B + r bits): the stored board (N heaps × B bits, the boardBits8   layout), the accumulator acc (B bits, LSB first) and the write pointer idx (r bits, LSB9   first, N < 2^r so that idx can hold N).10   TOKENS: row x | sep | reset (one-hot tag bits and B row bits, LSB first).11     row x : board[idx] := x (multiplexed write via an equality decoder), acc := acc ⊕ x,12             idx := idx + 1 (ripple increment);13     sep   : output the summary acc and the move computed by the CONSTANT-DEPTH selector14             varBin (phase 5) on the stored board with target acc; acc := 0, idx := 0;15     reset : board := 0, acc := 0, idx := 0.16   One decision is rows(P), SEP: N + 1 updates, one pass, no replay; the price is the17   B·N-bit board register.  Proved: bit-level refinement of every update on fitting18   states, the decision theorem (summary nim(P) and move decisionMove P), persistence and19   reset, a stateful winning theorem against every legal opponent, and family20   certificates for the update and output formulas (constant depth, polynomial size,21   fixed-scale networks). -/2223namespace NimAudit24namespace BoardStore2526open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit27  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame28  Family Barrier RolloutExec2930/-! ## Semantics -/3132structure BS where33  board : List Nat34  acc : Nat35  idx : Nat3637def bsInit (N : Nat) : BS := ⟨List.replicate N 0, 0, 0⟩3839/-- Output at a separator: summary and selected move. -/40structure BOut where41  sum : Nat42  move : Option (Nat × Nat)4344def bsStep (N : Nat) (s : BS) : Tok → BS × Option BOut45  | .reset => (bsInit N, none)46  | .row x => (⟨s.board.set s.idx x, s.acc ^^^ x, s.idx + 1⟩, none)47  | .sep => (⟨s.board, 0, 0⟩, some ⟨s.acc, attainT s.acc s.board⟩)4849def bsRun (N : Nat) : BS → List Tok → BS × List BOut50  | s, [] => (s, [])51  | s, t :: ts => ((bsRun N (bsStep N s t).1 ts).1, (bsStep N s t).2.toList ++ (bsRun N (bsStep N s t).1 ts).2)5253/-- The tokens of one decision: one pass over the rows, then a separator. -/54def btoks (P : List Nat) : List Tok := P.map Tok.row ++ [Tok.sep]5556theorem btoks_length (P : List Nat) : (btoks P).length = P.length + 1 := by simp [btoks]5758/-- Writing a list of rows into the board from position k. -/59def writes : List Nat → Nat → List Nat → List Nat60  | b, _, [] => b61  | b, k, x :: L => writes (b.set k x) (k + 1) L6263theorem bsRun_append (N : Nat) (s : BS) (ts us : List Tok) :64    bsRun N s (ts ++ us) = ((bsRun N (bsRun N s ts).1 us).1, (bsRun N s ts).2 ++ (bsRun N (bsRun N s ts).1 us).2) := by65  induction ts generalizing s with66  | nil => simp [bsRun]67  | cons t ts ih => simp only [List.cons_append, bsRun, ih, List.append_assoc]6869theorem bsRun_rows (N : Nat) : ∀ (L : List Nat) (b : List Nat) (a k : Nat),70    bsRun N ⟨b, a, k⟩ (L.map Tok.row) = (⟨writes b k L, a ^^^ nimSum L, k + L.length⟩, [])71  | [], b, a, k => by simp [bsRun, writes, nimSum]72  | x :: L, b, a, k => by73    simp only [List.map_cons, bsRun, bsStep, Option.toList, List.nil_append]74    rw [bsRun_rows N L]75    simp [writes, nimSum, Nat.xor_assoc]; omega7677theorem take_set_succ (b : List Nat) (k x : Nat) (hk : k < b.length) :78    (b.set k x).take (k + 1) = b.take k ++ [x] := by79  apply List.ext_getElem80  · simp; omega81  · intro n h1 h282    simp only [List.length_take, List.length_set] at h183    rw [List.getElem_take]84    by_cases hn : n < k85    · rw [List.getElem_append_left (by simp; omega), List.getElem_take, List.getElem_set_ne (by omega)]86    · have : n = k := by omega87      subst this88      rw [List.getElem_append_right (by simp; omega)]89      simp9091theorem writes_eq : ∀ (L b : List Nat) (k : Nat), k + L.length = b.length → writes b k L = b.take k ++ L92  | [], b, k, h => by simp [writes]; rw [List.take_of_length_le (by simp at h; omega)]93  | x :: L, b, k, h => by94    simp only [writes]95    rw [writes_eq L (b.set k x) (k + 1) (by simp at h ⊢; omega)]96    rw [take_set_succ b k x (by simp at h; omega)]97    simp9899/-- ONE DECISION: from any idle state whose board has N slots, rows(P), SEP stores P,100    reports nim(P) and the winning-move selector's move, and returns to idle. -/101theorem bs_decision {N : Nat} (b : List Nat) (hb : b.length = N) (P : List Nat) (hP : P.length = N) :102    bsRun N ⟨b, 0, 0⟩ (btoks P) = (⟨P, 0, 0⟩, [⟨nimSum P, decisionMove P⟩]) := by103  unfold btoks104  rw [bsRun_append, bsRun_rows N P b 0 0, writes_eq P b 0 (by omega)]105  simp [bsRun, bsStep, attainT_eq_replayMove, decisionMove]106107/-- RESET from any state. -/108theorem bs_reset (N : Nat) (s : BS) (ts : List Tok) : bsRun N s (Tok.reset :: ts) = bsRun N (bsInit N) ts := by109  simp [bsRun, bsStep, Option.toList]110111/-- The move output by one decision. -/112def bsMove (N : Nat) (s : BS) (P : List Nat) : Option (Nat × Nat) :=113  ((bsRun N s (btoks P)).2.head?).bind BOut.move114115/-- Stateful interaction (player to move at P, machine in state s). -/116inductive StoreWins (N : Nat) : BS → List Nat → Prop117  | intro (s : BS) (P R : List Nat) :118      applyM P (bsMove N s P) = some R → Move P R →119      (bsRun N s (btoks P)).1 = ⟨P, 0, 0⟩ →120      (∀ P', Move R P' → StoreWins N ⟨P, 0, 0⟩ P') → StoreWins N s P121122theorem storeWins_sound {N : Nat} {s : BS} {P : List Nat} (h : StoreWins N s P) : Win P := by123  induction h with124  | intro s P R _ hm _ _ ih => exact Win.intro P R hm (Lose.intro R ih)125126/-- WHOLE-GAME THEOREM (semantic board-storage controller): from any idle state with N127    slots and every nonzero board of length N, the one-pass controller wins against every128    legal opponent; the stored board persists between decisions. -/129theorem store_wins {N : Nat} : ∀ (P : List Nat), P.length = N → nimSum P ≠ 0 →130    ∀ b, b.length = N → StoreWins N ⟨b, 0, 0⟩ P := by131  intro P132  induction P using (measure List.sum).wf.induction with133  | h P ih =>134    intro hP h0 b hb135    have hdec := bs_decision b hb P hP136    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0137    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd138    refine StoreWins.intro _ P (P.set i v) ?_ hmv (by rw [hdec]) ?_139    · unfold bsMove; rw [hdec]; simp [hd, applyM]140    · intro P' hm'141      have hlt1 := move_sum_lt hmv142      have hlt2 := move_sum_lt hm'143      exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])144        (move_from_zero hm' hz) P hP145146/-! ## Bit level -/147148/-- State width B·N + B + r. -/149def sw (B N r : Nat) : Nat := B * N + B + r150151def accW (B N q : Nat) : Nat := B * N + q152def idxW (B N q : Nat) : Nat := B * N + B + q153154def bsBits (B N r : Nat) (s : BS) : Nat → Bool := fun w =>155  if w < B * N then boardBits B s.board w156  else if w < B * N + B then s.acc.testBit (w - B * N)157  else if w < sw B N r then s.idx.testBit (w - (B * N + B)) else false158159/-- Token bits: 0 row flag, 1 separator flag, 2 reset flag, 3 + q row bit q. -/160def tokB : Tok → Nat → Bool161  | .row x, j => if j = 0 then true else if 3 ≤ j then x.testBit (j - 3) else false162  | .sep, j => decide (j = 1)163  | .reset, j => decide (j = 2)164165def inB (B N r : Nat) (v : Nat → Bool) (t : Tok) : Nat → Bool := fun w =>166  if w < sw B N r then v w else tokB t (w - sw B N r)167168def rowC (B N r : Nat) : Circ := input (sw B N r)169def sepC (B N r : Nat) : Circ := input (sw B N r + 1)170def rstC' (B N r : Nat) : Circ := input (sw B N r + 2)171def xC (B N r q : Nat) : Circ := input (sw B N r + 3 + q)172173/-- Equality decoder for the LSB-first pointer. -/174def eqI (B N r i : Nat) : Circ := and ((List.range r).map (fun q => litEq (input (idxW B N q)) (i.testBit q)))175176/-- Ripple increment: bit q of idx + 1. -/177def incF (B N q : Nat) : Circ := xor2 (input (idxW B N q)) (and ((List.range q).map (fun t => input (idxW B N t))))178179def bBoard (B N r w : Nat) : Circ :=180  RolloutExec.mux (rstC' B N r) (const false)181    (RolloutExec.mux (and [rowC B N r, eqI B N r (w / B)]) (xC B N r (B - 1 - w % B)) (input w))182183def bAcc (B N r q : Nat) : Circ :=184  RolloutExec.mux (rstC' B N r) (const false)185    (RolloutExec.mux (rowC B N r) (xor2 (input (accW B N q)) (xC B N r q)) (RolloutExec.mux (sepC B N r) (const false) (input (accW B N q))))186187def bIdx (B N r q : Nat) : Circ :=188  RolloutExec.mux (rstC' B N r) (const false)189    (RolloutExec.mux (rowC B N r) (incF B N q) (RolloutExec.mux (sepC B N r) (const false) (input (idxW B N q))))190191/-- The update formulas: board, accumulator, pointer. -/192def bsForms (B N r : Nat) : List Circ :=193  (List.range (B * N)).map (bBoard B N r) ++ (List.range B).map (bAcc B N r) ++ (List.range r).map (bIdx B N r)194195theorem bsForms_length (B N r : Nat) : (bsForms B N r).length = sw B N r := by196  simp [bsForms, sw]; omega197198/-- The output formulas: separator flag, summary bits, then the selector (valid, index,199    value) on the stored board and the accumulator. -/200def bsOuts (B N r r' : Nat) : List Circ :=201  [sepC B N r] ++ (List.range B).map (fun q => input (accW B N q)) ++ bForms (varBin B N r')202203def bsBitStep (B N r : Nat) (v : Nat → Bool) (t : Tok) : Nat → Bool := fun w =>204  if w < sw B N r then eval (inB B N r v t) ((bsForms B N r).getD w (const false)) else false205206/-! ### Evaluation lemmas -/207208theorem bsForms_board {B N r w : Nat} (hw : w < B * N) : (bsForms B N r).getD w (const false) = bBoard B N r w := by209  unfold bsForms210  rw [List.getD_eq_getElem?_getD, List.append_assoc, List.getElem?_append_left (by simpa using hw), List.getElem?_map,211    List.getElem?_range hw]212  rfl213214theorem bsForms_acc {B N r q : Nat} (hq : q < B) :215    (bsForms B N r).getD (B * N + q) (const false) = bAcc B N r q := by216  unfold bsForms217  rw [List.getD_eq_getElem?_getD, List.append_assoc, List.getElem?_append_right (by simp),218    List.getElem?_append_left (by simp; omega)]219  rw [show B * N + q - (List.map (bBoard B N r) (List.range (B * N))).length = q by simp]220  simp [hq]221222theorem bsForms_idx {B N r q : Nat} (hq : q < r) :223    (bsForms B N r).getD (B * N + B + q) (const false) = bIdx B N r q := by224  unfold bsForms225  rw [List.getD_eq_getElem?_getD, List.append_assoc, List.getElem?_append_right (by simp; omega),226    List.getElem?_append_right (by simp; omega)]227  rw [show B * N + B + q - (List.map (bBoard B N r) (List.range (B * N))).length -228    (List.map (bAcc B N r) (List.range B)).length = q by simp; omega]229  simp [hq]230231theorem eqI_eval (B N r i : Nat) (z : Nat → Bool) :232    eval z (eqI B N r i) = decide (∀ q < r, z (idxW B N q) = i.testBit q) := by233  apply Bool.eq_iff_iff.mpr234  simp only [eqI, eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp_apply, decide_eq_true_iff]235  constructor236  · intro h q hq237    have := h q hq238    unfold litEq at this239    cases hb : i.testBit q <;> simp [hb] at this <;> simp [this]240  · intro h q hq241    unfold litEq242    rw [← h q hq]243    cases hz : z (idxW B N q) <;> simp [hz]244245theorem eq_of_low_bits {a b r : Nat} (ha : a < 2 ^ r) (hb : b < 2 ^ r)246    (h : ∀ q < r, a.testBit q = b.testBit q) : a = b := by247  apply Nat.eq_of_testBit_eq248  intro q249  rcases Nat.lt_or_ge q r with hq | hq250  · exact h q hq251  · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le ha (Nat.pow_le_pow_right (by decide) hq)),252      Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hb (Nat.pow_le_pow_right (by decide) hq))]253254/-- Register fit invariant (N < 2^r so the pointer can count to N). -/255structure FitsB (B N r : Nat) (s : BS) : Prop where256  len : s.board.length = N257  width : Width B s.board258  acc : s.acc < 2 ^ B259  idx : s.idx ≤ N260  cnt : N < 2 ^ r261262theorem boardBits_set' {B N : Nat} {P : List Nat} (hl : P.length = N) {i w : Nat} (v : Nat) (hw : w < B * N) :263    boardBits B (P.set i v) w = if w / B = i then v.testBit (B - 1 - w % B) else boardBits B P w := by264  by_cases hi : i < N265  · exact boardBits_set hl v hi hw266  · have hwi : w / B < N := by267      rcases Nat.eq_zero_or_pos B with hB | hB268      · subst hB; simp at hw269      · exact (Nat.div_lt_iff_lt_mul hB).2 (by rw [Nat.mul_comm]; exact hw)270    rw [List.set_eq_of_length_le (by omega), if_neg (by omega)]271272/-- ONE-STEP REFINEMENT: on fitting states (and a row value of width B; for a row the273    pointer is below N), the update formulas compute the encoding of the semantic step. -/274theorem boardBits_zero (B N w : Nat) : boardBits B (List.replicate N 0) w = false := by275  unfold boardBits276  split277  · rw [List.getD_eq_getElem?_getD, List.getElem?_replicate]; split <;> simp278  · rfl279280theorem bsBitStep_spec {B N r : Nat} (s : BS) (hf : FitsB B N r s) (t : Tok)281    (ht : ∀ x, t = Tok.row x → x < 2 ^ B ∧ s.idx < N) :282    bsBitStep B N r (bsBits B N r s) t = bsBits B N r (bsStep N s t).1 := by283  have hidx_lt : s.idx < 2 ^ r := Nat.lt_of_le_of_lt hf.idx hf.cnt284  let z := inB B N r (bsBits B N r s) t285  have zb : ∀ w, w < B * N → z w = boardBits B s.board w := by286    intro w hw; simp only [z, inB, bsBits, sw]; rw [if_pos (by omega), if_pos hw]287  have za : ∀ q, q < B → z (accW B N q) = s.acc.testBit q := by288    intro q hq; simp only [z, inB, bsBits, accW, sw]; rw [if_pos (by omega), if_neg (by omega), if_pos (by omega)]289    congr 1; omega290  have zi : ∀ q, q < r → z (idxW B N q) = s.idx.testBit q := by291    intro q hq; simp only [z, inB, bsBits, idxW, sw]292    rw [if_pos (by omega), if_neg (by omega), if_neg (by omega), if_pos (by omega)]293    congr 1; omega294  have zrow : z (sw B N r) = tokB t 0 := by simp only [z, inB]; rw [if_neg (by omega)]; simp295  have zsep : z (sw B N r + 1) = tokB t 1 := by simp only [z, inB]; rw [if_neg (by omega)]; congr 1; omega296  have zrst : z (sw B N r + 2) = tokB t 2 := by simp only [z, inB]; rw [if_neg (by omega)]; congr 1; omega297  have zx : ∀ q, z (sw B N r + 3 + q) = tokB t (3 + q) := by298    intro q; simp only [z, inB]; rw [if_neg (by omega)]; congr 1; omega299  have tok_row : ∀ x q, tokB (Tok.row x) (3 + q) = x.testBit q := by300    intro x q; simp only [tokB]; rw [if_neg (by omega), if_pos (by omega)]; congr 1; omega301  funext w302  unfold bsBitStep bsBits303  by_cases hw1 : w < B * N304  · rw [if_pos (by unfold sw; omega), bsForms_board hw1, if_pos hw1]305    show eval z (bBoard B N r w) = _306    simp only [bBoard, eval_mux, rstC', rowC, xC, eval_input, eval_const, eval_and, List.all_cons, List.all_nil,307      Bool.and_true, zrow, zrst, zx, zb w hw1]308    cases t with309    | reset => simp [tokB, bsStep, bsInit, boardBits_zero]310    | sep => simp [tokB, bsStep]311    | row x =>312      obtain ⟨hx, hlt⟩ := ht x rfl313      have hwi : w / B < N := by314        rcases Nat.eq_zero_or_pos B with hB | hB315        · subst hB; simp at hw1316        · exact (Nat.div_lt_iff_lt_mul hB).2 (by rw [Nat.mul_comm]; exact hw1)317      have h2 : tokB (Tok.row x) 2 = false := by simp [tokB]318      have h0 : tokB (Tok.row x) 0 = true := by simp [tokB]319      simp only [h2, h0, tok_row, Bool.false_eq_true, if_false, Bool.true_and, bsStep]320      rw [eqI_eval, boardBits_set' hf.len x hw1]321      have hdec : decide (∀ q < r, z (idxW B N q) = (w / B).testBit q) = decide (w / B = s.idx) := by322        apply Bool.eq_iff_iff.mpr323        simp only [decide_eq_true_iff]324        constructor325        · intro h326          exact (eq_of_low_bits hidx_lt (Nat.lt_of_lt_of_le hwi (Nat.le_of_lt hf.cnt))327            (fun q hq => by rw [← zi q hq, h q hq])).symm328        · intro h q hq; rw [zi q hq, h]329      rw [hdec]330      by_cases hc : w / B = s.idx331      · simp [hc]332      · simp [hc]333  · rw [if_neg hw1]334    by_cases hw2 : w < B * N + B335    · have hq : w - B * N < B := by omega336      have hw' : w = B * N + (w - B * N) := by omega337      rw [if_pos (by unfold sw; omega), if_pos hw2, hw', bsForms_acc hq]338      show eval z (bAcc B N r (w - B * N)) = _339      simp only [bAcc, eval_mux, rstC', rowC, sepC, xC, eval_input, eval_const, eval_xor2, zrow, zsep, zrst, zx,340        za _ hq]341      rw [show B * N + (w - B * N) - B * N = w - B * N by omega]342      cases t with343      | reset => simp [tokB, bsStep, bsInit]344      | sep => simp [tokB, bsStep]345      | row x => simp [tokB, bsStep, Nat.testBit_xor, tok_row]346    · rw [if_neg hw2]347      by_cases hw3 : w < sw B N r348      · have hq : w - (B * N + B) < r := by unfold sw at hw3; omega349        have hw' : w = B * N + B + (w - (B * N + B)) := by omega350        rw [if_pos hw3, if_pos hw3, hw', bsForms_idx hq]351        show eval z (bIdx B N r (w - (B * N + B))) = _352        simp only [bIdx, eval_mux, rstC', rowC, sepC, eval_input, eval_const, zrow, zsep, zrst, zi _ hq]353        rw [show B * N + B + (w - (B * N + B)) - (B * N + B) = w - (B * N + B) by omega]354        have hinc : eval z (incF B N (w - (B * N + B))) = (s.idx + 1).testBit (w - (B * N + B)) := by355          simp only [incF, eval_xor2, eval_input, zi _ hq, eval_and, List.all_map, Function.comp_def]356          rw [ControllerBits.testBit_succ]357          congr 1358          apply Bool.eq_iff_iff.mpr359          simp only [List.all_eq_true, List.mem_range, decide_eq_true_iff]360          constructor361          · intro h u hu; rw [← zi u (by omega)]; exact h u hu362          · intro h u hu; rw [zi u (by omega)]; exact h u hu363        rw [hinc]364        cases t with365        | reset => simp [tokB, bsStep, bsInit]366        | sep => simp [tokB, bsStep]367        | row x => simp [tokB, bsStep]368      · rw [if_neg hw3, if_neg hw3]369370/-- Output decoding at a separator: flag, summary, selected move. -/371def bsDecode (B N r r' : Nat) (z : Nat → Bool) : Option BOut :=372  if z (sw B N r + 1) then373    some ⟨ofBits B (fun q => z (accW B N q)), binSem (varBin B N r') N z⟩374  else none375376/-- OUTPUT REFINEMENT: at a separator from a fitting state, the decoded outputs are the377    summary acc and the move attainT acc board (the phase-5 selector's semantics). -/378theorem bsDecode_sep {B N r r' : Nat} (hr' : N ≤ 2 ^ r') (s : BS) (hf : FitsB B N r s) :379    bsDecode B N r r' (inB B N r (bsBits B N r s) Tok.sep) = (bsStep N s Tok.sep).2 := by380  have hsel : ∀ c ∈ bForms (varBin B N r'), eval (inB B N r (bsBits B N r s) Tok.sep) c =381      eval (selIn B N s.board s.acc) c := by382    intro c hc383    have hb := (varSel_bound (B := B) (N := N))384    have hm : maxInput c ≤ B * N + B := by385      have := encode_bound_sel hb hr'386      exact (this.all c hc).2.2387    apply eval_congr_below388    intro i hi389    simp only [inB, bsBits, selIn, sw]390    rw [if_pos (by omega)]391    by_cases h1 : i < B * N392    · rw [if_pos h1, if_pos h1]393    · rw [if_neg h1, if_neg h1, if_pos (by omega)]394  unfold bsDecode bsStep395  have hflag : inB B N r (bsBits B N r s) Tok.sep (sw B N r + 1) = true := by396    simp only [inB]; rw [if_neg (by omega)]; simp [tokB]397  rw [if_pos hflag]398  simp only [Option.some.injEq, BOut.mk.injEq]399  constructor400  · apply Nat.eq_of_testBit_eq401    intro q402    rw [testBit_ofBits]403    by_cases hq : q < B404    · simp only [hq, decide_true, Bool.true_and]405      simp only [inB, bsBits, accW, sw]406      rw [if_pos (by omega), if_neg (by omega), if_pos (by omega)]407      congr 1; omega408    · simp only [hq, decide_false, Bool.false_and]409      rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hf.acc (Nat.pow_le_pow_right (by decide) (by omega)))]410  · have hb := encode_bound_sel (varSel_bound (B := B) (N := N)) hr'411    have e : binSem (varBin B N r') N (inB B N r (bsBits B N r s) Tok.sep) =412        binSem (varBin B N r') N (selIn B N s.board s.acc) := by413      unfold binSem414      have hv : eval (inB B N r (bsBits B N r s) Tok.sep) (varBin B N r').valid =415          eval (selIn B N s.board s.acc) (varBin B N r').valid := hsel _ (by simp [bForms])416      have hi : (varBin B N r').idx.map (eval (inB B N r (bsBits B N r s) Tok.sep)) =417          (varBin B N r').idx.map (eval (selIn B N s.board s.acc)) :=418        List.map_congr_left (fun c hc => hsel c (by simp [bForms, hc]))419      have hva : (varBin B N r').val.map (eval (inB B N r (bsBits B N r s) Tok.sep)) =420          (varBin B N r').val.map (eval (selIn B N s.board s.acc)) :=421        List.map_congr_left (fun c hc => hsel c (by simp [bForms, hc]))422      rw [hv, hi, hva]423    rw [e]424    exact varBin_correct hr' hf.len hf.width hf.acc425426/-! ### Runs over one decision -/427428def bsBitRun (B N r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool)429  | v, [] => v430  | v, t :: ts => bsBitRun B N r (bsBitStep B N r v t) ts431432theorem bsBitRun_append (B N r : Nat) (v : Nat → Bool) (ts us : List Tok) :433    bsBitRun B N r v (ts ++ us) = bsBitRun B N r (bsBitRun B N r v ts) us := by434  induction ts generalizing v with435  | nil => rfl436  | cons t ts ih => exact ih _437438theorem bits_rows {B N r : Nat} : ∀ (L : List Nat) (b : List Nat) (a k : Nat),439    FitsB B N r ⟨b, a, k⟩ → Width B L → k + L.length ≤ N →440    bsBitRun B N r (bsBits B N r ⟨b, a, k⟩) (L.map Tok.row) = bsBits B N r ⟨writes b k L, a ^^^ nimSum L, k + L.length⟩ ∧441      FitsB B N r ⟨writes b k L, a ^^^ nimSum L, k + L.length⟩442  | [], b, a, k, hf, _, _ => by simpa [bsBitRun, writes, nimSum] using hf443  | x :: L, b, a, k, hf, hw, hk => by444    have hx : x < 2 ^ B := hw x (by simp)445    simp only [List.map_cons, bsBitRun]446    rw [bsBitStep_spec _ hf (Tok.row x) (fun y hy => by cases hy; exact ⟨hx, show k < N by simp at hk; omega⟩)]447    have hf' : FitsB B N r ⟨b.set k x, a ^^^ x, k + 1⟩ := by448      refine ⟨by simp [hf.len], fun y hy => ?_, Nat.xor_lt_two_pow hf.acc hx, show k + 1 ≤ N by simp at hk; omega, hf.cnt⟩449      rcases List.mem_or_eq_of_mem_set hy with h | h450      · exact hf.width y h451      · rw [h]; exact hx452    obtain ⟨h1, h2⟩ := bits_rows L (b.set k x) (a ^^^ x) (k + 1) hf' (fun y hy => hw y (by simp [hy]))453      (by simp at hk; omega)454    simp only [bsStep]455    have e1 : a ^^^ x ^^^ nimSum L = a ^^^ nimSum (x :: L) := by simp [nimSum, Nat.xor_assoc]456    have e2 : k + 1 + L.length = k + (x :: L).length := by simp; omega457    rw [e1, e2] at h1 h2458    exact ⟨h1, h2⟩459460/-- BIT-LEVEL DECISION THEOREM: from the encoding of any idle state with N slots, the461    N row updates and the separator update produce the encoding of the idle state storing462    P, and the outputs at the separator decode to (nim(P), decisionMove P). -/463theorem bits_decision {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') (b : List Nat) (hb : b.length = N)464    (hwb : Width B b) (P : List Nat) (hP : P.length = N) (hw : Width B P) :465    bsBitRun B N r (bsBits B N r ⟨b, 0, 0⟩) (btoks P) = bsBits B N r ⟨P, 0, 0⟩ ∧466    bsDecode B N r r' (inB B N r (bsBitRun B N r (bsBits B N r ⟨b, 0, 0⟩) (P.map Tok.row)) Tok.sep) =467      some ⟨nimSum P, decisionMove P⟩ := by468  have hf0 : FitsB B N r ⟨b, 0, 0⟩ := ⟨hb, hwb, Nat.two_pow_pos B, Nat.zero_le _, hN⟩469  obtain ⟨h1, h2⟩ := bits_rows P b 0 0 hf0 hw (by omega)470  rw [writes_eq P b 0 (by omega), Nat.zero_xor, Nat.zero_add] at h1 h2471  simp only [List.take_zero, List.nil_append] at h1 h2472  constructor473  · unfold btoks474    rw [bsBitRun_append, h1]475    simp only [bsBitRun]476    rw [bsBitStep_spec _ h2 Tok.sep (fun _ h => by cases h)]477    simp [bsStep]478  · rw [h1, bsDecode_sep hr' _ h2]479    simp [bsStep, attainT_eq_replayMove, decisionMove]480481/-- Bit-level reset from ANY register vector. -/482theorem bits_reset (B N r : Nat) (v : Nat → Bool) : bsBitStep B N r v Tok.reset = bsBits B N r (bsInit N) := by483  funext w484  unfold bsBitStep bsBits485  have zr : ∀ j, inB B N r v Tok.reset (sw B N r + j) = decide (j = 2) := by486    intro j; simp only [inB]; rw [if_neg (by omega)]; simp [tokB]487  by_cases hw1 : w < B * N488  · rw [if_pos (by unfold sw; omega), bsForms_board hw1, if_pos hw1]489    simp only [bBoard, eval_mux, rstC', eval_input, zr, eval_const]490    simp [bsInit, boardBits_zero]491  · rw [if_neg hw1]492    by_cases hw2 : w < B * N + B493    · have hw' : w = B * N + (w - B * N) := by omega494      rw [if_pos (by unfold sw; omega), if_pos hw2, hw', bsForms_acc (by omega)]495      simp [bAcc, eval_mux, rstC', zr, bsInit]496    · rw [if_neg hw2]497      by_cases hw3 : w < sw B N r498      · have hw' : w = B * N + B + (w - (B * N + B)) := by omega499        rw [if_pos hw3, if_pos hw3, hw', bsForms_idx (by unfold sw at hw3; omega)]500        simp [bIdx, eval_mux, rstC', zr, bsInit]501      · rw [if_neg hw3, if_neg hw3]502503/-- Memory and update counts: B·N + B + r state bits; N + 1 updates per decision. -/504theorem bs_counts (B N r : Nat) (P : List Nat) (hP : P.length = N) :505    sw B N r = B * N + B + r ∧ (btoks P).length = N + 1 ∧ (bsForms B N r).length = sw B N r :=506  ⟨rfl, by rw [btoks_length, hP], bsForms_length B N r⟩507508509/-! ## Bit-level whole game -/510511/-- The move decoded from the outputs at the separator of one decision. -/512def bitMove (B N r r' : Nat) (v : Nat → Bool) (P : List Nat) : Option (Nat × Nat) :=513  (bsDecode B N r r' (inB B N r (bsBitRun B N r v (P.map Tok.row)) Tok.sep)).bind BOut.move514515/-- Stateful interaction driven by the BIT-LEVEL machine (register vector v). -/516inductive BitStoreWins (B N r r' : Nat) : (Nat → Bool) → List Nat → Prop517  | intro (v : Nat → Bool) (P R : List Nat) :518      applyM P (bitMove B N r r' v P) = some R → Move P R →519      bsBitRun B N r v (btoks P) = bsBits B N r ⟨P, 0, 0⟩ →520      (∀ P', Move R P' → BitStoreWins B N r r' (bsBits B N r ⟨P, 0, 0⟩) P') → BitStoreWins B N r r' v P521522theorem bitStoreWins_sound {B N r r' : Nat} {v : Nat → Bool} {P : List Nat} (h : BitStoreWins B N r r' v P) :523    Win P := by524  induction h with525  | intro v P R _ hm _ _ ih => exact Win.intro P R hm (Lose.intro R ih)526527/-- BIT-LEVEL WHOLE-GAME THEOREM: with N < 2^r and N ≤ 2^r', from the encoding of any idle528    state storing a width-B board of N slots, the one-pass bit-level machine wins from every529    nonzero board of width B against every legal opponent. -/530theorem bits_store_wins {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') :531    ∀ (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →532    ∀ b, b.length = N → Width B b → BitStoreWins B N r r' (bsBits B N r ⟨b, 0, 0⟩) P := by533  intro P534  induction P using (measure List.sum).wf.induction with535  | h P ih =>536    intro hP hw h0 b hb hwb537    obtain ⟨h1, h2⟩ := bits_decision (r' := r') hN hr' b hb hwb P hP hw538    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0539    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd540    refine BitStoreWins.intro _ P (P.set i v) ?_ hmv h1 ?_541    · unfold bitMove; rw [h2]; simp [hd, applyM]542    · intro P' hm'543      have hlt1 := move_sum_lt hmv544      have hlt2 := move_sum_lt hm'545      exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])546        (width_move (width_move hw hmv) hm') (move_from_zero hm' hz) P hP hw547548/-- GAME START: one reset update from an ARBITRARY register vector gives the encoding of549    the empty store, from which the bit-level machine wins. -/550theorem bits_store_game {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') (v : Nat → Bool)551    {P : List Nat} (hP : P.length = N) (hw : Width B P) (h0 : nimSum P ≠ 0) :552    bsBitStep B N r v Tok.reset = bsBits B N r (bsInit N) ∧553    BitStoreWins B N r r' (bsBitStep B N r v Tok.reset) P := by554  refine ⟨bits_reset B N r v, ?_⟩555  rw [bits_reset]556  exact bits_store_wins hN hr' P hP hw h0 _ (by simp [bsInit]) (fun x hx => by557    rw [List.eq_of_mem_replicate hx]; exact Nat.two_pow_pos B)558559/-! ## Resources -/560561theorem eqI_res (B N r i : Nat) : depth (eqI B N r i) ≤ 2 ∧ size (eqI B N r i) ≤ 2 * r + 1 ∧562    maxInput (eqI B N r i) ≤ sw B N r := by563  have hl : ∀ q, q < r → depth (litEq (input (idxW B N q)) (i.testBit q)) ≤ 1 ∧564      size (litEq (input (idxW B N q)) (i.testBit q)) ≤ 2 ∧ maxInput (litEq (input (idxW B N q)) (i.testBit q)) ≤ sw B N r := by565    intro q hq; unfold litEq idxW sw; split <;> simp <;> omega566  refine ⟨depth_and_le (fun c hc => ?_), ?_, ControllerBits.maxInput_and_le (fun c hc => ?_)⟩567  · obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc; exact (hl q (List.mem_range.mp hq)).1568  · unfold eqI; rw [size_and]569    have := sum_le_len_mul (cs := (List.range r).map (fun q => litEq (input (idxW B N q)) (i.testBit q))) (S := 2)570      (fun c hc => by obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc; exact (hl q (List.mem_range.mp hq)).2.1)571    simp only [List.length_map, List.length_range] at this; omega572  · obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc; exact (hl q (List.mem_range.mp hq)).2.2573574theorem mux_res {c a b : Circ} {dc sc mc da sa ma db sb mb : Nat}575    (hc : depth c ≤ dc ∧ size c ≤ sc ∧ maxInput c ≤ mc) (ha : depth a ≤ da ∧ size a ≤ sa ∧ maxInput a ≤ ma)576    (hb : depth b ≤ db ∧ size b ≤ sb ∧ maxInput b ≤ mb) :577    depth (RolloutExec.mux c a b) ≤ max (dc + 1) (max da db) + 2 ∧ size (RolloutExec.mux c a b) ≤ 2 * sc + sa + sb + 4 ∧578    maxInput (RolloutExec.mux c a b) ≤ max mc (max ma mb) := by579  have h1 := depth_mux_le c a b580  have h2 := size_mux c a b581  have h3 := maxInput_mux c a b582  refine ⟨by omega, by omega, by omega⟩583584theorem xor2_res' {a b : Circ} {da sa ma db sb mb : Nat}585    (ha : depth a ≤ da ∧ size a ≤ sa ∧ maxInput a ≤ ma) (hb : depth b ≤ db ∧ size b ≤ sb ∧ maxInput b ≤ mb) :586    depth (xor2 a b) ≤ max da db + 3 ∧ size (xor2 a b) ≤ 2 * sa + 2 * sb + 5 ∧ maxInput (xor2 a b) ≤ max ma mb := by587  obtain ⟨h1, h2, h3⟩ := xor2_res a b588  refine ⟨by omega, by omega, by omega⟩589590theorem inp_res {i m : Nat} (h : i + 1 ≤ m) : depth (input i) ≤ 0 ∧ size (input i) ≤ 1 ∧ maxInput (input i) ≤ m := by591  simp; omega592593theorem cst_res (b : Bool) : depth (const b) ≤ 0 ∧ size (const b) ≤ 1 ∧ maxInput (const b) ≤ 0 := by simp594595/-- UPDATE-FORMULA RESOURCES: depth ≤ 8, size ≤ 4r + 30, inputs below sw + 3 + B. -/596theorem bsForms_res (B N r : Nat) :597    ∀ c ∈ bsForms B N r, depth c ≤ 8 ∧ size c ≤ 4 * r + 30 ∧ maxInput c ≤ sw B N r + 3 + B := by598  have hrow : depth (rowC B N r) ≤ 0 ∧ size (rowC B N r) ≤ 1 ∧ maxInput (rowC B N r) ≤ sw B N r + 3 + B :=599    inp_res (by omega)600  have hsep : depth (sepC B N r) ≤ 0 ∧ size (sepC B N r) ≤ 1 ∧ maxInput (sepC B N r) ≤ sw B N r + 3 + B :=601    inp_res (by omega)602  have hrst : depth (rstC' B N r) ≤ 0 ∧ size (rstC' B N r) ≤ 1 ∧ maxInput (rstC' B N r) ≤ sw B N r + 3 + B :=603    inp_res (by omega)604  have hx : ∀ q, q < B → depth (xC B N r q) ≤ 0 ∧ size (xC B N r q) ≤ 1 ∧ maxInput (xC B N r q) ≤ sw B N r + 3 + B :=605    fun q hq => inp_res (by omega)606  intro c hc607  simp only [bsForms, List.mem_append, List.mem_map, List.mem_range] at hc608  rcases hc with (⟨w, hw, rfl⟩ | ⟨q, hq, rfl⟩) | ⟨q, hq, rfl⟩609  · obtain ⟨e1, e2, e3⟩ := eqI_res B N r (w / B)610    have hc1 : depth (and [rowC B N r, eqI B N r (w / B)]) ≤ 3 ∧ size (and [rowC B N r, eqI B N r (w / B)]) ≤ 2 * r + 3 ∧611        maxInput (and [rowC B N r, eqI B N r (w / B)]) ≤ sw B N r + 3 + B := by612      simp only [rowC, depth_and, size_and, maxInput_and, depth_input, size_input, maxInput_input, List.map_cons,613        List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr]614      refine ⟨by omega, by omega, by omega⟩615    have hB : B - 1 - w % B < B := by616      rcases Nat.eq_zero_or_pos B with hB | hB617      · subst hB; simp at hw618      · omega619    have hin := mux_res hc1 (hx _ hB) (inp_res (i := w) (m := sw B N r + 3 + B) (by unfold sw; omega))620    have hout := mux_res hrst (cst_res false) hin621    unfold bBoard622    refine ⟨by omega, by omega, by omega⟩623  · have hxo := xor2_res' (inp_res (i := accW B N q) (m := sw B N r + 3 + B) (by unfold accW sw; omega)) (hx q hq)624    have hm := mux_res hsep (cst_res false) (inp_res (i := accW B N q) (m := sw B N r + 3 + B) (by unfold accW sw; omega))625    have hn := mux_res hrow hxo hm626    have hout := mux_res hrst (cst_res false) hn627    unfold bAcc628    refine ⟨by omega, by omega, by omega⟩629  · have ha : depth (and ((List.range q).map (fun t => input (idxW B N t)))) ≤ 1 ∧630        size (and ((List.range q).map (fun t => input (idxW B N t)))) ≤ r + 1 ∧631        maxInput (and ((List.range q).map (fun t => input (idxW B N t)))) ≤ sw B N r + 3 + B := by632      refine ⟨depth_and_le (fun c hc => by obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp), ?_,633        ControllerBits.maxInput_and_le (fun c hc => ?_)⟩634      · rw [size_and]635        have := sum_le_len_mul (cs := (List.range q).map (fun t => input (idxW B N t))) (S := 1)636          (fun c hc => by obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp)637        simp only [List.length_map, List.length_range] at this; omega638      · obtain ⟨t, ht, rfl⟩ := List.mem_map.mp hc639        have := List.mem_range.mp ht; simp [idxW, sw]; omega640    have hinc := xor2_res' (inp_res (i := idxW B N q) (m := sw B N r + 3 + B) (by unfold idxW sw; omega)) ha641    have hm := mux_res hsep (cst_res false) (inp_res (i := idxW B N q) (m := sw B N r + 3 + B) (by unfold idxW sw; omega))642    have hn := mux_res hrow hinc hm643    have hout := mux_res hrst (cst_res false) hn644    unfold bIdx incF645    refine ⟨by omega, by omega, by omega⟩646647def varSz (B N : Nat) : Nat :=648  4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 + 2)) ^ 3649650/-- OUTPUT-FORMULA RESOURCES: depth ≤ 16; the selector part has the phase-5 bound. -/651theorem bsOuts_res {B N r r' : Nat} (hr' : N ≤ 2 ^ r') :652    ∀ c ∈ bsOuts B N r r', depth c ≤ 16 ∧ size c ≤ varSz B N + 1 ∧ maxInput c ≤ sw B N r + 3 + B := by653  have hb : BinBound (varBin B N r') N B r' (4 + 9 + 3) (varSz B N) (B * N + B) :=654    encode_bound_sel (varSel_bound (B := B) (N := N)) hr'655  intro c hc656  simp only [bsOuts, List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map, List.mem_range] at hc657  rcases hc with (rfl | ⟨q, hq, rfl⟩) | hc658  · simp [sepC, sw]; omega659  · simp [accW, sw]; omega660  · obtain ⟨a, b, d⟩ := hb.all c hc661    refine ⟨by omega, by omega, by unfold sw; omega⟩662663/-- Members (B, N), B, N ≥ 1, r = r' = log₂N + 1; input = registers + token. -/664def bsLen : Nat × Nat → Nat := fun i => sw i.1 i.2 (rIdx i.2) + 3 + i.1665def bsAll (i : Nat × Nat) : List Circ := bsForms i.1 i.2 (rIdx i.2) ++ bsOuts i.1 i.2 (rIdx i.2) (rIdx i.2)666667theorem bsLen_pos (i : Nat × Nat) (_hi : restAdm i) : 1 ≤ bsLen i := by unfold bsLen; omega668theorem bs_leaves (k : Nat) (i : Nat × Nat) (hi : restAdm i) : leafBN k i ≤ bsLen i := by669  have hB := Nat.mul_le_mul_left i.1 hi.2670  have hN := Nat.mul_le_mul_right i.2 hi.1671  match k with672  | 0 => show i.1 ≤ bsLen i; unfold bsLen sw; omega673  | 1 => show i.2 ≤ bsLen i; unfold bsLen sw; simp at hN; omega674  | _ + 2 => show rIdx i.2 ≤ bsLen i; unfold bsLen sw; omega675676def varSzE {ι : Type} : PE ι := 4 * ((vN + 2) * (12 * ((vN + 2) * (vB + 2) * (vB * (2 * vB + 3) + 9 + 2)) ^ 8 + 2)) ^ 3677678def bsSizeE {ι : Type} : PE ι := (vB * vN + vB + vr) * (4 * vr + 30) + (1 + vB + (1 + vr + vB)) * (varSzE + 1)679680theorem bsSizeE_eval (i : Nat × Nat) : PE.eval leafBN bsSizeE i =681    sw i.1 i.2 (rIdx i.2) * (4 * rIdx i.2 + 30) + (1 + i.1 + (1 + rIdx i.2 + i.1)) * (varSz i.1 i.2 + 1) := rfl682683theorem bsAll_tsize (i : Nat × Nat) :684    tsize (bsAll i) ≤ sw i.1 i.2 (rIdx i.2) * (4 * rIdx i.2 + 30) + (1 + i.1 + (1 + rIdx i.2 + i.1)) * (varSz i.1 i.2 + 1) := by685  unfold bsAll tsize686  rw [List.map_append, List.sum_append_nat]687  have h1 := sum_le_len_mul (cs := bsForms i.1 i.2 (rIdx i.2)) (S := 4 * rIdx i.2 + 30) (fun c hc => (bsForms_res _ _ _ c hc).2.1)688  have h2 := sum_le_len_mul (cs := bsOuts i.1 i.2 (rIdx i.2) (rIdx i.2)) (S := varSz i.1 i.2 + 1)689    (fun c hc => (bsOuts_res (rIdx_width i.2) c hc).2.1)690  have hl : (bsOuts i.1 i.2 (rIdx i.2) (rIdx i.2)).length = 1 + i.1 + (1 + rIdx i.2 + i.1) := by691    have hb := encode_bound_sel (varSel_bound (B := i.1) (N := i.2)) (rIdx_width i.2)692    have e1 : (varBin i.1 i.2 (rIdx i.2)).idx.length = rIdx i.2 := hb.idx_len693    have e2 : (varBin i.1 i.2 (rIdx i.2)).val.length = i.1 := hb.val_len694    unfold bsOuts bForms695    simp only [List.length_append, List.length_cons, List.length_map, List.length_range, List.length_nil, e1, e2]696    omega697  rw [bsForms_length] at h1; rw [hl] at h2698  omega699700/-- BOARD-STORAGE FAMILY CERTIFICATE: update and output formulas together have depth ≤ 16,701    read only the registers and one token, and have total size polynomial in that width. -/702theorem bs_ac0 : AC0Fam restAdm bsLen bsAll 16 := by703  refine ⟨bsLen_pos, fun i _ c hc => ?_, fun i _ c hc => ?_, ?_⟩704  · rcases List.mem_append.mp hc with h | h705    · have := (bsForms_res _ _ _ c h).1; omega706    · exact (bsOuts_res (rIdx_width i.2) c h).1707  · rcases List.mem_append.mp hc with h | h708    · exact (bsForms_res _ _ _ c h).2.2709    · exact (bsOuts_res (rIdx_width i.2) c h).2.2710  · exact polyIn_mono (fun i _ => bsAll_tsize i)711      (polyE bsLen_pos leafBN bs_leaves bsSizeE _ (fun i => (bsSizeE_eval i).symm))712713def bsNet (i : Nat × Nat) : List Layer := compileF (bsAll i)714715/-- The network computes exactly the formulas bsAll (outputs beyond them are 0). -/716theorem bsNet_eval (i : Nat × Nat) (x : Nat → Bool) {k : Nat} (hk : k < (bsAll i).length) :717    evalNet (bsNet i) x k = eval x (bsAll i)[k] := compileF_eval (bsAll i) x hk718719theorem bsNet_evalD (i : Nat × Nat) (x : Nat → Bool) {k : Nat} (hk : k < (bsAll i).length) :720    evalNet (bsNet i) x k = eval x ((bsAll i).getD k (const false)) := by721  rw [bsNet_eval i x hk, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hk, Option.getD_some]722723/-- NETWORK STEP = BIT STEP: the first sw network outputs on (state, token) are the next724    register vector, so bsBitStep_spec applies to the network. -/725theorem bsNet_step (B N : Nat) (v : Nat → Bool) (t : Tok) (w : Nat) :726    (if w < sw B N (rIdx N) then evalNet (bsNet (B, N)) (inB B N (rIdx N) v t) w else false) =727      bsBitStep B N (rIdx N) v t w := by728  unfold bsBitStep729  split730  · rename_i hw731    have hl : (bsForms B N (rIdx N)).length = sw B N (rIdx N) := bsForms_length B N (rIdx N)732    have hk : w < (bsAll (B, N)).length := by733      show w < (bsForms B N (rIdx N) ++ bsOuts B N (rIdx N) (rIdx N)).length734      rw [List.length_append]; omega735    rw [bsNet_evalD (B, N) _ hk]736    show eval _ ((bsForms B N (rIdx N) ++ bsOuts B N (rIdx N) (rIdx N)).getD w (const false)) = _737    rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append_left (by omega)]738  · rfl739740/-- NETWORK OUTPUTS: network output sw + k is output formula k of bsOuts (separator flag,741    accumulator bits, then the selector formulas read by bsDecode). -/742theorem bsNet_outputs (B N : Nat) (x : Nat → Bool) {k : Nat} (hk : k < (bsOuts B N (rIdx N) (rIdx N)).length) :743    evalNet (bsNet (B, N)) x (sw B N (rIdx N) + k) = eval x ((bsOuts B N (rIdx N) (rIdx N)).getD k (const false)) := by744  have hl : (bsForms B N (rIdx N)).length = sw B N (rIdx N) := bsForms_length B N (rIdx N)745  have hk' : sw B N (rIdx N) + k < (bsAll (B, N)).length := by746    show sw B N (rIdx N) + k < (bsForms B N (rIdx N) ++ bsOuts B N (rIdx N) (rIdx N)).length747    rw [List.length_append]; omega748  rw [bsNet_evalD (B, N) _ hk']749  show eval x ((bsForms B N (rIdx N) ++ bsOuts B N (rIdx N) (rIdx N)).getD (sw B N (rIdx N) + k) (const false)) = _750  rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append_right (by omega), hl,751    Nat.add_sub_cancel_left]752753/-- BOARD-STORAGE NETWORK CERTIFICATE (W = 1, ≤ 34 layers). -/754theorem bs_net : NetFam restAdm bsLen bsNet 1 34 := by755  have spec := fun i => compileF_spec (bsAll i) (bsLen i) 16756    (fun c hc => by757      rcases List.mem_append.mp hc with h | h758      · exact (bsForms_res _ _ _ c h).2.2759      · exact (bsOuts_res (rIdx_width i.2) c h).2.2)760    (fun c hc => by761      rcases List.mem_append.mp hc with h | h762      · have := (bsForms_res _ _ _ c h).1; omega763      · exact (bsOuts_res (rIdx_width i.2) c h).1)764  have hT := polyE bsLen_pos leafBN bs_leaves bsSizeE _ (fun i => (bsSizeE_eval i).symm)765  refine ⟨bsLen_pos, fun i _ => (spec i).2.2.1, fun i _ => (spec i).2.2.2.1, fun i _ => (spec i).2.2.2.2.1, ?_, ?_⟩766  · obtain ⟨c, k, h⟩ := polyIn_add bsLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (bsLen i)))767    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩768    have := bsAll_tsize i; have := h i hi; dsimp only at *; unfold tsize at *; omega769  · refine polyIn_mono (fun i _ => ?_) (polyIn_mul (polyIn_const _ _ 34) hT)770    have g := (spec i).2.2.2.2.2.2771    have h1 := bsAll_tsize i772    have h2 := length_le_tsize (bsAll i)773    unfold tsize at h1 h2774    show gateCount (compileF (bsAll i)) ≤ 34 * _775    omega776777/-! ## Axiom audit -/778779#print axioms btoks_length780#print axioms bsRun_append781#print axioms bsRun_rows782#print axioms take_set_succ783#print axioms writes_eq784#print axioms bs_decision785#print axioms bs_reset786#print axioms storeWins_sound787#print axioms store_wins788#print axioms bsForms_length789#print axioms bsForms_board790#print axioms bsForms_acc791#print axioms bsForms_idx792#print axioms eqI_eval793#print axioms eq_of_low_bits794#print axioms boardBits_set'795#print axioms boardBits_zero796#print axioms bsBitStep_spec797#print axioms bsDecode_sep798#print axioms bsBitRun_append799#print axioms bits_rows800#print axioms bits_decision801#print axioms bits_reset802#print axioms bs_counts803#print axioms bitStoreWins_sound804#print axioms bits_store_wins805#print axioms bits_store_game806#print axioms eqI_res807#print axioms mux_res808#print axioms xor2_res'809#print axioms inp_res810#print axioms cst_res811#print axioms bsForms_res812#print axioms bsOuts_res813#print axioms bsLen_pos814#print axioms bs_leaves815#print axioms bsSizeE_eval816#print axioms bsAll_tsize817#print axioms bs_ac0818#print axioms bsNet_eval819#print axioms bsNet_evalD820#print axioms bsNet_step821#print axioms bsNet_outputs822#print axioms bs_net823824