NimRecurrent

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 NimAttain2import Circuit34/- Phase 3, target B: the complete recurrent separator/state protocol.5   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.67   Stream: each position P is serialised as its rows (one token per heap, in8   order, empty heaps included) followed by SEP.  Persistent state: accumulator,9   previous completed summary, validity flag.10     row x : acc := acc XOR x11     SEP   : output (acc, if valid then some (prev XOR acc) else none);12             prev := acc; valid := true; acc := 0   (only the accumulator is reset)13   Proved:14     * fold invariant for arbitrary finite sequences of positions, including the15       first position, empty positions (= consecutive separators) and retained16       state between positions;17     * width preservation for B-bit rows; validity/reset behaviour;18     * stream differences equal Delta(P_{t-1}, P_t) and drive restoration;19     * move extraction by REPLAY (second scan; legal winning move when sigma ≠ 0,20       legal fallback / halt otherwise) with index and value bounds, and by BOARD21       STORAGE;22     * a bit-level encoding with 2B+1 state bits and an explicit per-update23       Boolean circuit (target C formulas) of constant depth and O(B) size, plus a24       fixed-scale threshold realisation of the XOR bit update.25   Not claimed: learning, self-play, or that training finds this update. -/2627namespace NimAudit28namespace Recurrent2930open Game Rollout Prob Attain AC0 AC0.Circ3132inductive Token where33  | row (x : Nat)34  | sep3536structure State where37  acc : Nat38  prev : Nat39  valid : Bool4041structure Out where42  summary : Nat43  diff : Option Nat4445def init : State := ⟨0, 0, false⟩4647/-- One recurrent update; SEP produces an output. -/48def step (s : State) : Token → State × Option Out49  | .row x => (⟨s.acc ^^^ x, s.prev, s.valid⟩, none)50  | .sep => (⟨0, s.acc, true⟩, some ⟨s.acc, if s.valid then some (s.prev ^^^ s.acc) else none⟩)5152/-- Run the recurrence over a token list, collecting outputs. -/53def run : State → List Token → State × List Out54  | s, [] => (s, [])55  | s, t :: ts => ((run (step s t).1 ts).1, (step s t).2.toList ++ (run (step s t).1 ts).2)5657/-- Serialise positions: rows then SEP, position after position. -/58def serialize (Ps : List (List Nat)) : List Token :=59  Ps.flatMap (fun P => P.map Token.row ++ [Token.sep])6061theorem run_append (s : State) (ts us : List Token) :62    run s (ts ++ us) = ((run (run s ts).1 us).1, (run s ts).2 ++ (run (run s ts).1 us).2) := by63  induction ts generalizing s with64  | nil => simp [run]65  | cons t ts ih => simp only [List.cons_append, run, ih, List.append_assoc]6667/-- Rows XOR into the accumulator; nothing else changes and nothing is output. -/68theorem run_rows (s : State) (P : List Nat) :69    run s (P.map Token.row) = (⟨s.acc ^^^ nimSum P, s.prev, s.valid⟩, []) := by70  induction P generalizing s with71  | nil => simp [run, nimSum]72  | cons x P ih =>73    simp only [List.map_cons, run, step, ih, Option.toList, List.nil_append, nimSum,74      Nat.xor_assoc]7576/-- One complete position. -/77theorem run_position (s : State) (P : List Nat) :78    run s (P.map Token.row ++ [Token.sep]) =79      (⟨0, s.acc ^^^ nimSum P, true⟩,80        [⟨s.acc ^^^ nimSum P, if s.valid then some (s.prev ^^^ (s.acc ^^^ nimSum P)) else none⟩]) := by81  rw [run_append, run_rows]82  simp [run, step]8384/-- Expected outputs for a sequence of positions from a state with empty accumulator. -/85def expectedOuts : Bool → Nat → List (List Nat) → List Out86  | _, _, [] => []87  | v, q, P :: Ps =>88    ⟨nimSum P, if v then some (q ^^^ nimSum P) else none⟩ :: expectedOuts true (nimSum P) Ps8990/-- Expected final state. -/91def expectedState : State → List (List Nat) → State92  | s, [] => s93  | _, P :: Ps => expectedState ⟨0, nimSum P, true⟩ Ps9495/-- FOLD INVARIANT.  From any state with empty accumulator, for ANY finite sequence96    of positions (empty positions allowed): the t-th output is97    (sigma(P_t), Delta) where Delta = prev XOR sigma(P_1) if the starting state is98    valid (none otherwise) for t = 1 and sigma(P_{t-1}) XOR sigma(P_t) for t ≥ 2;99    the final state retains the last summary with valid = true and acc = 0. -/100theorem fold_invariant (s : State) (hs : s.acc = 0) (Ps : List (List Nat)) :101    run s (serialize Ps) = (expectedState s Ps, expectedOuts s.valid s.prev Ps) := by102  induction Ps generalizing s with103  | nil => simp [serialize, run, expectedState, expectedOuts]104  | cons P Ps ih =>105    have e : serialize (P :: Ps) = (P.map Token.row ++ [Token.sep]) ++ serialize Ps := by106      simp [serialize]107    rw [e, run_append, run_position, hs, Nat.zero_xor]108    rw [ih ⟨0, nimSum P, true⟩ rfl]109    simp [expectedState, expectedOuts]110111/-- From the initial state: first output has no difference; later outputs carry112    the consecutive differences. -/113theorem stream_from_init (Ps : List (List Nat)) :114    (run init (serialize Ps)).2 = expectedOuts false 0 Ps := by115  rw [fold_invariant init rfl]; rfl116117/-- Empty positions are exactly consecutive separators. -/118theorem serialize_empty (Ps : List (List Nat)) :119    serialize ([] :: Ps) = Token.sep :: serialize Ps := by120  simp [serialize]121122/-- A separator immediately after a separator reports summary 0 (the empty123    position) and difference prev XOR 0 = prev. -/124theorem consecutive_sep (s : State) :125    run s [Token.sep, Token.sep] =126      (⟨0, 0, true⟩, [⟨s.acc, if s.valid then some (s.prev ^^^ s.acc) else none⟩,127        ⟨0, some (s.acc ^^^ 0)⟩]) := by128  simp [run, step]129130/-- RESET BEHAVIOUR: after SEP the accumulator is 0, the summary is retained and the131    validity bit is set; rows never change prev or valid. -/132theorem sep_resets (s : State) :133    (step s Token.sep).1 = ⟨0, s.acc, true⟩ := rfl134135theorem row_keeps (s : State) (x : Nat) :136    (step s (Token.row x)).1.prev = s.prev ∧ (step s (Token.row x)).1.valid = s.valid := ⟨rfl, rfl⟩137138/-- WIDTH PRESERVATION: B-bit rows keep acc and prev below 2^B. -/139def StateWidth (B : Nat) (s : State) : Prop := s.acc < 2 ^ B ∧ s.prev < 2 ^ B140141def TokenWidth (B : Nat) : Token → Prop142  | .row x => x < 2 ^ B143  | .sep => True144145theorem step_width {B : Nat} {s : State} {t : Token} (hs : StateWidth B s) (ht : TokenWidth B t) :146    StateWidth B (step s t).1 := by147  cases t with148  | row x => exact ⟨Nat.xor_lt_two_pow hs.1 ht, hs.2⟩149  | sep => exact ⟨Nat.two_pow_pos B, hs.1⟩150151theorem run_width {B : Nat} : ∀ {s : State} {ts : List Token}, StateWidth B s →152    (∀ t ∈ ts, TokenWidth B t) → StateWidth B (run s ts).1153  | s, [], hs, _ => hs154  | s, t :: ts, hs, ht => by155    simp only [run]156    exact run_width (step_width hs (ht t (by simp))) (fun u hu => ht u (List.mem_cons_of_mem _ hu))157158/-! ## Differences and restoration from the stream -/159160/-- Stream differences are nimber differences of consecutive positions. -/161theorem stream_diff_one_heap (pre post : List Nat) (a b : Nat) :162    nimSum (pre ++ a :: post) ^^^ nimSum (pre ++ b :: post) = a ^^^ b :=163  one_heap_difference pre post a b164165/-- RESTORATION FROM THE STREAM: if the previous position Q had nim-sum zero and the166    opponent moved legally to Q', the difference reported at Q's successor drives a167    legal move to nim-sum zero (cancel the reported difference at the first168    qualifying heap). -/169theorem stream_restoration {Q Q' : List Nat} (h0 : nimSum Q = 0) (hm : Move Q Q') :170    ∃ R, cancelFirst (nimSum Q ^^^ nimSum Q') Q' = some R ∧ Move Q' R ∧ nimSum R = 0 :=171  restore_correct h0 hm172173theorem stream_reports_delta (Q Q' : List Nat) (Ps : List (List Nat)) :174    expectedOuts false 0 (Q :: Q' :: Ps) =175      ⟨nimSum Q, none⟩ :: ⟨nimSum Q', some (nimSum Q ^^^ nimSum Q')⟩ ::176        expectedOuts true (nimSum Q') Ps := by177  simp [expectedOuts]178179/-! ## Move extraction by replay -/180181structure Replay where182  idx : Nat183  sel : Option (Nat × Nat)184  fnz : Option (Nat × Nat)185186/-- Replay update for row x, with the summary sigma held fixed. -/187def replayStep (σ : Nat) (r : Replay) (x : Nat) : Replay :=188  ⟨r.idx + 1,189   (match r.sel with190    | some m => some m191    | none => if σ ≠ 0 ∧ x ^^^ σ < x then some (r.idx, x ^^^ σ) else none),192   (match r.fnz with193    | some m => some m194    | none => if 0 < x then some (r.idx, x - 1) else none)⟩195196def replay (σ : Nat) (r : Replay) (P : List Nat) : Replay := P.foldl (replayStep σ) r197198def shift (i0 : Nat) : Option (Nat × Nat) → Option (Nat × Nat) :=199  Option.map (fun p => (i0 + p.1, p.2))200201/-- Left-biased choice. -/202def firstSome {α : Type} : Option α → Option α → Option α203  | some x, _ => some x204  | none, y => y205206/-- The cancelling selection for summary sigma (none when sigma = 0). -/207def selFor (σ : Nat) (P : List Nat) : Option (Nat × Nat) :=208  if σ = 0 then none else cancelIdx σ P209210theorem shift_zero (o : Option (Nat × Nat)) : shift 0 o = o := by211  cases o <;> simp [shift]212213theorem firstSome_none_right {α : Type} (o : Option α) : firstSome o none = o := by214  cases o <;> rfl215216theorem shift_map_succ (i0 : Nat) (o : Option (Nat × Nat)) :217    shift i0 (o.map (fun p => (p.1 + 1, p.2))) = shift (i0 + 1) o := by218  cases o with219  | none => rfl220  | some p => simp [shift]; omega221222/-- REPLAY CHARACTERISATION: replaying P from index i0 with partial selections s, f223    yields s (if already set) or the first cancelling heap, and f or the first224    nonzero heap, with indices offset by i0. -/225theorem replay_spec (σ : Nat) : ∀ (P : List Nat) (i0 : Nat) (s f : Option (Nat × Nat)),226    replay σ ⟨i0, s, f⟩ P =227      ⟨i0 + P.length, firstSome s (shift i0 (selFor σ P)), firstSome f (shift i0 (decIdx P))⟩228  | [], i0, s, f => by229    simp [replay, selFor, cancelIdx, decIdx, shift, firstSome_none_right]230  | x :: P, i0, s, f => by231    have ih := replay_spec σ P (i0 + 1)232    simp only [replay, List.foldl_cons] at ih ⊢233    rw [replayStep, ih]234    simp only [Replay.mk.injEq, List.length_cons]235    refine ⟨by omega, ?_, ?_⟩236    · cases s with237      | some m => rfl238      | none =>239        simp only [firstSome]240        by_cases hσ : σ = 0241        · simp [hσ, selFor, shift]242        · by_cases hx : x ^^^ σ < x243          · simp [hσ, hx, selFor, cancelIdx, shift]244          · simp only [hσ, hx, and_false, if_false, firstSome, selFor, cancelIdx, ne_eq,245              not_false_eq_true, true_and]246            rw [shift_map_succ]247    · cases f with248      | some m => rfl249      | none =>250        simp only [firstSome]251        by_cases hx : 0 < x252        · simp [hx, decIdx, shift]253        · simp only [hx, if_false, firstSome, decIdx]254          first | done | rw [shift_map_succ]255256/-- The move chosen after replay. -/257def replayMove (σ : Nat) (P : List Nat) : Option (Nat × Nat) :=258  let r := replay σ ⟨0, none, none⟩ P259  firstSome r.sel r.fnz260261theorem replayMove_eq (σ : Nat) (P : List Nat) :262    replayMove σ P = firstSome (selFor σ P) (decIdx P) := by263  unfold replayMove264  rw [replay_spec]265  simp [firstSome, shift_zero]266267theorem terminal_nimSum_zero {P : List Nat} (h : Terminal P) : nimSum P = 0 := by268  induction P with269  | nil => rfl270  | cons y ys ih =>271    simp only [nimSum, h y (by simp), Nat.zero_xor]272    exact ih (fun z hz => h z (List.mem_cons_of_mem _ hz))273274/-- 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 _315316/-- TWO-SCAN PROTOCOL: the first scan (N rows + SEP, from the initial state) reports317    sigma = nim(P); the replay scan (N more rows) then yields the move of318    `replay_correct`.  Total 2N + 1 updates. -/319theorem two_scan_protocol (P : List Nat) :320    (run init (P.map Token.row ++ [Token.sep])).2 = [⟨nimSum P, none⟩] ∧321    (P.map Token.row ++ [Token.sep]).length + P.length = 2 * P.length + 1 := by322  refine ⟨?_, by simp; omega⟩323  rw [run_position]324  simp [init]325326/-- Replay resources: the index counter ends at N, selected indices are < N, and on327    a B-bit board selected values are < 2^B; indices < N fit in log2 N + 1 bits. -/328theorem replay_resources {B : Nat} (P : List Nat) (hw : Width B P) :329    (replay (nimSum P) ⟨0, none, none⟩ P).idx = P.length ∧330    (∀ i v, replayMove (nimSum P) P = some (i, v) →331      i < P.length ∧ v < 2 ^ B ∧ i < 2 ^ (P.length.log2 + 1)) := by332  refine ⟨by rw [replay_spec]; simp, ?_⟩333  intro i v h334  obtain ⟨x, hx, hlt⟩ := (replay_correct P).2.1 i v h335  have hi : i < P.length := by336    rcases Nat.lt_or_ge i P.length with h' | h'337    · exact h'338    · rw [List.getElem?_eq_none h'] at hx; cases hx339  have hxm : x ∈ P := List.mem_of_getElem? hx340  exact ⟨hi, Nat.lt_trans hlt (hw x hxm), Nat.lt_trans hi Nat.lt_log2_self⟩341342/-! ## Move extraction by board storage -/343344structure Store where345  acc : Nat346  board : List Nat347348def storeStep (st : Store) (x : Nat) : Store := ⟨st.acc ^^^ x, st.board ++ [x]⟩349350theorem store_fold (P : List Nat) (a : Nat) (b : List Nat) :351    P.foldl storeStep ⟨a, b⟩ = ⟨a ^^^ nimSum P, b ++ P⟩ := by352  induction P generalizing a b with353  | nil => simp [nimSum]354  | cons x P ih =>355    simp only [List.foldl_cons, storeStep, ih, nimSum, Nat.xor_assoc, List.append_assoc,356      List.singleton_append]357358theorem store_fold0 (P : List Nat) : P.foldl storeStep ⟨0, []⟩ = ⟨nimSum P, P⟩ := by359  rw [store_fold]; simp360361/-- BOARD STORAGE: one scan stores (nim(P), P); the separator applies the phase-2362    selector, which is legal, winning when sigma ≠ 0 and halts only when terminal.363    Memory: N rows of B bits plus a B-bit accumulator. -/364theorem store_correct (P : List Nat) :365    (P.foldl storeStep ⟨0, []⟩).acc = nimSum P ∧ (P.foldl storeStep ⟨0, []⟩).board = P ∧366    (∀ q, selectMove (P.foldl storeStep ⟨0, []⟩).acc (P.foldl storeStep ⟨0, []⟩).board = some q →367      Move P q) ∧368    (selectMove (P.foldl storeStep ⟨0, []⟩).acc (P.foldl storeStep ⟨0, []⟩).board = none ↔369      Terminal P) ∧370    (nimSum P ≠ 0 → ∃ q, selectMove (P.foldl storeStep ⟨0, []⟩).acc371      (P.foldl storeStep ⟨0, []⟩).board = some q ∧ Move P q ∧ nimSum q = 0) := by372  rw [store_fold0]373  exact ⟨rfl, rfl, fun q h => selectMove_legal h, selectMove_none_iff _ P, selectMove_zero⟩374375/-! ## Bit-level state and the per-update circuit -/376377/-- Input layout of one update: acc bits 0..B-1, prev bits B..2B-1, valid 2B,378    tag 2B+1 (true = row), row bits 2B+2..3B+1. -/379def encode (B : Nat) (s : State) (t : Token) : Nat → Bool := fun j =>380  if j < B then s.acc.testBit j381  else if j < 2 * B then s.prev.testBit (j - B)382  else if j = 2 * B then s.valid383  else if j = 2 * B + 1 then (match t with | .row _ => true | .sep => false)384  else if j < 3 * B + 2 then (match t with | .row x => x.testBit (j - (2 * B + 2)) | .sep => false)385  else false386387def xorC (a b : Circ) : Circ := or [and [a, not b], and [not a, b]]388def accC (B k : Nat) : Circ := and [input (2 * B + 1), xorC (input k) (input (2 * B + 2 + k))]389def prevC (B k : Nat) : Circ :=390  or [and [input (2 * B + 1), input (B + k)], and [not (input (2 * B + 1)), input k]]391def validC (B : Nat) : Circ := or [input (2 * B), not (input (2 * B + 1))]392def diffC (B k : Nat) : Circ := xorC (input (B + k)) (input k)393def diffValidC (B : Nat) : Circ := and [input (2 * B), not (input (2 * B + 1))]394395theorem eval_xorC (x : Nat → Bool) (a b : Circ) : eval x (xorC a b) = xor (eval x a) (eval x b) := by396  unfold xorC397  simp only [eval_or, eval_and, eval_not, List.all_cons, List.all_nil, List.any_cons, List.any_nil]398  generalize eval x a = p399  generalize eval x b = q400  cases p <;> cases q <;> rfl401402theorem enc_acc {B k : Nat} (hk : k < B) (s : State) (t : Token) :403    encode B s t k = s.acc.testBit k := by simp [encode, hk]404405theorem enc_prev {B k : Nat} (hk : k < B) (s : State) (t : Token) :406    encode B s t (B + k) = s.prev.testBit k := by407  simp [encode, show ¬ B + k < B by omega, show B + k < 2 * B by omega]408409theorem enc_valid (B : Nat) (s : State) (t : Token) : encode B s t (2 * B) = s.valid := by410  simp [encode, show ¬ 2 * B < B by omega]411412theorem enc_tag (B : Nat) (s : State) (t : Token) :413    encode B s t (2 * B + 1) = (match t with | .row _ => true | .sep => false) := by414  simp [encode, show ¬ 2 * B + 1 < B by omega, show ¬ 2 * B + 1 < 2 * B by omega]415416theorem enc_x {B k : Nat} (hk : k < B) (s : State) (x : Nat) :417    encode B s (Token.row x) (2 * B + 2 + k) = x.testBit k := by418  simp [encode, show ¬ 2 * B + 2 + k < B by omega, show ¬ 2 * B + 2 + k < 2 * B by omega,419    show 2 * B + 2 + k ≠ 2 * B by omega, show 2 * B + 2 + k ≠ 2 * B + 1 by omega,420    show 2 * B + 2 + k < 3 * B + 2 by omega]421422/-- PER-UPDATE CIRCUIT CORRECTNESS (k < B): the circuits compute the new state bits423    and, at a separator, the output bits. -/424theorem circuit_update {B k : Nat} (hk : k < B) (s : State) (t : Token) :425    eval (encode B s t) (accC B k) = (step s t).1.acc.testBit k ∧426    eval (encode B s t) (prevC B k) = (step s t).1.prev.testBit k ∧427    eval (encode B s t) (validC B) = (step s t).1.valid ∧428    (t = Token.sep → eval (encode B s t) (input k) = s.acc.testBit k ∧429      eval (encode B s t) (diffC B k) = (s.prev ^^^ s.acc).testBit k ∧430      eval (encode B s t) (diffValidC B) = s.valid) := by431  cases t with432  | row x =>433    simp only [accC, prevC, validC, eval_and, eval_or, eval_not, eval_input, eval_xorC,434      List.all_cons, List.all_nil, List.any_cons, List.any_nil, enc_acc hk, enc_prev hk,435      enc_valid, enc_tag, enc_x hk, step, Nat.testBit_xor]436    refine ⟨by simp, by simp, by simp, fun h => by cases h⟩437  | sep =>438    simp only [accC, prevC, validC, diffC, diffValidC, eval_and, eval_or, eval_not, eval_input,439      eval_xorC, List.all_cons, List.all_nil, List.any_cons, List.any_nil, enc_acc hk,440      enc_prev hk, enc_valid, enc_tag, step, Nat.testBit_xor, Nat.zero_testBit]441    refine ⟨by simp, by simp, by simp, fun _ => ⟨by simp, by simp, by simp⟩⟩442443/-- The 2B+1 state bits determine the state (B-bit width). -/444def stateOfBits (B : Nat) (bits : Nat → Bool) : State :=445  ⟨ofBits B (fun k => bits k), ofBits B (fun k => bits (B + k)), bits (2 * B)⟩446447theorem ofBits_testBit_eq {B v : Nat} (hv : v < 2 ^ B) (f : Nat → Bool)448    (hf : ∀ k < B, f k = v.testBit k) : ofBits B f = v := by449  apply Nat.eq_of_testBit_eq450  intro i451  rw [testBit_ofBits]452  by_cases hi : i < B453  · simp [hi, hf i hi]454  · simp only [hi, decide_false, Bool.false_and]455    exact (Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hv456      (Nat.pow_le_pow_right (by decide) (by omega)))).symm457458/-- STATE-BIT THEOREM: 2B+1 bits suffice, and the per-update circuit maps the bit459    encoding of a B-bit state to the bit encoding of its successor. -/460theorem circuit_step_correct {B : Nat} {s : State} {t : Token} (hs : StateWidth B s)461    (ht : TokenWidth B t) :462    stateOfBits B (fun j =>463        if j < B then eval (encode B s t) (accC B j)464        else if j < 2 * B then eval (encode B s t) (prevC B (j - B))465        else eval (encode B s t) (validC B)) = (step s t).1 := by466  have hw := step_width hs ht467  unfold stateOfBits468  have h1 : ofBits B (fun k => if k < B then eval (encode B s t) (accC B k)469      else if k < 2 * B then eval (encode B s t) (prevC B (k - B))470      else eval (encode B s t) (validC B)) = (step s t).1.acc := by471    apply ofBits_testBit_eq hw.1472    intro k hk473    simp only [hk, if_true]474    exact (circuit_update hk s t).1475  have h2 : ofBits B (fun k => if B + k < B then eval (encode B s t) (accC B (B + k))476      else if B + k < 2 * B then eval (encode B s t) (prevC B (B + k - B))477      else eval (encode B s t) (validC B)) = (step s t).1.prev := by478    apply ofBits_testBit_eq hw.2479    intro k hk480    simp only [show ¬ B + k < B by omega, show B + k < 2 * B by omega, if_true, if_false,481      show B + k - B = k by omega]482    exact (circuit_update hk s t).2.1483  have h3 : (if 2 * B < B then eval (encode B s t) (accC B (2 * B))484      else if 2 * B < 2 * B then eval (encode B s t) (prevC B (2 * B - B))485      else eval (encode B s t) (validC B)) = (step s t).1.valid := by486    simp only [show ¬ 2 * B < B by omega, Nat.lt_irrefl, if_false]487    cases t <;> simp [validC, enc_valid, enc_tag, step]488  simp only []489  rw [h1, h2, h3]490491/-- Per-update circuit resources: depth ≤ 4, total size ≤ 28 B + 8 for all492    state and output bits (constant depth, O(B) size). -/493theorem circuit_resources (B k : Nat) :494    depth (accC B k) ≤ 4 ∧ depth (prevC B k) ≤ 4 ∧ depth (validC B) ≤ 4 ∧495    depth (diffC B k) ≤ 4 ∧ depth (diffValidC B) ≤ 4 ∧496    size (accC B k) + size (prevC B k) + size (diffC B k) ≤ 28 ∧497    size (validC B) + size (diffValidC B) ≤ 8 := by498  simp [accC, prevC, validC, diffC, diffValidC, xorC, listMax]499500/-- Fixed-scale threshold realisation of one XOR bit update (W = 2): a two-layer501    network of literal-threshold gates computes a XOR b. -/502def xorNet : List Layer :=503  [[⟨[1, 1], [false, true], 2⟩, ⟨[1, 1], [true, false], 2⟩], [⟨[1, 1], [false, false], 1⟩]]504505theorem xorNet_valid : NetValid 2 xorNet := by506  intro l hl g hg507  simp [xorNet] at hl508  rcases hl with rfl | rfl <;> simp at hg <;> rcases hg with rfl | rfl <;>509    simp [Gate.Valid] <;> omega510511theorem xorNet_correct (a b : Bool) :512    evalNet xorNet (fun j => if j = 0 then a else if j = 1 then b else false) 0 = xor a b := by513  cases a <;> cases b <;> decide514515#print axioms run_append516#print axioms run_rows517#print axioms run_position518#print axioms fold_invariant519#print axioms stream_from_init520#print axioms serialize_empty521#print axioms consecutive_sep522#print axioms sep_resets523#print axioms row_keeps524#print axioms step_width525#print axioms run_width526#print axioms stream_diff_one_heap527#print axioms stream_restoration528#print axioms stream_reports_delta529#print axioms shift_zero530#print axioms firstSome_none_right531#print axioms shift_map_succ532#print axioms replay_spec533#print axioms replayMove_eq534#print axioms terminal_nimSum_zero535#print axioms replay_correct536#print axioms two_scan_protocol537#print axioms replay_resources538#print axioms store_fold539#print axioms store_fold0540#print axioms store_correct541#print axioms eval_xorC542#print axioms enc_acc543#print axioms enc_prev544#print axioms enc_valid545#print axioms enc_tag546#print axioms enc_x547#print axioms circuit_update548#print axioms ofBits_testBit_eq549#print axioms circuit_step_correct550#print axioms circuit_resources551#print axioms xorNet_valid552#print axioms xorNet_correct553554end Recurrent555end NimAudit