LocalRestore

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 SelectCircuit23/- Phase 4, Priority 4: LOCAL two-frame delta and restoration circuits, and the4   bounded-change difference lemma.  Written by Claude (10 October 2026).5   Lean 4.26.0, core/Std only.67   Input: two frames Q (wires below B·N) and Q' (wires B·N … 2B·N − 1), each in the8   `boardBits` layout.  Nothing here computes a global nim-sum: every circuit is built9   from per-heap bit comparisons.10   * changed-row detection  `chgC i`  (OR over the block of bitwise XORs);11   * single-change delta    `dC q`    (OR over heaps of the bit-q XORs) — equal to12     nim(Q) ⊕ nim(Q') whenever the frames differ in at most one heap (`OneChange`,13     implied by any legal move);14   * restoration circuit    `restC`   = variable-target selector on Q' with σ := δ;15     under the zero-predecessor / legal-transition promise it outputs exactly the16     move of `NimGame.restore` (whose specification uses global nim-sums) and that17     move is legal and restores nim-sum 0;18   * bounded-change delta   `bdC t q` for any constant t: exact counting circuits19     "at least k of the heaps differ in bit q" give the parity of the at most t20     differing heaps; equal to nim(Q) ⊕ nim(Q') when at most t heaps changed21     (paper Lemma "bounded-change differences"), with depth 2t + 8 and size22     (2t+6)·U^(3t+6), U = N + t + 11. -/2324namespace NimAudit25namespace LocalRestore2627open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit2829/-- Two-frame input vector. -/30def tf (B N : Nat) (Q Q' : List Nat) : Nat → Bool := fun j =>31  if j < B * N then boardBits B Q j else boardBits B Q' (j - B * N)3233section Frames34variable {B N : Nat} {Q Q' : List Nat}3536theorem tf_left {j : Nat} (hj : j < B * N) : tf B N Q Q' j = boardBits B Q j := by simp [tf, hj]3738theorem tf_right (j : Nat) : tf B N Q Q' (B * N + j) = boardBits B Q' j := by39  simp only [tf, if_neg (show ¬ (B * N + j < B * N) by omega), Nat.add_sub_cancel_left]4041theorem tf_heapL (hQ : Q.length = N) {i p : Nat} (hi : i < N) (hp : p < B) :42    tf B N Q Q' (B * i + p) = (Q.getD i 0).testBit (B - 1 - p) := by43  rw [tf_left (heap_lt hi hp), boardBits_heap hQ hi hp]4445theorem tf_heapR (hQ' : Q'.length = N) {i p : Nat} (hi : i < N) (hp : p < B) :46    tf B N Q Q' (B * N + (B * i + p)) = (Q'.getD i 0).testBit (B - 1 - p) := by47  rw [tf_right, boardBits_heap hQ' hi hp]4849end Frames5051/-- Bitwise XOR of heap i of the two frames at big-endian position p. -/52def yC (B N i p : Nat) : Circ := xor2 (input (B * i + p)) (input (B * N + (B * i + p)))5354/-- Heap i changed between the frames. -/55def chgC (B N i : Nat) : Circ := or ((List.range B).map (yC B N i))5657/-- Little-endian bit q of the single-change delta: OR over heaps of the bit-q XORs. -/58def dC (B N q : Nat) : Circ := if q < B then or ((List.range N).map (fun i => yC B N i (B - 1 - q))) else const false5960theorem yC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N) {i p : Nat}61    (hi : i < N) (hp : p < B) :62    eval (tf B N Q Q') (yC B N i p) = ((Q.getD i 0).testBit (B - 1 - p) != (Q'.getD i 0).testBit (B - 1 - p)) := by63  simp only [yC, eval_xor2, eval_input, tf_heapL hQ hi hp, tf_heapR hQ' hi hp]64  try (cases (Q.getD i 0).testBit (B - 1 - p) <;> cases (Q'.getD i 0).testBit (B - 1 - p) <;> rfl)6566theorem testBit_ne_iff {x y B : Nat} (hx : x < 2 ^ B) (hy : y < 2 ^ B) :67    x ≠ y ↔ ∃ k < B, x.testBit k ≠ y.testBit k := by68  constructor69  · intro h70    apply Classical.byContradiction; intro hall71    apply h72    apply Nat.eq_of_testBit_eq73    intro k74    rcases Nat.lt_or_ge k B with hk | hk75    · apply Classical.byContradiction; intro hne; exact hall ⟨k, hk, hne⟩76    · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by decide) hk)),77        Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hy (Nat.pow_le_pow_right (by decide) hk))]78  · rintro ⟨k, _, hk⟩ h; subst h; exact hk rfl7980/-- CHANGED-ROW DETECTION. -/81theorem chgC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)82    (hw : Width B Q) (hw' : Width B Q') {i : Nat} (hi : i < N) :83    eval (tf B N Q Q') (chgC B N i) = decide (Q.getD i 0 ≠ Q'.getD i 0) := by84  apply Bool.eq_iff_iff.mpr85  rw [decide_eq_true_iff, testBit_ne_iff (getD_lt_of_width hQ hw hi) (getD_lt_of_width hQ' hw' hi)]86  simp only [chgC, eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp_apply]87  constructor88  · rintro ⟨p, hp, h⟩89    rw [yC_eval hQ hQ' hi hp] at h90    refine ⟨B - 1 - p, by omega, ?_⟩91    simpa using h92  · rintro ⟨k, hk, h⟩93    refine ⟨B - 1 - k, by omega, ?_⟩94    rw [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - k) = k by omega]95    simpa using h9697/-! ## Single-change delta -/9899/-- The frames differ in at most one heap. -/100def OneChange (Q Q' : List Nat) : Prop :=101  Q = Q' ∨ ∃ pre x post y, Q = pre ++ x :: post ∧ Q' = pre ++ y :: post102103theorem oneChange_of_move {Q Q' : List Nat} (h : Move Q Q') : OneChange Q Q' := by104  obtain ⟨pre, x, post, y, h1, h2, _⟩ := h105  exact Or.inr ⟨pre, x, post, y, h1, h2⟩106107theorem nimSum_split (pre post : List Nat) (x : Nat) :108    nimSum (pre ++ x :: post) = nimSum pre ^^^ (x ^^^ nimSum post) := by109  rw [NimAudit.nimSum_append]; rfl110111theorem delta_oneChange {pre post : List Nat} (x y : Nat) :112    nimSum (pre ++ x :: post) ^^^ nimSum (pre ++ y :: post) = x ^^^ y := by113  rw [nimSum_split, nimSum_split]114  apply Nat.eq_of_testBit_eq; intro k115  simp only [Nat.testBit_xor]116  cases (nimSum pre).testBit k <;> cases x.testBit k <;> cases y.testBit k <;>117    cases (nimSum post).testBit k <;> rfl118119theorem getD_split (pre post : List Nat) (x i : Nat) :120    (pre ++ x :: post).getD i 0 =121      if i < pre.length then pre.getD i 0 else if i = pre.length then x else post.getD (i - pre.length - 1) 0 := by122  simp only [List.getD_eq_getElem?_getD]123  by_cases h1 : i < pre.length124  · simp [h1, List.getElem?_append_left h1]125  · rw [List.getElem?_append_right (by omega)]126    by_cases h2 : i = pre.length127    · subst h2; simp128    · simp only [h1, h2, if_false]129      rw [show i - pre.length = (i - pre.length - 1) + 1 by omega, List.getElem?_cons_succ]130      simp only [Nat.add_sub_cancel]131132/-- The local delta value read off the circuit (no promise). -/133def localDelta (B N : Nat) (Q Q' : List Nat) : Nat :=134  ofBits B (fun q => (List.range N).any (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q))135136theorem dC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N) (q : Nat) :137    eval (tf B N Q Q') (dC B N q) = (localDelta B N Q Q').testBit q := by138  unfold dC localDelta139  rw [testBit_ofBits]140  by_cases hq : q < B141  · simp only [hq, if_true, decide_true, Bool.true_and, eval_or, List.any_map]142    apply Bool.eq_iff_iff.mpr143    simp only [List.any_eq_true, List.mem_range, Function.comp_apply]144    constructor145    · rintro ⟨i, hi, h⟩146      refine ⟨i, hi, ?_⟩147      rwa [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega] at h148    · rintro ⟨i, hi, h⟩149      refine ⟨i, hi, ?_⟩150      rwa [yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega]151  · simp [hq]152153/-- SINGLE-CHANGE DELTA: on frames differing in at most one heap the local delta is154    nim(Q) ⊕ nim(Q'). -/155theorem localDelta_eq {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)156    (hw : Width B Q) (hw' : Width B Q') (h1 : OneChange Q Q') :157    localDelta B N Q Q' = nimSum Q ^^^ nimSum Q' := by158  apply ofBits_testBit_eq (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw'))159  intro q _160  rcases h1 with rfl | ⟨pre, x, post, y, rfl, rfl⟩161  · simp162  · rw [delta_oneChange, Nat.testBit_xor]163    have hN : N = pre.length + 1 + post.length := by rw [← hQ]; simp; omega164    apply Bool.eq_iff_iff.mpr165    simp only [List.any_eq_true, List.mem_range, getD_split]166    constructor167    · rintro ⟨i, _, hi⟩168      by_cases h1 : i < pre.length169      · simp [h1] at hi170      · by_cases h2 : i = pre.length171        · simpa [h2] using hi172        · simp [h1, h2] at hi173    · intro h174      exact ⟨pre.length, by omega, by simpa using h⟩175176/-! ## The restoration circuit -/177178/-- Board wires read Q'; σ wires read the local delta circuits. -/179def restSubst (B N : Nat) : Nat → Circ := fun w => if w < B * N then input (B * N + w) else dC B N (w - B * N)180181def restC (B N : Nat) : RCirc := substR (restSubst B N) (varSel B N)182183theorem rest_inputs {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N) :184    (fun w => eval (tf B N Q Q') (restSubst B N w)) = selIn B N Q' (localDelta B N Q Q') := by185  funext w186  unfold restSubst selIn187  by_cases hw : w < B * N188  · simp only [hw, if_true, eval_input, tf_right]189  · simp only [hw, if_false]190    exact dC_eval hQ hQ' _191192/-- RESTORATION CIRCUIT (no promise): it outputs `attainT δ Q'` for the local delta δ. -/193theorem restC_eval {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)194    (hw' : Width B Q') :195    selReadout (restC B N) (tf B N Q Q') = attainT (localDelta B N Q Q') Q' := by196  unfold restC197  rw [selReadout_subst, rest_inputs hQ hQ']198  exact varSel_correct hQ' hw' (ofBits_lt B _)199200theorem cancelFirst_eq (t : Nat) : ∀ P : List Nat, cancelFirst t P = applyM P (cancelIdx t P)201  | [] => rfl202  | x :: rest => by203    by_cases h : x ^^^ t < x204    · simp [cancelFirst, cancelIdx, h, applyM]205    · simp only [cancelFirst, cancelIdx, h, if_false]206      rw [applyM_shift, cancelFirst_eq t rest]207208/-- LOCAL RESTORATION EQUIVALENCE: under the zero-predecessor / legal-transition209    promise (nim(Q) = 0 and Q → Q' a legal move), the purely local circuit outputs a210    move (i, v) whose application is exactly `NimGame.restore Q Q'`; the move is legal211    and restores nim-sum 0. -/212theorem restore_equiv {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)213    (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :214    ∃ i v, selReadout (restC B N) (tf B N Q Q') = some (i, v) ∧215      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by216  rw [restC_eval hQ hQ' hw', localDelta_eq hQ hQ' hw hw' (oneChange_of_move hm)]217  obtain ⟨R, hR, hmR, hzR⟩ := restore_correct h0 hm218  have hR' := hR219  unfold restore at hR'220  rw [cancelFirst_eq] at hR'221  cases hc : cancelIdx (nimSum Q ^^^ nimSum Q') Q' with222  | none => rw [hc] at hR'; cases hR'223  | some m =>224    obtain ⟨i, v⟩ := m225    rw [hc] at hR'226    simp only [applyM, Option.some.injEq] at hR'227    subst hR'228    refine ⟨i, v, ?_, hR, hmR, hzR⟩229    unfold attainT; rw [hc]230231/-! ## Bounded-change differences (any constant t) -/232233/-- Number of indices below n satisfying p. -/234def cntR (p : Nat → Bool) (n : Nat) : Nat := ((List.range n).filter p).length235236theorem cntR_zero (p : Nat → Bool) : cntR p 0 = 0 := rfl237238theorem cntR_succ (p : Nat → Bool) (n : Nat) : cntR p (n + 1) = cntR p n + (if p n then 1 else 0) := by239  unfold cntR240  rw [List.range_succ, List.filter_append, List.length_append]241  cases h : p n <;> simp [h]242243theorem cntR_mono {p p' : Nat → Bool} (n : Nat) (h : ∀ i < n, p i = true → p' i = true) :244    cntR p n ≤ cntR p' n := by245  induction n with246  | zero => simp [cntR_zero]247  | succ n ih =>248    rw [cntR_succ, cntR_succ]249    have := ih (fun i hi => h i (by omega))250    cases hp : p n251    · simp only [Bool.false_eq_true, if_false]; split <;> omega252    · simp [h n (by omega) hp]; omega253254/-- "At least k of y 0, …, y (n-1) are true". -/255def atLeastC (y : Nat → Circ) : Nat → Nat → Circ256  | 0, _ => const true257  | k + 1, n => or ((List.range n).map (fun i => and [y i, atLeastC y k i]))258259theorem atLeastC_eval (z : Nat → Bool) (y : Nat → Circ) :260    ∀ k n, eval z (atLeastC y k n) = decide (k ≤ cntR (fun i => eval z (y i)) n)261  | 0, n => by simp [atLeastC]262  | k + 1, n => by263    induction n with264    | zero => simp [atLeastC, cntR_zero]265    | succ n ih =>266      have e : atLeastC y (k + 1) (n + 1) =267          or ((List.range n).map (fun i => and [y i, atLeastC y k i]) ++ [and [y n, atLeastC y k n]]) := by268        simp [atLeastC, List.range_succ]269      rw [e, eval_or, List.any_append, cntR_succ]270      have ih' : ((List.range n).map (fun i => and [y i, atLeastC y k i])).any (eval z) =271          decide (k + 1 ≤ cntR (fun i => eval z (y i)) n) := by272        rw [← ih]; simp [atLeastC]273      rw [ih']274      simp only [List.any_cons, List.any_nil, Bool.or_false, eval_and, List.all_cons, List.all_nil,275        Bool.and_true, atLeastC_eval z y k n]276      cases hy : eval z (y n) <;> simp [hy] <;> omega277278/-- Parity of the number of true y_i, valid when at most t are true. -/279def parC (y : Nat → Circ) (t n : Nat) : Circ :=280  or ((List.range (t + 1)).map (fun k =>281    if k % 2 = 1 then and [atLeastC y k n, not (atLeastC y (k + 1) n)] else const false))282283theorem parC_eval (z : Nat → Bool) (y : Nat → Circ) (t n : Nat)284    (ht : cntR (fun i => eval z (y i)) n ≤ t) :285    eval z (parC y t n) = decide (cntR (fun i => eval z (y i)) n % 2 = 1) := by286  generalize hc : cntR (fun i => eval z (y i)) n = c at ht287  apply Bool.eq_iff_iff.mpr288  simp only [parC, eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp_apply,289    decide_eq_true_iff]290  constructor291  · rintro ⟨k, _, hk⟩292    by_cases hodd : k % 2 = 1293    · simp only [hodd, if_true, eval_and, List.all_cons, List.all_nil, Bool.and_true, eval_not,294        atLeastC_eval, hc, Bool.and_eq_true, decide_eq_true_iff, Bool.not_eq_true',295        decide_eq_false_iff_not] at hk296      have : k = c := by omega297      subst this; exact hodd298    · simp [hodd] at hk299  · intro h300    refine ⟨c, by omega, ?_⟩301    simp [h, atLeastC_eval, hc]302303/-- Little-endian bit q of the bounded-change delta (t = maximum number of changed heaps). -/304def bdC (B N t q : Nat) : Circ := if q < B then parC (fun i => yC B N i (B - 1 - q)) t N else const false305306/-- Parity of the bit-q differences equals bit q of nim(Q) ⊕ nim(Q'). -/307theorem nimSum_xor_testBit : ∀ (Q Q' : List Nat), Q.length = Q'.length → ∀ q,308    (nimSum Q ^^^ nimSum Q').testBit q =309      decide (cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) Q.length % 2 = 1)310  | [], [], _, q => by simp [nimSum, cntR_zero]311  | x :: Q, y :: Q', hl, q => by312    have hl' : Q.length = Q'.length := by simpa using hl313    have ih := nimSum_xor_testBit Q Q' hl' q314    have hshift : cntR (fun i => ((x :: Q).getD i 0).testBit q != ((y :: Q').getD i 0).testBit q)315        (Q.length + 1) = (if x.testBit q != y.testBit q then 1 else 0) +316          cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) Q.length := by317      unfold cntR318      rw [List.range_succ_eq_map, List.filter_cons, List.filter_map]319      simp only [List.getD_cons_zero, Function.comp_def, List.getD_cons_succ]320      by_cases hc : (x.testBit q != y.testBit q) = true321      · simp only [hc, if_true, List.length_cons, List.length_map]; omega322      · simp only [hc, Bool.false_eq_true, if_false, List.length_map]; omega323    simp only [List.length_cons]324    simp only [hshift]325    have e : (nimSum (x :: Q) ^^^ nimSum (y :: Q')).testBit q =326        xor (x.testBit q != y.testBit q) ((nimSum Q ^^^ nimSum Q').testBit q) := by327      simp only [nimSum, Nat.testBit_xor]328      cases x.testBit q <;> cases y.testBit q <;> cases (nimSum Q).testBit q <;>329        cases (nimSum Q').testBit q <;> rfl330    rw [e, ih]331    generalize cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) Q.length = c332    cases hxy : (x.testBit q != y.testBit q)333    · simp only [Bool.false_xor, Bool.false_eq_true, if_false, Nat.zero_add]334    · simp only [Bool.true_xor, if_true]335      by_cases hc : c % 2 = 1336      · have : ¬ (1 + c) % 2 = 1 := by omega337        simp [hc, this]338      · have : (1 + c) % 2 = 1 := by omega339        simp [hc, this]340  | [], _ :: _, hl, _ => by simp at hl341  | _ :: _, [], hl, _ => by simp at hl342343/-- BOUNDED-CHANGE DIFFERENCES: if at most t heaps changed, the delta circuits compute344    nim(Q) ⊕ nim(Q') exactly. -/345theorem bdC_eval {B N t : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)346    (hw : Width B Q) (hw' : Width B Q')347    (ht : cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t) (q : Nat) :348    eval (tf B N Q Q') (bdC B N t q) = (nimSum Q ^^^ nimSum Q').testBit q := by349  unfold bdC350  by_cases hq : q < B351  · simp only [hq, if_true]352    have hyc : (fun i => eval (tf B N Q Q') (yC B N i (B - 1 - q))) =353        fun i => if i < N then ((Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) else354          eval (tf B N Q Q') (yC B N i (B - 1 - q)) := by355      funext i356      by_cases hi : i < N357      · rw [if_pos hi, yC_eval hQ hQ' hi (by omega), show B - 1 - (B - 1 - q) = q by omega]358      · rw [if_neg hi]359    have hcnt : cntR (fun i => eval (tf B N Q Q') (yC B N i (B - 1 - q))) N =360        cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) N := by361      unfold cntR362      congr 1363      apply List.filter_congr364      intro i hi365      rw [yC_eval hQ hQ' (List.mem_range.mp hi) (by omega), show B - 1 - (B - 1 - q) = q by omega]366    have hle : cntR (fun i => (Q.getD i 0).testBit q != (Q'.getD i 0).testBit q) N ≤ t := by367      refine Nat.le_trans (cntR_mono N (fun i hi h => ?_)) ht368      simp only [bne_iff_ne, ne_eq] at h369      simp only [decide_eq_true_iff]370      intro he; rw [he] at h; exact h rfl371    rw [parC_eval _ _ t N (by rw [hcnt]; exact hle), hcnt,372      nimSum_xor_testBit Q Q' (by rw [hQ, hQ']) q, hQ]373  · simp only [hq, if_false, eval_const]374    rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw'))375      (Nat.pow_le_pow_right (by decide) (by omega)))]376377theorem bdDelta_eq {B N t : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)378    (hw : Width B Q) (hw' : Width B Q')379    (ht : cntR (fun i => decide (Q.getD i 0 ≠ Q'.getD i 0)) N ≤ t) :380    ofBits B (fun q => eval (tf B N Q Q') (bdC B N t q)) = nimSum Q ^^^ nimSum Q' :=381  ofBits_testBit_eq (Nat.xor_lt_two_pow (nimSum_lt hw) (nimSum_lt hw')) _382    (fun q _ => bdC_eval hQ hQ' hw hw' ht q)383384/-! ## Resources -/385386section Res387variable {B N : Nat}388389theorem yC_res (i p : Nat) : depth (yC B N i p) ≤ 3 ∧ size (yC B N i p) ≤ 9 := by390  simp [yC, xor2, listMax]391392theorem yC_max {i p : Nat} (hi : i < N) (hp : p < B) : maxInput (yC B N i p) ≤ 2 * (B * N) := by393  have := heap_lt (B := B) (N := N) hi hp394  simp [yC, xor2, listMax]; omega395396theorem dC_res (q : Nat) : depth (dC B N q) ≤ 4 ∧ size (dC B N q) ≤ 10 * N + 1 ∧397    maxInput (dC B N q) ≤ 2 * (B * N) := by398  unfold dC399  by_cases hq : q < B400  · simp only [hq, if_true]401    refine ⟨?_, ?_, ?_⟩402    · apply depth_or_le; intro c hc; obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (yC_res _ _).1403    · have := ControllerBits.size_or_le' (S := 9) (cs := (List.range N).map (fun i => yC B N i (B - 1 - q)))404        (by intro c hc; obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (yC_res _ _).2)405      simp only [List.length_map, List.length_range] at this; omega406    · apply ControllerBits.maxInput_or_le; intro c hc407      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc408      exact yC_max (List.mem_range.mp hi) (by omega)409  · simp [hq]410411theorem chgC_res {i : Nat} (hi : i < N) : depth (chgC B N i) ≤ 4 ∧ size (chgC B N i) ≤ 10 * B + 1 ∧412    maxInput (chgC B N i) ≤ 2 * (B * N) := by413  unfold chgC414  refine ⟨?_, ?_, ?_⟩415  · apply depth_or_le; intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; exact (yC_res _ _).1416  · have := ControllerBits.size_or_le' (S := 9) (cs := (List.range B).map (yC B N i))417      (by intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; exact (yC_res _ _).2)418    simp only [List.length_map, List.length_range] at this; omega419  · apply ControllerBits.maxInput_or_le; intro c hc420    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc421    exact yC_max hi (List.mem_range.mp hp)422423/-- The restoration circuit: depth ≤ 17, polynomial size, reading only the two frames. -/424theorem restC_bound :425    SelBound (restC B N) N B (4 + 9 + 4)426      (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1)) (2 * (B * N)) := by427  apply substR_bound (restSubst B N) varSel_bound428  · intro w; unfold restSubst; split429    · simp430    · exact (dC_res _).1431  · intro w; unfold restSubst; split432    · simp433    · exact (dC_res _).2.1434  · intro w; unfold restSubst; split435    · simp; omega436    · exact (dC_res _).2.2437438theorem atLeast_res {U dy : Nat} (hU : 2 ≤ U) (y : Nat → Circ) (hy : ∀ i, size (y i) ≤ U ∧ depth (y i) ≤ dy) :439    ∀ k n, n ≤ U → size (atLeastC y k n) ≤ (2 * k + 1) * U ^ (3 * k) ∧ depth (atLeastC y k n) ≤ 2 * k + dy440  | 0, n, _ => by simp [atLeastC]441  | k + 1, n, hn => by442    have hU1 : 1 ≤ U := by omega443    refine ⟨?_, ?_⟩444    · show size (or ((List.range n).map (fun i => and [y i, atLeastC y k i]))) ≤ _445      have e : (2 * (k + 1) + 1) * U ^ (3 * (k + 1)) = ((2 * k + 2) + 1) * U ^ ((3 * k + 2) + 1) := by446        congr 1447      rw [e]448      apply size_or_le hU1 (by simp; omega)449      intro c hc450      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc451      have hi' := List.mem_range.mp hi452      apply size_and_le hU1 (by simp; omega)453      intro c hc454      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc455      rcases hc with rfl | rfl456      · exact lift1 hU1 (show size (y i) ≤ 1 * U ^ 1 by simp; exact (hy i).1) (by omega) (by omega)457      · exact lift1 hU1 (atLeast_res hU y hy k i (by omega)).1 (by omega) (by omega)458    · show depth (or ((List.range n).map (fun i => and [y i, atLeastC y k i]))) ≤ _459      refine Nat.le_trans (depth_or_le (D := 2 * k + dy + 1) ?_) (by omega)460      intro c hc461      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc462      have hi' := List.mem_range.mp hi463      apply depth_and_le464      intro c hc465      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc466      rcases hc with rfl | rfl467      · have := (hy i).2; omega468      · have := (atLeast_res hU y hy k i (by omega)).2; omega469470theorem atLeast_max (y : Nat → Circ) {M n0 : Nat} (hy : ∀ i < n0, maxInput (y i) ≤ M) :471    ∀ k n, n ≤ n0 → maxInput (atLeastC y k n) ≤ M472  | 0, _, _ => by simp [atLeastC]473  | k + 1, n, hn => by474    show maxInput (or ((List.range n).map (fun i => and [y i, atLeastC y k i]))) ≤ M475    apply ControllerBits.maxInput_or_le; intro c hc476    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc477    have hi' := List.mem_range.mp hi478    apply ControllerBits.maxInput_and_le; intro c hc479    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc480    rcases hc with rfl | rfl481    · exact hy i (by omega)482    · exact atLeast_max y hy k i (by omega)483484theorem parC_res {U dy : Nat} (hU : 2 ≤ U) (y : Nat → Circ) (hy : ∀ i, size (y i) ≤ U ∧ depth (y i) ≤ dy)485    (t n : Nat) (hn : n ≤ U) (ht : t + 1 ≤ U) :486    size (parC y t n) ≤ (2 * t + 6) * U ^ (3 * t + 6) ∧ depth (parC y t n) ≤ 2 * t + dy + 5 := by487  have hU1 : 1 ≤ U := by omega488  refine ⟨?_, ?_⟩489  · unfold parC490    have e : (2 * t + 6) * U ^ (3 * t + 6) = ((2 * t + 5) + 1) * U ^ ((3 * t + 5) + 1) := by congr 1491    rw [e]492    apply size_or_le hU1 (by simp; omega)493    intro c hc494    obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc495    have hk' := List.mem_range.mp hk496    split497    · apply size_and_le hU1 (by simp; omega)498      intro c hc499      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc500      rcases hc with rfl | rfl501      · exact lift1 hU1 (atLeast_res hU y hy k n hn).1 (by omega) (by omega)502      · exact lift1 hU1 (size_not_le hU1 (atLeast_res hU y hy (k + 1) n hn).1) (by omega) (by omega)503    · exact lift1 hU1 (show size (const false) ≤ 1 * U ^ 0 by simp) (by omega) (by omega)504  · unfold parC505    apply depth_or_le506    intro c hc507    obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc508    have hk' := List.mem_range.mp hk509    split510    · apply depth_and_le511      intro c hc512      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc513      rcases hc with rfl | rfl514      · have := (atLeast_res hU y hy k n hn).2; omega515      · simp only [depth_not]; have := (atLeast_res hU y hy (k + 1) n hn).2; omega516    · simp517518/-- BOUNDED-CHANGE DELTA RESOURCES: depth ≤ 2t + 8 and size ≤ (2t+6)·U^(3t+6) with519    U = N + t + 11; inputs from the two frames only.  Constant depth and polynomial size520    for every fixed t. -/521theorem bdC_res (t q : Nat) :522    depth (bdC B N t q) ≤ 2 * t + 8 ∧ size (bdC B N t q) ≤ (2 * t + 6) * (N + t + 11) ^ (3 * t + 6) ∧523      maxInput (bdC B N t q) ≤ 2 * (B * N) := by524  unfold bdC525  by_cases hq : q < B526  · simp only [hq, if_true]527    have hy : ∀ i, size (yC B N i (B - 1 - q)) ≤ N + t + 11 ∧ depth (yC B N i (B - 1 - q)) ≤ 3 :=528      fun i => ⟨by have := (yC_res (B := B) (N := N) i (B - 1 - q)).2; omega, (yC_res i _).1⟩529    have h := parC_res (by omega) _ hy t N (by omega) (by omega)530    refine ⟨by omega, h.1, ?_⟩531    unfold parC532    apply ControllerBits.maxInput_or_le; intro c hc533    obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc534    split535    · apply ControllerBits.maxInput_and_le; intro c hc536      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc537      have hyM : ∀ i < N, maxInput (yC B N i (B - 1 - q)) ≤ 2 * (B * N) := fun i hi => yC_max hi (by omega)538      rcases hc with rfl | rfl539      · exact atLeast_max _ hyM k N (Nat.le_refl _)540      · simp only [maxInput_not]; exact atLeast_max _ hyM (k + 1) N (Nat.le_refl _)541    · simp542  · simp only [hq, if_false, depth_const, size_const, maxInput_const]543    refine ⟨by omega, ?_, by omega⟩544    have h1 : 1 ≤ (N + t + 11) ^ (3 * t + 6) := Nat.pow_pos (by omega)545    exact Nat.le_trans h1 (Nat.le_mul_of_pos_left _ (by omega))546547end Res548549550/-! ## Axiom audit -/551552#print axioms tf_left553#print axioms tf_right554#print axioms tf_heapL555#print axioms tf_heapR556#print axioms yC_eval557#print axioms testBit_ne_iff558#print axioms chgC_eval559#print axioms oneChange_of_move560#print axioms nimSum_split561#print axioms delta_oneChange562#print axioms getD_split563#print axioms dC_eval564#print axioms localDelta_eq565#print axioms rest_inputs566#print axioms restC_eval567#print axioms cancelFirst_eq568#print axioms restore_equiv569#print axioms cntR_zero570#print axioms cntR_succ571#print axioms cntR_mono572#print axioms atLeastC_eval573#print axioms parC_eval574#print axioms nimSum_xor_testBit575#print axioms bdC_eval576#print axioms bdDelta_eq577#print axioms yC_res578#print axioms yC_max579#print axioms dC_res580#print axioms chgC_res581#print axioms restC_bound582#print axioms atLeast_res583#print axioms atLeast_max584#print axioms parC_res585#print axioms bdC_res586end LocalRestore587end NimAudit