SelectCircuit

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 ControllerBits23/- Phase 4, Priority 4: constructive selection circuits.  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   * A GENERIC first-index move selector `genSel` (primary test with its new value,7     fallback "subtract 1 from the first nonzero heap"), with one exactness theorem8     `genSel_correct` reused by every instance below.9   * VARIABLE-TARGET selector `varSel`: the target σ arrives on B input wires (it is10     not a constant baked into the circuit, unlike phase-3 `attRC`); it computes11     `attainT σ P` = `replayMove σ P` (cancel σ at the first qualifying heap, else12     the fallback, else halt).13   * MULTI-HEAD selector `mhSel`: σ is reconstructed inside the circuit from the B14     rollout-outcome wires (σ₀ = o₀, σⱼ = oⱼ ⊕ o₀); on the true outcomes it outputs15     `decisionMove P`, the same verified move as the recurrent controller.16   * POLICY-STEP circuits `polSel j` for π_j (threshold eligibility 2^j ≤ x, first17     eligible heap, subtraction of 2^j, fallback subtract-1): exact for `policyStep`.18   Input layout: board bits as in `CorrBridge.boardBits` (heap i, big-endian position19   p at wire B·i + p) on wires below B·N; extra wires (σ or outcomes) from B·N on. -/2021namespace NimAudit22namespace SelectCircuit2324open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge2526/-- Evaluation of a move readout on an arbitrary input vector. -/27def selReadout (R : RCirc) (z : Nat → Bool) : Option (Nat × Nat) :=28  if eval z R.valid then29    match firstTrue (R.sel.map (eval z)) with30    | some i => some (i, toNatBE (R.val.map (eval z)))31    | none => none32  else none3334theorem readoutOf_eq (B : Nat) (R : Bool → RCirc) (P : List Nat) (b : Bool) :35    readoutOf B R P b = selReadout (R b) (boardBits B P) := rfl3637/-- Substitution into all formulas of a readout. -/38def substR (τ : Nat → Circ) (R : RCirc) : RCirc := ⟨subst τ R.valid, R.sel.map (subst τ), R.val.map (subst τ)⟩3940theorem selReadout_subst (τ : Nat → Circ) (R : RCirc) (z : Nat → Bool) :41    selReadout (substR τ R) z = selReadout R (fun w => eval z (τ w)) := by42  have h : (eval z ∘ subst τ) = eval (fun w => eval z (τ w)) := funext (fun c => eval_subst τ z c)43  simp only [selReadout, substR, List.map_map, h, eval_subst]4445def orFirst (N : Nat) (cs bs : Nat → Circ) : Circ :=46  or ((List.range N).map (fun i => and [firstC cs i, bs i]))4748theorem orFirst_eval {N : Nat} (z : Nat → Bool) (cs bs : Nat → Circ) :49    eval z (orFirst N cs bs) =50      match firstTrue ((List.range N).map (fun i => eval z (cs i))) with51      | some i => eval z (bs i)52      | none => false := by53  apply Bool.eq_iff_iff.mpr54  simp only [orFirst, eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp_apply,55    eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true]56  constructor57  · rintro ⟨i, hi, hf, hb⟩58    rw [firstC_eval (N := N) z cs hi, decide_eq_true_iff] at hf59    rw [hf]; exact hb60  · intro h61    cases hft : firstTrue ((List.range N).map (fun i => eval z (cs i))) with62    | none => rw [hft] at h; cases h63    | some i =>64      rw [hft] at h65      have hi : i < N := by have := firstTrue_lt hft; simpa using this66      exact ⟨i, hi, by rw [firstC_eval (N := N) z cs hi, decide_eq_true_iff]; exact hft, h⟩6768theorem firstTrue_isSome (l : List Bool) : (firstTrue l).isSome = l.any id := by69  induction l with70  | nil => rfl71  | cons b l ih => cases b <;> simp [firstTrue, ih]7273/-! ## The generic selector -/7475/-- First heap passing a primary test, with its new value. -/76def firstIdx (pr : Nat → Bool) (f : Nat → Nat) (P : List Nat) : Option (Nat × Nat) :=77  (firstTrue (P.map pr)).map (fun i => (i, f (P.getD i 0)))7879/-- Primary choice, else fallback (first nonzero heap minus one), else halt. -/80def primOr (pr : Nat → Bool) (f : Nat → Nat) (P : List Nat) : Option (Nat × Nat) :=81  match firstIdx pr f P with82  | some m => some m83  | none => decIdx P8485def anyC' (N : Nat) (prim : Nat → Circ) : Circ := or ((List.range N).map prim)8687def genSel (B N : Nat) (prim : Nat → Circ) (pv : Nat → Nat → Circ) : RCirc :=88  ⟨validA B N,89   (List.range N).map (fun i => or [prim i, and [not (anyC' N prim), AttainCircuit.nzC B i]]),90   (List.range B).map (fun p => or [and [anyC' N prim, orFirst N prim (fun i => pv i p)],91     and [not (anyC' N prim), orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p)]])⟩9293section GenSel94variable {B N : Nat} {P : List Nat}9596theorem max_nzC {i : Nat} (hi : i < N) : maxInput (AttainCircuit.nzC B i) ≤ B * N := by97  unfold AttainCircuit.nzC98  apply ControllerBits.maxInput_or_le; intro c hc99  obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc100  have := List.mem_range.mp hp101  have : B * i + B ≤ B * N := by rw [← Nat.mul_succ]; exact Nat.mul_le_mul_left _ hi102  simp; omega103104theorem max_decbitC {i p : Nat} (hi : i < N) (hp : p < B) : maxInput (decbitC B i p) ≤ B * N := by105  have hb : B * i + B ≤ B * N := by rw [← Nat.mul_succ]; exact Nat.mul_le_mul_left _ hi106  have h1 : maxInput (lowZeroC B i p) ≤ B * N := by107    unfold lowZeroC108    apply ControllerBits.maxInput_and_le; intro c hc109    obtain ⟨r, hr, rfl⟩ := List.mem_map.mp hc110    have := List.mem_range.mp hr111    simp; omega112  unfold decbitC xor2113  generalize lowZeroC B i p = L at h1114  simp only [maxInput_or, maxInput_and, maxInput_not, maxInput_input, List.map_cons, List.map_nil,115    listMax, List.foldr_cons, List.foldr_nil]116  omega117118theorem decbit_eval (hP : P.length = N) {i p : Nat} (hi : i < N) (hp : p < B) (hpos : 0 < P.getD i 0) :119    eval (boardBits B P) (decbitC B i p) = (P.getD i 0 - 1).testBit (B - 1 - p) := by120  rw [testBit_pred _ hpos]121  unfold decbitC122  rw [eval_xor2, eval_input, boardBits_heap hP hi hp]123  congr 1124  unfold lowZeroC125  apply Bool.eq_iff_iff.mpr126  simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp_apply,127    eval_not, eval_input, Bool.not_eq_true', decide_eq_true_iff]128  constructor129  · intro h j hj130    have := h (B - 1 - p - 1 - j) (by omega)131    rw [boardBits_heap hP hi (by omega)] at this132    rwa [show B - 1 - (p + 1 + (B - 1 - p - 1 - j)) = j by omega] at this133  · intro h r hr134    rw [boardBits_heap hP hi (by omega)]135    exact h _ (by omega)136137theorem getD_lt_of_width (hP : P.length = N) (hw : Width B P) {i : Nat} (hi : i < N) :138    P.getD i 0 < 2 ^ B := by139  apply hw; simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp140141theorem map_getD_eq (hP : P.length = N) {f : Nat → Bool} {g : Nat → Bool}142    (h : ∀ i < N, g i = f (P.getD i 0)) : (List.range N).map g = P.map f := by143  rw [← range_map_getD f P, hP]144  apply List.map_congr_left; intro i hi; exact h i (List.mem_range.mp hi)145146theorem firstTrue_map_getD {l : List Bool} {i : Nat} (pr : Nat → Bool) (hl : l = P.map pr)147    (h : firstTrue l = some i) : i < P.length ∧ pr (P.getD i 0) = true := by148  obtain ⟨hlen, hb, _⟩ := (firstTrue_some_iff _ i).1 h149  subst hl150  rw [List.length_map] at hlen151  refine ⟨hlen, ?_⟩152  simp only [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_eq_getElem hlen] at hb ⊢153  simpa using hb154155/-- GENERIC SELECTOR EXACTNESS. -/156theorem genSel_correct (hP : P.length = N) (hw : Width B P) (z : Nat → Bool)157    (hz : ∀ j < B * N, z j = boardBits B P j) (prim : Nat → Circ) (pv : Nat → Nat → Circ)158    (pr : Nat → Bool) (f : Nat → Nat)159    (hpr : ∀ i < N, eval z (prim i) = pr (P.getD i 0))160    (hpos : ∀ x, pr x = true → 0 < x)161    (hf : ∀ x, pr x = true → x < 2 ^ B → f x < 2 ^ B)162    (hpv : ∀ i < N, ∀ p < B, pr (P.getD i 0) = true →163      eval z (pv i p) = (f (P.getD i 0)).testBit (B - 1 - p)) :164    selReadout (genSel B N prim pv) z = primOr pr f P := by165  have hnzz : ∀ i < N, eval z (AttainCircuit.nzC B i) = decide (0 < P.getD i 0) := by166    intro i hi167    rw [eval_congr_below z (boardBits B P) _ (fun j hj => hz j (Nat.lt_of_lt_of_le hj (max_nzC hi))),168      nz_eval hP hw hi]169  have hdbz : ∀ i < N, ∀ p < B, 0 < P.getD i 0 →170      eval z (decbitC B i p) = (P.getD i 0 - 1).testBit (B - 1 - p) := by171    intro i hi p hp hpos'172    rw [eval_congr_below z (boardBits B P) _173      (fun j hj => hz j (Nat.lt_of_lt_of_le hj (max_decbitC hi hp))), decbit_eval hP hi hp hpos']174  have hcan : (List.range N).map (fun i => eval z (prim i)) = P.map pr := map_getD_eq hP hpr175  have hnz : (List.range N).map (fun i => eval z (AttainCircuit.nzC B i)) = P.map (fun x => decide (0 < x)) :=176    map_getD_eq hP hnzz177  have hany : eval z (anyC' N prim) = (P.map pr).any id := by178    unfold anyC'; rw [eval_or, ← hcan, List.any_map, List.any_map]; rfl179  have hsel : (genSel B N prim pv).sel.map (eval z) =180      (List.range N).map (fun i => eval z (prim i) ||181        (!((List.range N).any (fun i => eval z (prim i))) && eval z (AttainCircuit.nzC B i))) := by182    unfold genSel183    rw [List.map_map]184    apply List.map_congr_left; intro i _185    simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil,186      List.all_cons, List.all_nil, Bool.or_false, Bool.and_true, anyC', List.any_map]187    rfl188  have hvalid : eval z (genSel B N prim pv).valid = (P.map (fun x => decide (0 < x))).any id := by189    unfold genSel validA; rw [eval_or, ← hnz, List.any_map, List.any_map]; rfl190  have hanyR : (List.range N).any (fun i => eval z (prim i)) = (P.map pr).any id := by191    rw [← hcan, List.any_map]; rfl192  unfold selReadout primOr firstIdx193  rw [hsel, firstTrue_or, hvalid, hanyR, hcan, hnz, decIdx_firstTrue]194  by_cases hA : (P.map pr).any id = true195  · rw [← firstTrue_isSome] at hA196    obtain ⟨i, hi⟩ := Option.isSome_iff_exists.mp hA197    obtain ⟨hiN, hpri⟩ := firstTrue_map_getD pr rfl hi198    rw [hP] at hiN199    have hvalidT : (P.map (fun x => decide (0 < x))).any id = true := by200      rw [List.any_map]; apply List.any_eq_true.mpr201      exact ⟨P.getD i 0, by202        simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp,203        by simpa using hpos _ hpri⟩204    rw [firstTrue_isSome] at hA205    simp only [hvalidT, if_true, hA, hi, Option.map_some]206    congr 2207    have hxlt := getD_lt_of_width hP hw hiN208    simp only [genSel, List.map_map]209    apply toNatBE_of_bits (hf _ hpri hxlt)210    intro p hp211    simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil, List.all_cons,212      List.all_nil, Bool.and_true, Bool.or_false, hany, hA, Bool.not_true, Bool.false_and,213      Bool.true_and]214    rw [orFirst_eval, hcan, hi]215    exact hpv i hiN p hp hpri216  · have hnone : firstTrue (P.map pr) = none := by217      cases h : firstTrue (P.map pr) with218      | none => rfl219      | some i =>220        exfalso; apply hA; rw [← firstTrue_isSome, h]; rfl221    have hA' : (P.map pr).any id = false := by simpa using hA222    simp only [hA', Bool.false_eq_true, if_false, hnone, Option.map_none]223    by_cases hV : (P.map (fun x => decide (0 < x))).any id = true224    · simp only [hV, if_true]225      rw [← firstTrue_isSome] at hV226      obtain ⟨i, hi⟩ := Option.isSome_iff_exists.mp hV227      obtain ⟨hiN, hposi⟩ := firstTrue_map_getD (fun x => decide (0 < x)) rfl hi228      rw [hP] at hiN229      simp only [hi, Option.map_some]230      congr 2231      have hxlt := getD_lt_of_width hP hw hiN232      have hpos' : 0 < P.getD i 0 := by simpa using hposi233      simp only [genSel, List.map_map]234      apply toNatBE_of_bits (Nat.lt_of_le_of_lt (Nat.sub_le _ _) hxlt)235      intro p hp236      simp only [Function.comp_apply, eval_or, eval_and, eval_not, List.any_cons, List.any_nil, List.all_cons,237        List.all_nil, Bool.and_true, Bool.or_false, hany, hA', Bool.not_false, Bool.false_and,238        Bool.true_and, Bool.false_or]239      rw [orFirst_eval, hnz, hi]240      exact hdbz i hiN p hp hpos'241    · have hV' : (P.map (fun x => decide (0 < x))).any id = false := by simpa using hV242      have hnone' : firstTrue (P.map (fun x => decide (0 < x))) = none := by243        cases h : firstTrue (P.map (fun x => decide (0 < x))) with244        | none => rfl245        | some i => exfalso; apply hV; rw [← firstTrue_isSome, h]; rfl246      simp [hV', hnone']247248end GenSel249250/-! ## Index form versus list form of moves -/251252theorem firstIdx_cons (pr : Nat → Bool) (f : Nat → Nat) (x : Nat) (rest : List Nat) :253    firstIdx pr f (x :: rest) =254      if pr x then some (0, f x) else (firstIdx pr f rest).map (fun m => (m.1 + 1, m.2)) := by255  unfold firstIdx256  cases h : pr x257  · simp only [List.map_cons, h, firstTrue, Bool.false_eq_true, if_false]258    cases firstTrue (rest.map pr) <;> simp259  · simp [h, firstTrue]260261theorem cancelIdx_eq_firstIdx (t : Nat) (P : List Nat) :262    cancelIdx t P = firstIdx (fun x => decide (x ^^^ t < x)) (fun x => x ^^^ t) P := by263  rw [cancelIdx_firstTrue]; rfl264265theorem attainT_eq_primOr (t : Nat) (P : List Nat) :266    attainT t P = primOr (fun x => decide (x ^^^ t < x)) (fun x => x ^^^ t) P := by267  unfold attainT primOr; rw [cancelIdx_eq_firstIdx]268  cases firstIdx (fun x => decide (x ^^^ t < x)) (fun x => x ^^^ t) P <;> rfl269270theorem cancelIdx_zero (P : List Nat) : cancelIdx 0 P = none := by271  induction P with272  | nil => rfl273  | cons x P ih => simp [cancelIdx, ih]274275/-- The variable-target selection is the replay move of the recurrent controller. -/276theorem attainT_eq_replayMove (σ : Nat) (P : List Nat) : attainT σ P = replayMove σ P := by277  rw [replayMove_eq]278  unfold attainT selFor279  by_cases h : σ = 0280  · subst h; simp [cancelIdx_zero, firstSome]281  · simp only [h, if_false]282    cases cancelIdx σ P <;> rfl283284/-- Applying an index-form move. -/285def applyM (P : List Nat) : Option (Nat × Nat) → Option (List Nat)286  | some m => some (P.set m.1 m.2)287  | none => none288289theorem applyM_shift (x : Nat) (rest : List Nat) (o : Option (Nat × Nat)) :290    applyM (x :: rest) (o.map (fun m => (m.1 + 1, m.2))) = (applyM rest o).map (x :: ·) := by291  cases o <;> rfl292293theorem subFirstGe_eq (u : Nat) : ∀ P : List Nat,294    subFirstGe u P = applyM P (firstIdx (fun x => decide (u ≤ x)) (fun x => x - u) P)295  | [] => rfl296  | x :: rest => by297    rw [firstIdx_cons]298    by_cases h : u ≤ x299    · simp [subFirstGe, h, applyM]300    · simp only [subFirstGe, h, if_false, decide_false, Bool.false_eq_true]301      rw [applyM_shift, subFirstGe_eq u rest]302303theorem subFirstPos_eq : ∀ P : List Nat, subFirstPos P = applyM P (decIdx P)304  | [] => rfl305  | x :: rest => by306    by_cases h : 0 < x307    · simp [subFirstPos, decIdx, h, applyM]308    · simp only [subFirstPos, decIdx, h, if_false]309      rw [applyM_shift, subFirstPos_eq rest]310311/-- The policy step of π_j in index form. -/312def policyIdx (j : Nat) (P : List Nat) : Option (Nat × Nat) :=313  primOr (fun x => decide (2 ^ j ≤ x)) (fun x => x - 2 ^ j) P314315theorem policyIdx_step (j : Nat) (P : List Nat) : applyM P (policyIdx j P) = policyStep j P := by316  unfold policyIdx primOr policyStep317  rw [subFirstGe_eq]318  cases firstIdx (fun x => decide (2 ^ j ≤ x)) (fun x => x - 2 ^ j) P with319  | some m => rfl320  | none => rw [subFirstPos_eq]; rfl321322/-! ## Variable-target selector -/323324/-- Input vector: board on wires below B·N, then the bits of σ (little-endian). -/325def selIn (B N : Nat) (P : List Nat) (σ : Nat) : Nat → Bool := fun j =>326  if j < B * N then boardBits B P j else σ.testBit (j - B * N)327328def sigW (B N q : Nat) : Circ := input (B * N + q)329330/-- σ has its top bit at position k. -/331def topC (B N k : Nat) : Circ :=332  and (sigW B N k :: (List.range (B - 1 - k)).map (fun u => not (sigW B N (k + 1 + u))))333334/-- Heap i cancels σ (σ ≠ 0 and x_i XOR σ < x_i). -/335def cancV (B N i : Nat) : Circ :=336  or ((List.range B).map (fun k => and [topC B N k, input (B * i + (B - 1 - k))]))337338/-- Big-endian bit p of x_i XOR σ. -/339def xbV (B N i p : Nat) : Circ := xor2 (input (B * i + p)) (sigW B N (B - 1 - p))340341def varSel (B N : Nat) : RCirc := genSel B N (cancV B N) (xbV B N)342343section VarSel344variable {B N : Nat} {P : List Nat}345346theorem selIn_board (σ : Nat) {j : Nat} (hj : j < B * N) : selIn B N P σ j = boardBits B P j := by347  simp [selIn, hj]348349theorem selIn_sig (σ q : Nat) : selIn B N P σ (B * N + q) = σ.testBit q := by350  simp only [selIn, if_neg (show ¬ (B * N + q < B * N) by omega), Nat.add_sub_cancel_left]351352theorem heap_lt {i p : Nat} (hi : i < N) (hp : p < B) : B * i + p < B * N := by353  have : B * i + B ≤ B * N := by rw [← Nat.mul_succ]; exact Nat.mul_le_mul_left _ hi354  omega355356theorem cancV_eval (hP : P.length = N) {σ : Nat} (hσ : σ < 2 ^ B) {i : Nat} (hi : i < N) :357    eval (selIn B N P σ) (cancV B N i) = decide (P.getD i 0 ^^^ σ < P.getD i 0) := by358  have e : decide (P.getD i 0 ^^^ σ < P.getD i 0) = decide (σ ≠ 0 ∧ P.getD i 0 ^^^ σ < P.getD i 0) := by359    by_cases h : σ = 0360    · subst h; simp361    · simp [h]362  rw [e]363  apply Bool.eq_iff_iff.mpr364  rw [decide_eq_true_iff, ControllerBits.canc_iff hσ]365  simp only [cancV, topC, sigW, eval_or, eval_and, eval_not, eval_input, List.any_map, List.all_cons,366    List.all_map, List.all_nil, List.any_eq_true, List.all_eq_true, List.mem_range, Function.comp_apply,367    Bool.and_eq_true, Bool.and_true, Bool.not_eq_true', selIn_sig]368  constructor369  · rintro ⟨k, hk, ⟨h1, h2⟩, h3⟩370    refine ⟨k, hk, h1, ?_, h2⟩371    rw [selIn_board σ (heap_lt hi (by omega)), boardBits_heap hP hi (by omega),372      show B - 1 - (B - 1 - k) = k by omega] at h3373    exact h3374  · rintro ⟨k, hk, h1, h2, h3⟩375    refine ⟨k, hk, ⟨h1, h3⟩, ?_⟩376    rw [selIn_board σ (heap_lt hi (by omega)), boardBits_heap hP hi (by omega),377      show B - 1 - (B - 1 - k) = k by omega]378    exact h2379380theorem xbV_eval (hP : P.length = N) (σ : Nat) {i p : Nat} (hi : i < N) (hp : p < B) :381    eval (selIn B N P σ) (xbV B N i p) = (P.getD i 0 ^^^ σ).testBit (B - 1 - p) := by382  simp only [xbV, sigW, eval_xor2, eval_input, selIn_sig, selIn_board σ (heap_lt hi hp),383    boardBits_heap hP hi hp, Nat.testBit_xor]384385/-- VARIABLE-TARGET SELECTOR EXACTNESS: for every σ < 2^B supplied on the σ wires, the386    circuit outputs `attainT σ P` (= `replayMove σ P`). -/387theorem varSel_correct (hP : P.length = N) (hw : Width B P) {σ : Nat} (hσ : σ < 2 ^ B) :388    selReadout (varSel B N) (selIn B N P σ) = attainT σ P := by389  rw [attainT_eq_primOr]390  apply genSel_correct hP hw _ (fun j hj => selIn_board σ hj)391  · intro i hi; exact cancV_eval hP hσ hi392  · intro x hx393    rcases Nat.eq_zero_or_pos x with h | h394    · subst h; simp at hx395    · exact h396  · intro x _ hx; exact Nat.xor_lt_two_pow hx hσ397  · intro i hi p hp _; exact xbV_eval hP σ hi hp398399end VarSel400401/-! ## Multi-head reconstruction and move selection -/402403/-- Input vector: board, then the B rollout outcome bits o 0, …, o (B-1). -/404def obsIn (B N : Nat) (P : List Nat) (o : Nat → Bool) : Nat → Bool := fun j =>405  if j < B * N then boardBits B P j else o (j - B * N)406407/-- σ_j from the outcome wires: σ₀ = o₀, σⱼ = oⱼ ⊕ o₀ (j < B). -/408def recC (B N j : Nat) : Circ :=409  if j < B then (if j = 0 then input (B * N) else xor2 (input (B * N + j)) (input (B * N))) else const false410411def mhSubst (B N : Nat) : Nat → Circ := fun w => if w < B * N then input w else recC B N (w - B * N)412413/-- The multi-head selector: the variable-target selector with σ reconstructed. -/414def mhSel (B N : Nat) : RCirc := substR (mhSubst B N) (varSel B N)415416theorem mh_inputs (B N : Nat) (P : List Nat) (o : Nat → Bool) :417    (fun w => eval (obsIn B N P o) (mhSubst B N w)) = selIn B N P (reconstruct B o) := by418  funext w419  unfold mhSubst selIn420  by_cases hw : w < B * N421  · simp [hw, obsIn]422  · simp only [hw, if_false]423    unfold reconstruct424    rw [testBit_ofBits]425    unfold recC recoverBit426    by_cases hj : w - B * N < B427    · by_cases h0 : w - B * N = 0428      · have hB : 0 < B := by omega429        rw [h0]430        simp [hB, obsIn]431      · simp only [hj, h0, if_true, if_false, eval_xor2, eval_input, decide_true, Bool.true_and]432        simp [obsIn, show ¬ (B * N + (w - B * N) < B * N) by omega, show ¬ (B * N < B * N) by omega]433    · simp [hj]434435/-- MULTI-HEAD SELECTOR: for any outcome vector o the circuit outputs436    `attainT (reconstruct B o) P`; on the true rollout outcomes of a B-bit board it437    outputs `decisionMove P` (legal, zero successor from nonzero positions, halting438    exactly on terminal boards: `Controller.decision_correct`). -/439theorem mhSel_correct {B N : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) (o : Nat → Bool) :440    selReadout (mhSel B N) (obsIn B N P o) = attainT (reconstruct B o) P := by441  unfold mhSel442  rw [selReadout_subst, mh_inputs]443  exact varSel_correct hP hw (ofBits_lt B _)444445theorem mhSel_outcomes {B N : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) :446    selReadout (mhSel B N) (obsIn B N P (outcomes P)) = Controller.decisionMove P := by447  rw [mhSel_correct hP hw, reconstruct_eq hw, attainT_eq_replayMove]448  rfl449450/-! ## Policy-step circuits for π_j -/451452/-- Heap i is eligible for π_j: 2^j ≤ x_i (some bit at position ≥ j is set). -/453def eligC (B j i : Nat) : Circ :=454  or ((List.range (B - j)).map (fun u => input (B * i + (B - 1 - (j + u)))))455456/-- Big-endian bit p of x_i − 2^j (valid when 2^j ≤ x_i). -/457def subbitC (B j i p : Nat) : Circ :=458  if B - 1 - p < j then input (B * i + p)459  else xor2 (input (B * i + p))460    (and ((List.range (B - 1 - p - j)).map (fun m => not (input (B * i + (B - 1 - (j + m)))))))461462def polSel (B N j : Nat) : RCirc := genSel B N (eligC B j) (subbitC B j)463464theorem pow_le_iff_bit {x j B : Nat} (hx : x < 2 ^ B) :465    2 ^ j ≤ x ↔ ∃ u < B - j, x.testBit (j + u) = true := by466  constructor467  · intro h468    have hx0 : x ≠ 0 := by have := Nat.two_pow_pos j; omega469    have h1 : j ≤ x.log2 := by470      rcases Nat.lt_or_ge x.log2 j with h' | h'471      · exfalso472        have := Nat.lt_log2_self (n := x)473        have : x < 2 ^ j := Nat.lt_of_lt_of_le this (Nat.pow_le_pow_right (by decide) (by omega))474        omega475      · exact h'476    have h2 : x.log2 < B := by477      rcases Nat.lt_or_ge x.log2 B with h' | h'478      · exact h'479      · exfalso480        have := Nat.log2_self_le hx0481        have : 2 ^ B ≤ x := Nat.le_trans (Nat.pow_le_pow_right (by decide) h') this482        omega483    refine ⟨x.log2 - j, by omega, ?_⟩484    rw [show j + (x.log2 - j) = x.log2 by omega]485    cases hb : x.testBit x.log2 with486    | true => rfl487    | false =>488      exfalso489      have : x < 2 ^ x.log2 := by490        apply Nat.lt_pow_two_of_testBit491        intro i hi492        by_cases hik : i = x.log2493        · subst hik; exact hb494        · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self495            (Nat.pow_le_pow_right (by decide) (by omega)))496      exact absurd (Nat.log2_self_le hx0) (Nat.not_le.mpr this)497  · rintro ⟨u, _, hu⟩498    exact Nat.le_trans (Nat.pow_le_pow_right (by decide) (by omega)) (Nat.ge_two_pow_of_testBit hu)499500theorem sub_pow_testBit {x j : Nat} (hx : 2 ^ j ≤ x) (k : Nat) :501    (x - 2 ^ j).testBit k =502      if k < j then x.testBit k else xor (x.testBit k) (decide (∀ m < k - j, x.testBit (j + m) = false)) := by503  have hq : 0 < x / 2 ^ j := Nat.div_pos hx (Nat.two_pow_pos j)504  have hdecomp : x - 2 ^ j = 2 ^ j * (x / 2 ^ j - 1) + x % 2 ^ j := by505    have h1 := Nat.div_add_mod x (2 ^ j)506    have h2 : 2 ^ j * (x / 2 ^ j - 1) + 2 ^ j = 2 ^ j * (x / 2 ^ j) := by507      rw [Nat.mul_sub_one]; have := Nat.le_mul_of_pos_right (2 ^ j) hq; omega508    omega509  rw [hdecomp, Nat.testBit_two_pow_mul_add _ (Nat.mod_lt _ (Nat.two_pow_pos j))]510  by_cases hk : k < j511  · simp only [hk, if_true]512    rw [Nat.testBit_mod_two_pow]; simp [hk]513  · simp only [hk, if_false]514    rw [testBit_pred _ hq]515    simp only [Nat.testBit_div_two_pow]516    rw [show k - j + j = k by omega]517    congr 1518    apply Bool.eq_iff_iff.mpr519    simp only [decide_eq_true_iff]520    constructor521    · intro h m hm; rw [Nat.add_comm]; exact h m hm522    · intro h m hm; rw [Nat.add_comm]; exact h m hm523524theorem eligC_eval {B N j : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) {i : Nat} (hi : i < N) :525    eval (boardBits B P) (eligC B j i) = decide (2 ^ j ≤ P.getD i 0) := by526  apply Bool.eq_iff_iff.mpr527  rw [decide_eq_true_iff, pow_le_iff_bit (getD_lt_of_width hP hw hi)]528  simp only [eligC, eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp_apply,529    eval_input]530  constructor531  · rintro ⟨u, hu, h⟩532    rw [boardBits_heap hP hi (by omega), show B - 1 - (B - 1 - (j + u)) = j + u by omega] at h533    exact ⟨u, hu, h⟩534  · rintro ⟨u, hu, h⟩535    refine ⟨u, hu, ?_⟩536    rw [boardBits_heap hP hi (by omega), show B - 1 - (B - 1 - (j + u)) = j + u by omega]537    exact h538539theorem subbitC_eval {B N j : Nat} {P : List Nat} (hP : P.length = N) {i p : Nat} (hi : i < N) (hp : p < B)540    (hx : 2 ^ j ≤ P.getD i 0) :541    eval (boardBits B P) (subbitC B j i p) = (P.getD i 0 - 2 ^ j).testBit (B - 1 - p) := by542  rw [sub_pow_testBit hx]543  unfold subbitC544  by_cases hk : B - 1 - p < j545  · simp only [hk, if_true, eval_input, boardBits_heap hP hi hp]546  · simp only [hk, if_false, eval_xor2, eval_input, boardBits_heap hP hi hp]547    congr 1548    apply Bool.eq_iff_iff.mpr549    simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp_apply, eval_not,550      eval_input, Bool.not_eq_true', decide_eq_true_iff]551    constructor552    · intro h m hm553      have := h m hm554      rwa [boardBits_heap hP hi (by omega), show B - 1 - (B - 1 - (j + m)) = j + m by omega] at this555    · intro h m hm556      rw [boardBits_heap hP hi (by omega), show B - 1 - (B - 1 - (j + m)) = j + m by omega]557      exact h m hm558559/-- POLICY-STEP CIRCUIT EXACTNESS: the circuit outputs the π_j move (index form), and560    applying it gives exactly `policyStep j P`. -/561theorem polSel_correct {B N j : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) :562    selReadout (polSel B N j) (boardBits B P) = policyIdx j P ∧563      applyM P (selReadout (polSel B N j) (boardBits B P)) = policyStep j P := by564  have h : selReadout (polSel B N j) (boardBits B P) = policyIdx j P := by565    apply genSel_correct hP hw _ (fun _ _ => rfl)566    · intro i hi; exact eligC_eval hP hw hi567    · intro x hx; have := Nat.two_pow_pos j; simp at hx; omega568    · intro x _ hx; exact Nat.lt_of_le_of_lt (Nat.sub_le _ _) hx569    · intro i hi p hp hx; exact subbitC_eval hP hi hp (by simpa using hx)570  exact ⟨h, by rw [h, policyIdx_step]⟩571572/-! ## Resources: constant depth, polynomial size -/573574/-- All formulas of a readout: depth ≤ D, size ≤ S, inputs below M. -/575def SelBound (R : RCirc) (N B D S M : Nat) : Prop :=576  R.sel.length = N ∧ R.val.length = B ∧577    ∀ c ∈ R.valid :: (R.sel ++ R.val), depth c ≤ D ∧ size c ≤ S ∧ maxInput c ≤ M578579section Res580variable {U : Nat}581582theorem lift1 (hU : 1 ≤ U) {x a k a' k' : Nat} (h : x ≤ a * U ^ k) (ha : a ≤ a') (hk : k ≤ k') :583    x ≤ a' * U ^ k' :=584  Nat.le_trans h (Nat.mul_le_mul ha (Nat.pow_le_pow_right hU hk))585586theorem sz_firstC (hU : 1 ≤ U) {cs : Nat → Circ} {i a k : Nat} (hi : i + 1 ≤ U)587    (h : ∀ i' ≤ i, size (cs i') ≤ a * U ^ k) : size (firstC cs i) ≤ (a + 2) * U ^ (k + 1) := by588  unfold firstC589  apply size_and_le hU (by simp; omega)590  intro c hc591  simp only [List.mem_cons, List.mem_map, List.mem_range] at hc592  rcases hc with rfl | ⟨i', hi', rfl⟩593  · exact lift1 hU (h i (Nat.le_refl _)) (by omega) (Nat.le_refl _)594  · exact size_not_le hU (h i' (by omega))595596theorem dp_firstC {cs : Nat → Circ} {i d : Nat} (h : ∀ i' ≤ i, depth (cs i') ≤ d) :597    depth (firstC cs i) ≤ d + 2 := by598  unfold firstC599  apply depth_and_le600  intro c hc601  simp only [List.mem_cons, List.mem_map, List.mem_range] at hc602  rcases hc with rfl | ⟨i', hi', rfl⟩603  · have := h i (Nat.le_refl _); omega604  · simp only [depth_not]; have := h i' (by omega); omega605606theorem mx_firstC {cs : Nat → Circ} {i M : Nat} (h : ∀ i' ≤ i, maxInput (cs i') ≤ M) :607    maxInput (firstC cs i) ≤ M := by608  unfold firstC609  apply ControllerBits.maxInput_and_le610  intro c hc611  simp only [List.mem_cons, List.mem_map, List.mem_range] at hc612  rcases hc with rfl | ⟨i', hi', rfl⟩613  · exact h i (Nat.le_refl _)614  · simp only [maxInput_not]; exact h i' (by omega)615616theorem sz_orFirst (hU : 2 ≤ U) {N : Nat} {cs bs : Nat → Circ} {a k : Nat} (hN : N ≤ U)617    (hcs : ∀ i < N, size (cs i) ≤ a * U ^ k) (hbs : ∀ i < N, size (bs i) ≤ a * U ^ k) :618    size (orFirst N cs bs) ≤ (a + 4) * U ^ (k + 3) := by619  have hU1 : 1 ≤ U := by omega620  unfold orFirst621  apply size_or_le hU1 (by simp; omega)622  intro c hc623  obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc624  have hi' := List.mem_range.mp hi625  apply size_and_le hU1 (by simp; omega)626  intro c hc627  simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc628  rcases hc with rfl | rfl629  · exact sz_firstC hU1 (by omega) (fun i' hi'' => hcs i' (by omega))630  · exact lift1 hU1 (hbs i hi') (by omega) (by omega)631632theorem dp_orFirst {N : Nat} {cs bs : Nat → Circ} {d : Nat} (hcs : ∀ i < N, depth (cs i) ≤ d)633    (hbs : ∀ i < N, depth (bs i) ≤ d + 2) : depth (orFirst N cs bs) ≤ d + 4 := by634  unfold orFirst635  apply depth_or_le636  intro c hc637  obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc638  have hi' := List.mem_range.mp hi639  apply depth_and_le640  intro c hc641  simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc642  rcases hc with rfl | rfl643  · have := dp_firstC (cs := cs) (i := i) (d := d) (fun i' hi'' => hcs i' (by omega)); omega644  · have := hbs i hi'; omega645646theorem mx_orFirst {N M : Nat} {cs bs : Nat → Circ} (hcs : ∀ i < N, maxInput (cs i) ≤ M)647    (hbs : ∀ i < N, maxInput (bs i) ≤ M) : maxInput (orFirst N cs bs) ≤ M := by648  unfold orFirst649  apply ControllerBits.maxInput_or_le650  intro c hc651  obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc652  have hi' := List.mem_range.mp hi653  apply ControllerBits.maxInput_and_le654  intro c hc655  simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc656  rcases hc with rfl | rfl657  · exact mx_firstC (fun i' hi'' => hcs i' (by omega))658  · exact hbs i hi'659660end Res661662section GenRes663variable {B N : Nat}664665theorem nzC_res (hU : 2 ≤ U) (hB : B ≤ U) (i : Nat) :666    size (AttainCircuit.nzC B i) ≤ 2 * U ^ 1 ∧ depth (AttainCircuit.nzC B i) ≤ 1 := by667  have hU1 : 1 ≤ U := by omega668  refine ⟨?_, ?_⟩669  · unfold AttainCircuit.nzC670    apply size_or_le hU1 (by simp; omega)671    intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; simp672  · unfold AttainCircuit.nzC673    apply depth_or_le; intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; simp674675theorem decbitC_res (hU : 2 ≤ U) (hB : B ≤ U) (i p : Nat) :676    size (decbitC B i p) ≤ 6 * U ^ 3 ∧ depth (decbitC B i p) ≤ 5 := by677  have hU1 : 1 ≤ U := by omega678  have hl1 : size (lowZeroC B i p) ≤ 3 * U ^ 1 := by679    unfold lowZeroC680    apply size_and_le hU1 (by simp; omega)681    intro c hc; obtain ⟨r, _, rfl⟩ := List.mem_map.mp hc; simp682  have hl2 : depth (lowZeroC B i p) ≤ 2 := by683    unfold lowZeroC684    apply depth_and_le; intro c hc; obtain ⟨r, _, rfl⟩ := List.mem_map.mp hc; simp685  unfold decbitC xor2686  generalize lowZeroC B i p = L at hl1 hl2687  refine ⟨?_, ?_⟩688  · apply size_or_le hU1 (by simp; omega)689    intro c hc690    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc691    rcases hc with rfl | rfl692    · apply size_and_le hU1 (by simp; omega)693      intro c hc694      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc695      rcases hc with rfl | rfl696      · exact lift1 hU1 (show size (input (B * i + p)) ≤ 1 * U ^ 0 by simp) (by omega) (by omega)697      · exact size_not_le hU1 hl1698    · apply size_and_le hU1 (by simp; omega)699      intro c hc700      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc701      rcases hc with rfl | rfl702      · exact lift1 hU1 (show size (not (input (B * i + p))) ≤ 2 * U ^ 0 by simp) (by omega) (by omega)703      · exact lift1 hU1 hl1 (by omega) (Nat.le_refl _)704  · simp only [depth_or, depth_and, depth_not, depth_input, List.map_cons, List.map_nil, listMax,705      List.foldr_cons, List.foldr_nil]706    omega707708/-- GENERIC SELECTOR RESOURCES: depth ≤ d + 9, size ≤ 12·U^8 with709    U = (N+2)(B+2)(s+2), inputs below M. -/710theorem genSel_bound (prim : Nat → Circ) (pv : Nat → Nat → Circ) (d s M : Nat)711    (hprim : ∀ i < N, depth (prim i) ≤ d ∧ size (prim i) ≤ s ∧ maxInput (prim i) ≤ M)712    (hpv : ∀ i < N, ∀ p < B, depth (pv i p) ≤ d ∧ size (pv i p) ≤ s ∧ maxInput (pv i p) ≤ M)713    (hM : B * N ≤ M) :714    SelBound (genSel B N prim pv) N B (d + 9) (12 * ((N + 2) * (B + 2) * (s + 2)) ^ 8) M := by715  generalize hUdef : (N + 2) * (B + 2) * (s + 2) = U716  have hNU : N + 2 ≤ U := by717    rw [← hUdef]718    have := Nat.le_mul_of_pos_right (N + 2) (show 0 < (B + 2) * (s + 2) from Nat.mul_pos (by omega) (by omega))719    rw [Nat.mul_assoc]; exact this720  have hBU : B + 2 ≤ U := by721    rw [← hUdef]722    have := Nat.le_mul_of_pos_left (B + 2) (show 0 < N + 2 by omega)723    have h2 := Nat.le_mul_of_pos_right ((N + 2) * (B + 2)) (show 0 < s + 2 by omega)724    exact Nat.le_trans this h2725  have hsU : s + 2 ≤ U := by726    rw [← hUdef]727    exact Nat.le_mul_of_pos_left (s + 2) (show 0 < (N + 2) * (B + 2) from Nat.mul_pos (by omega) (by omega))728  have hU2 : 2 ≤ U := by omega729  have hU1 : 1 ≤ U := by omega730  have hps : ∀ i < N, size (prim i) ≤ 1 * U ^ 1 := fun i hi => by731    have := (hprim i hi).2.1; simp; omega732  have hvs : ∀ i < N, ∀ p < B, size (pv i p) ≤ 1 * U ^ 1 := fun i hi p hp => by733    have := (hpv i hi p hp).2.1; simp; omega734  -- the shared OR of primary tests735  have hA_s : size (anyC' N prim) ≤ 2 * U ^ 2 := by736    unfold anyC'737    apply size_or_le hU1 (by simp; omega)738    intro c hc; obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact hps i (List.mem_range.mp hi)739  have hA_d : depth (anyC' N prim) ≤ d + 1 := by740    unfold anyC'741    apply depth_or_le742    intro c hc; obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact (hprim i (List.mem_range.mp hi)).1743  have hA_m : maxInput (anyC' N prim) ≤ M := by744    unfold anyC'745    apply ControllerBits.maxInput_or_le746    intro c hc; obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact (hprim i (List.mem_range.mp hi)).2.2747  refine ⟨by simp [genSel], by simp [genSel], ?_⟩748  intro c hc749  simp only [genSel, List.mem_cons, List.mem_append, List.mem_map, List.mem_range] at hc750  rcases hc with rfl | ⟨i, hi, rfl⟩ | ⟨p, hp, rfl⟩751  · -- validity752    refine ⟨?_, ?_, ?_⟩753    · unfold validA; apply depth_or_le754      intro c hc; obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc755      have := (nzC_res hU2 (by omega) (B := B) i).2; omega756    · unfold validA757      have h1 := size_or_le (a := 2) (k := 1) hU1 (cs := (List.range N).map (AttainCircuit.nzC B))758        (by simp; omega) (fun c hc => by759          obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (nzC_res hU2 (by omega) i).1)760      have h2 : (2 + 1) * U ^ (1 + 1) ≤ 12 * U ^ 8 :=761        Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hU1 (by omega))762      omega763    · unfold validA764      apply ControllerBits.maxInput_or_le765      intro c hc; obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc766      exact Nat.le_trans (max_nzC (List.mem_range.mp hi)) hM767  · -- selection formula i768    refine ⟨?_, ?_, ?_⟩769    · apply depth_or_le770      intro c hc771      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc772      rcases hc with rfl | rfl773      · have := (hprim i hi).1; omega774      · apply depth_and_le775        intro c hc776        simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc777        rcases hc with rfl | rfl778        · simp only [depth_not]; omega779        · have := (nzC_res hU2 (by omega) (B := B) i).2; omega780    · have h1 : size (or [prim i, and [not (anyC' N prim), AttainCircuit.nzC B i]]) ≤ 5 * U ^ 4 := by781        apply size_or_le hU1 (by simp; omega)782        intro c hc783        simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc784        rcases hc with rfl | rfl785        · exact lift1 hU1 (hps i hi) (by omega) (by omega)786        · apply size_and_le hU1 (by simp; omega)787          intro c hc788          simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc789          rcases hc with rfl | rfl790          · exact lift1 hU1 (size_not_le hU1 hA_s) (by omega) (by omega)791          · exact lift1 hU1 (nzC_res hU2 (by omega) i).1 (by omega) (by omega)792      exact Nat.le_trans h1 (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hU1 (by omega)))793    · apply ControllerBits.maxInput_or_le794      intro c hc795      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc796      rcases hc with rfl | rfl797      · exact (hprim i hi).2.2798      · apply ControllerBits.maxInput_and_le799        intro c hc800        simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc801        rcases hc with rfl | rfl802        · simp only [maxInput_not]; exact hA_m803        · exact Nat.le_trans (max_nzC hi) hM804  · -- value bit p805    have hO1s : size (orFirst N prim (fun i => pv i p)) ≤ 5 * U ^ 4 :=806      sz_orFirst hU2 (by omega) hps (fun i hi => hvs i hi p hp)807    have hO2s : size (orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p)) ≤ 10 * U ^ 6 :=808      sz_orFirst hU2 (by omega) (fun i _ => lift1 hU1 (nzC_res hU2 (by omega) i).1 (by omega) (by omega))809        (fun i _ => (decbitC_res hU2 (by omega) i p).1)810    have hO1d : depth (orFirst N prim (fun i => pv i p)) ≤ d + 4 :=811      dp_orFirst (fun i hi => (hprim i hi).1) (fun i hi => by have := (hpv i hi p hp).1; omega)812    have hO2d : depth (orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p)) ≤ 3 + 4 :=813      dp_orFirst (fun i _ => by have := (nzC_res hU2 (by omega) (B := B) i).2; omega)814        (fun i _ => (decbitC_res hU2 (by omega) i p).2)815    have hO1m : maxInput (orFirst N prim (fun i => pv i p)) ≤ M :=816      mx_orFirst (fun i hi => (hprim i hi).2.2) (fun i hi => (hpv i hi p hp).2.2)817    have hO2m : maxInput (orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p)) ≤ M :=818      mx_orFirst (fun i hi => Nat.le_trans (max_nzC hi) hM)819        (fun i hi => Nat.le_trans (max_decbitC hi hp) hM)820    generalize orFirst N prim (fun i => pv i p) = O1 at hO1s hO1d hO1m821    generalize orFirst N (AttainCircuit.nzC B) (fun i => decbitC B i p) = O2 at hO2s hO2d hO2m822    generalize anyC' N prim = A at hA_s hA_d hA_m823    refine ⟨?_, ?_, ?_⟩824    · simp only [depth_or, depth_and, depth_not, List.map_cons, List.map_nil, listMax,825        List.foldr_cons, List.foldr_nil]826      omega827    · apply size_or_le hU1 (by simp; omega)828      intro c hc829      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc830      rcases hc with rfl | rfl831      · apply size_and_le hU1 (by simp; omega)832        intro c hc833        simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc834        rcases hc with rfl | rfl835        · exact lift1 hU1 hA_s (by omega) (by omega)836        · exact lift1 hU1 hO1s (by omega) (by omega)837      · apply size_and_le hU1 (by simp; omega)838        intro c hc839        simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc840        rcases hc with rfl | rfl841        · exact lift1 hU1 (size_not_le hU1 hA_s) (by omega) (by omega)842        · exact hO2s843    · simp only [maxInput_or, maxInput_and, maxInput_not, List.map_cons, List.map_nil, listMax,844        List.foldr_cons, List.foldr_nil]845      omega846847end GenRes848849theorem substR_bound {R : RCirc} {N B D S M D' S' M' : Nat} (τ : Nat → Circ) (hR : SelBound R N B D S M)850    (hτd : ∀ w, depth (τ w) ≤ D') (hτs : ∀ w, size (τ w) ≤ S') (hτm : ∀ w, maxInput (τ w) ≤ M') :851    SelBound (substR τ R) N B (D + D') (S * (S' + 1)) M' := by852  obtain ⟨h1, h2, h3⟩ := hR853  refine ⟨by simp [substR, h1], by simp [substR, h2], ?_⟩854  intro c hc855  have : ∃ c', c' ∈ R.valid :: (R.sel ++ R.val) ∧ c = subst τ c' := by856    simp only [substR, List.mem_cons, List.mem_append, List.mem_map] at hc857    rcases hc with rfl | ⟨c', hc', rfl⟩ | ⟨c', hc', rfl⟩858    · exact ⟨R.valid, by simp, rfl⟩859    · exact ⟨c', by simp [hc'], rfl⟩860    · exact ⟨c', by simp [hc'], rfl⟩861  obtain ⟨c', hc', rfl⟩ := this862  obtain ⟨hd, hs, _⟩ := h3 c' hc'863  refine ⟨Nat.le_trans (depth_subst_le τ D' hτd c') (by omega),864    Nat.le_trans (size_subst_le τ S' hτs c') (Nat.mul_le_mul_right _ hs), maxInput_subst_le τ M' hτm c'⟩865866section InstRes867variable {B N : Nat}868869theorem cancV_res {i : Nat} (hi : i < N) :870    depth (cancV B N i) ≤ 4 ∧ size (cancV B N i) ≤ B * (2 * B + 3) + 9 ∧ maxInput (cancV B N i) ≤ B * N + B := by871  refine ⟨?_, ?_, ?_⟩872  · unfold cancV; apply depth_or_le; intro c hc873    obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc874    apply depth_and_le; intro c hc875    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc876    rcases hc with rfl | rfl877    · unfold topC; apply depth_and_le; intro c hc878      simp only [List.mem_cons, List.mem_map, List.mem_range] at hc879      rcases hc with rfl | ⟨u, _, rfl⟩ <;> simp [sigW]880    · simp881  · unfold cancV882    have := ControllerBits.size_or_le' (S := 2 * B + 3) (cs := (List.range B).map (fun k => and [topC B N k, input (B * i + (B - 1 - k))])) (by883      intro c hc884      obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc885      have hk' := List.mem_range.mp hk886      have ht := ControllerBits.size_and_le' (S := 2) (cs := sigW B N k :: (List.range (B - 1 - k)).map887        (fun u => not (sigW B N (k + 1 + u)))) (by888          intro c hc889          simp only [List.mem_cons, List.mem_map, List.mem_range] at hc890          rcases hc with rfl | ⟨u, _, rfl⟩ <;> simp [sigW])891      simp only [List.length_cons, List.length_map, List.length_range] at ht892      have ht' : size (topC B N k) ≤ (B - 1 - k + 1) * 2 + 1 := ht893      simp only [size_and, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, size_input]894      have : (B - 1 - k + 1) * 2 + 1 + 2 ≤ 2 * B + 3 := by omega895      omega)896    simp only [List.length_map, List.length_range] at this897    omega898  · unfold cancV; apply ControllerBits.maxInput_or_le; intro c hc899    obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc900    have hk' := List.mem_range.mp hk901    apply ControllerBits.maxInput_and_le; intro c hc902    simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc903    rcases hc with rfl | rfl904    · unfold topC; apply ControllerBits.maxInput_and_le; intro c hc905      simp only [List.mem_cons, List.mem_map, List.mem_range] at hc906      rcases hc with rfl | ⟨u, hu, rfl⟩907      · simp [sigW]; omega908      · simp [sigW]; omega909    · simp; have := heap_lt (B := B) (N := N) hi (show B - 1 - k < B by omega); omega910911theorem xbV_res {i p : Nat} (hi : i < N) (hp : p < B) :912    depth (xbV B N i p) ≤ 3 ∧ size (xbV B N i p) ≤ 9 ∧ maxInput (xbV B N i p) ≤ B * N + B := by913  have := heap_lt (B := B) (N := N) hi hp914  refine ⟨?_, ?_, ?_⟩ <;> simp [xbV, xor2, sigW, listMax] <;> omega915916/-- The variable-target selector: depth ≤ 13, size ≤ 12·U^8 with917    U = (N+2)(B+2)(2B²+3B+11), inputs below B·N + B. -/918theorem varSel_bound :919    SelBound (varSel B N) N B (4 + 9) (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8) (B * N + B) :=920  genSel_bound (cancV B N) (xbV B N) 4 (B * (2 * B + 3) + 9) (B * N + B)921    (fun i hi => cancV_res hi)922    (fun i hi p hp => by obtain ⟨a, b, c⟩ := xbV_res (B := B) (N := N) hi hp; exact ⟨by omega, by omega, c⟩)923    (by omega)924925theorem recC_res (j : Nat) : depth (recC B N j) ≤ 3 ∧ size (recC B N j) ≤ 9 ∧ maxInput (recC B N j) ≤ B * N + B := by926  unfold recC927  by_cases hj : j < B928  · by_cases h0 : j = 0929    · subst h0; simp [hj]; omega930    · simp [hj, h0, xor2, listMax]; omega931  · simp [hj]932933/-- The multi-head selector: depth ≤ 16, size ≤ 120·U^8 (U as for `varSel`), reading the934    board and the B outcome wires only. -/935theorem mhSel_bound :936    SelBound (mhSel B N) N B (4 + 9 + 3)937      (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (9 + 1)) (B * N + B) := by938  apply substR_bound (mhSubst B N) varSel_bound939  · intro w; unfold mhSubst; split940    · simp941    · exact (recC_res _).1942  · intro w; unfold mhSubst; split943    · simp944    · exact (recC_res _).2.1945  · intro w; unfold mhSubst; split946    · simp; omega947    · exact (recC_res _).2.2948949theorem eligC_res (j : Nat) {i : Nat} (hi : i < N) :950    depth (eligC B j i) ≤ 5 ∧ size (eligC B j i) ≤ 4 * B + 9 ∧ maxInput (eligC B j i) ≤ B * N := by951  refine ⟨?_, ?_, ?_⟩952  · have : depth (eligC B j i) ≤ 1 := by953      unfold eligC; apply depth_or_le; intro c hc; obtain ⟨u, _, rfl⟩ := List.mem_map.mp hc; simp954    omega955  · unfold eligC956    have := ControllerBits.size_or_le' (S := 1) (cs := (List.range (B - j)).map (fun u => input (B * i + (B - 1 - (j + u)))))957      (by intro c hc; obtain ⟨u, _, rfl⟩ := List.mem_map.mp hc; simp)958    simp only [List.length_map, List.length_range] at this959    omega960  · unfold eligC; apply ControllerBits.maxInput_or_le; intro c hc961    obtain ⟨u, hu, rfl⟩ := List.mem_map.mp hc962    have := List.mem_range.mp hu963    have := heap_lt (B := B) (N := N) hi (show B - 1 - (j + u) < B by omega)964    simp; omega965966theorem subbitC_res (j : Nat) {i p : Nat} (hi : i < N) (hp : p < B) :967    depth (subbitC B j i p) ≤ 5 ∧ size (subbitC B j i p) ≤ 4 * B + 9 ∧ maxInput (subbitC B j i p) ≤ B * N := by968  have hip := heap_lt (B := B) (N := N) hi hp969  unfold subbitC970  by_cases hk : B - 1 - p < j971  · simp only [hk, if_true]; simp; omega972  · simp only [hk, if_false]973    have hs := ControllerBits.size_and_le' (S := 2) (cs := (List.range (B - 1 - p - j)).map974      (fun m => not (input (B * i + (B - 1 - (j + m)))))) (by975        intro c hc; obtain ⟨m, _, rfl⟩ := List.mem_map.mp hc; simp)976    have hd : depth (and ((List.range (B - 1 - p - j)).map977        (fun m => not (input (B * i + (B - 1 - (j + m))))))) ≤ 2 := by978      apply depth_and_le; intro c hc; obtain ⟨m, _, rfl⟩ := List.mem_map.mp hc; simp979    have hm : maxInput (and ((List.range (B - 1 - p - j)).map980        (fun m => not (input (B * i + (B - 1 - (j + m))))))) ≤ B * N := by981      apply ControllerBits.maxInput_and_le; intro c hc982      obtain ⟨m, hm, rfl⟩ := List.mem_map.mp hc983      have := List.mem_range.mp hm984      have := heap_lt (B := B) (N := N) hi (show B - 1 - (j + m) < B by omega)985      simp; omega986    simp only [List.length_map, List.length_range] at hs987    generalize and ((List.range (B - 1 - p - j)).map (fun m => not (input (B * i + (B - 1 - (j + m)))))) = A988      at hs hd hm989    unfold xor2990    refine ⟨?_, ?_, ?_⟩991    · simp only [depth_or, depth_and, depth_not, depth_input, List.map_cons, List.map_nil, listMax,992        List.foldr_cons, List.foldr_nil]; omega993    · simp only [size_or, size_and, size_not, size_input, List.map_cons, List.map_nil, List.sum_cons,994        List.sum_nil]; omega995    · simp only [maxInput_or, maxInput_and, maxInput_not, maxInput_input, List.map_cons, List.map_nil,996        listMax, List.foldr_cons, List.foldr_nil]; omega997998/-- The π_j policy-step circuit: depth ≤ 14, size ≤ 12·U^8 with U = (N+2)(B+2)(4B+11),999    reading only the B·N board wires. -/1000theorem polSel_bound (j : Nat) :1001    SelBound (polSel B N j) N B (5 + 9) (12 * ((N + 2) * (B + 2) * (4 * B + 9 + 2)) ^ 8) (B * N) :=1002  genSel_bound (eligC B j) (subbitC B j) 5 (4 * B + 9) (B * N)1003    (fun i hi => eligC_res j hi) (fun i hi p hp => subbitC_res j hi hp) (Nat.le_refl _)10041005end InstRes100610071008/-! ## Axiom audit -/10091010#print axioms readoutOf_eq1011#print axioms selReadout_subst1012#print axioms orFirst_eval1013#print axioms firstTrue_isSome1014#print axioms max_nzC1015#print axioms max_decbitC1016#print axioms decbit_eval1017#print axioms getD_lt_of_width1018#print axioms map_getD_eq1019#print axioms firstTrue_map_getD1020#print axioms genSel_correct1021#print axioms firstIdx_cons1022#print axioms cancelIdx_eq_firstIdx1023#print axioms attainT_eq_primOr1024#print axioms cancelIdx_zero1025#print axioms attainT_eq_replayMove1026#print axioms applyM_shift1027#print axioms subFirstGe_eq1028#print axioms subFirstPos_eq1029#print axioms policyIdx_step1030#print axioms selIn_board1031#print axioms selIn_sig1032#print axioms heap_lt1033#print axioms cancV_eval1034#print axioms xbV_eval1035#print axioms varSel_correct1036#print axioms mh_inputs1037#print axioms mhSel_correct1038#print axioms mhSel_outcomes1039#print axioms pow_le_iff_bit1040#print axioms sub_pow_testBit1041#print axioms eligC_eval1042#print axioms subbitC_eval1043#print axioms polSel_correct1044#print axioms lift11045#print axioms sz_firstC1046#print axioms dp_firstC1047#print axioms mx_firstC1048#print axioms sz_orFirst1049#print axioms dp_orFirst1050#print axioms mx_orFirst1051#print axioms nzC_res1052#print axioms decbitC_res1053#print axioms genSel_bound1054#print axioms substR_bound1055#print axioms cancV_res1056#print axioms xbV_res1057#print axioms varSel_bound1058#print axioms recC_res1059#print axioms mhSel_bound1060#print axioms eligC_res1061#print axioms subbitC_res1062#print axioms polSel_bound1063end SelectCircuit1064end NimAudit