RolloutExec

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 Barrier23/- Phase 6, Priority 2: a finite-register rollout executor.  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   The phase-5 loop `WholeGame.rollMoves` is an exact semantic specification, but it7   uses Nat fuel P.sum + 1 and reads the low bit of an unbounded move count.  Here the8   rollout is executed by a REGISTER MACHINE with B·N + 2 state bits:9     board (N heaps × B bits, the boardBits layout), par (one outcome bit), halt (one bit),10   and one SHALLOW STEP CIRCUIT whose extra inputs are a reset bit and an external board11   (loaded on reset).  On each clock step with halt = 0 the circuit evaluates the12   compiled policy selector polBin (the actual phase-5 formulas) on the board bits;13   if it returns a legal binary move (valid ∧ index < N), the addressed heap is replaced14   by the value bits (index comparison by the equality decoder, multiplexed write) and15   par toggles; otherwise halt is set.  With halt = 1 the registers are unchanged.  On16   reset the board is loaded and par, halt are cleared, from ANY register contents.1718   The scheduler is the loop "while halt = 0, clock the step circuit": it reads one bit19   and keeps no counter.  The theorems show that it stops after exactly L + 1 policy20   evaluations (L simulated moves plus the terminal test), that the fixed bound21   N(2^B − 1) + 1 (a function of B and N only) never runs out, and that par is then the22   rollout outcome.  No P.sum oracle and no unbounded arithmetic gate is used: Lean's23   loop fuel is the fixed clock bound and is never exhausted.2425   The step circuit is also compiled to a W = 1 threshold network.  B such executions26   feed the compiled multi-head readout network; the result equals decisionMove and wins27   against every legal opponent.  Per step the work is one evaluation of a depth-≤2828   formula list (≤ 58 network layers, step_net); the number of sequential steps is29   Σ_j (L_j + 1) ≤ B (N(2^B − 1) + 1), which is NOT constant: total sequential depth30   grows with the board (unbounded_steps). -/3132namespace NimAudit33namespace RolloutExec3435open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit36  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame37  Family Barrier3839/-! ## The semantic register machine -/4041/-- Registers of the rollout machine. -/42structure RS where43  board : List Nat44  par : Bool45  halted : Bool4647/-- One clock step, driven by a selector in index form (pol = policyIdx j for π_j). -/48def rsStep (pol : List Nat → Option (Nat × Nat)) (s : RS) : RS :=49  if s.halted then s else50    match pol s.board with51    | none => ⟨s.board, s.par, true⟩52    | some m => ⟨s.board.set m.1 m.2, !s.par, false⟩5354/-- The scheduler: while halt = 0, clock the step; count the clocked steps (each step55    is one policy evaluation).  The Nat argument is Lean's termination fuel. -/56def untilHalt (pol : List Nat → Option (Nat × Nat)) : Nat → RS → RS × Nat57  | 0, s => (s, 0)58  | f + 1, s => if s.halted then (s, 0) else59      ((untilHalt pol f (rsStep pol s)).1, (untilHalt pol f (rsStep pol s)).2 + 1)6061theorem untilHalt_halted (pol : List Nat → Option (Nat × Nat)) (s : RS) (hs : s.halted = true) :62    ∀ f, untilHalt pol f s = (s, 0)63  | 0 => rfl64  | f + 1 => by simp [untilHalt, hs]6566theorem rolloutWinner_none' {j : Nat} {p : List Nat} (h : policyStep j p = none) : rolloutWinner j p = false := by67  rw [rolloutWinner]; split <;> simp_all6869theorem rolloutWinner_some' {j : Nat} {p q : List Nat} (h : policyStep j p = some q) :70    rolloutWinner j p = !rolloutWinner j q := by71  rw [rolloutWinner]; split <;> simp_all7273/-- SEMANTIC EXECUTION: from (P, b, halt = 0), with fuel at least L + 1 (L = number of74    simulated moves), the scheduler stops with halt = 1, par = b XOR outcome, after75    exactly L + 1 clocked steps. -/76theorem untilHalt_spec (j : Nat) : ∀ (f : Nat) (P : List Nat) (b : Bool), rolloutMoves j P + 1 ≤ f →77    (untilHalt (policyIdx j) f ⟨P, b, false⟩).1.par = xor b (rolloutWinner j P) ∧78    (untilHalt (policyIdx j) f ⟨P, b, false⟩).1.halted = true ∧79    (untilHalt (policyIdx j) f ⟨P, b, false⟩).2 = rolloutMoves j P + 180  | 0, P, b, h => by omega81  | f + 1, P, b, h => by82    simp only [untilHalt, Bool.false_eq_true, if_false]83    cases hp : policyIdx j P with84    | none =>85      have hs : policyStep j P = none := by rw [← policyIdx_step, hp]; rfl86      have e : rsStep (policyIdx j) ⟨P, b, false⟩ = ⟨P, b, true⟩ := by simp [rsStep, hp]87      rw [e, untilHalt_halted _ _ rfl f]88      simp [rolloutWinner_none' hs, rolloutMoves_none hs]89    | some m =>90      have hs : policyStep j P = some (P.set m.1 m.2) := by rw [← policyIdx_step, hp]; rfl91      have e : rsStep (policyIdx j) ⟨P, b, false⟩ = ⟨P.set m.1 m.2, !b, false⟩ := by simp [rsStep, hp]92      rw [e]93      have hL := rolloutMoves_some hs94      obtain ⟨h1, h2, h3⟩ := untilHalt_spec j f (P.set m.1 m.2) (!b) (by omega)95      refine ⟨by rw [h1, rolloutWinner_some' hs]; cases b <;> simp, h2, by rw [h3, hL]⟩9697/-- The fixed clock bound (a function of B and N only). -/98def clockBound (B N : Nat) : Nat := N * (2 ^ B - 1) + 199100theorem clock_ok {B j : Nat} {P : List Nat} (hw : Width B P) : rolloutMoves j P + 1 ≤ clockBound B P.length := by101  have := rolloutMoves_le (j := j) hw; unfold clockBound; omega102103/-! ## The step circuit -/104105def mux (c a b : Circ) : Circ := or [and [c, a], and [not c, b]]106107theorem eval_mux (z : Nat → Bool) (c a b : Circ) :108    eval z (mux c a b) = if eval z c then eval z a else eval z b := by109  unfold mux; cases h : eval z c <;> simp [h]110111/-- A legal binary move exists: valid ∧ (index < N), via the equality decoder. -/112def mvC (S : BCirc) (N : Nat) : Circ := and [S.valid, or ((List.range N).map (decodeC S.idx))]113/-- Active step: halt = 0 and a move exists. -/114def actC (B N : Nat) (S : BCirc) : Circ := and [not (input (B * N + 1)), mvC S N]115/-- The reset input wire. -/116def rstC (B N : Nat) : Circ := input (B * N + 2)117/-- New board bit w = B·i + p: on reset the external bit; if active and the index is i,118    the selector's value bit p; otherwise the old bit. -/119def boardC (B N : Nat) (S : BCirc) (w : Nat) : Circ :=120  mux (rstC B N) (input (B * N + 3 + w))121    (mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w))122/-- New outcome bit: toggled on an active step, cleared on reset. -/123def parC (B N : Nat) (S : BCirc) : Circ := and [not (rstC B N), xor2 (actC B N S) (input (B * N))]124/-- New halt bit: set exactly when the step is not active, cleared on reset. -/125def haltC (B N : Nat) (S : BCirc) : Circ := and [not (rstC B N), not (actC B N S)]126127/-- THE STEP CIRCUIT: B·N board outputs, then par, then halt. -/128def stepForms (B N : Nat) (S : BCirc) : List Circ :=129  (List.range (B * N)).map (boardC B N S) ++ [parC B N S, haltC B N S]130131theorem stepForms_length (B N : Nat) (S : BCirc) : (stepForms B N S).length = B * N + 2 := by132  simp [stepForms]133134/-- Encoding of the registers: board bits, then par (wire B·N), then halt (wire B·N+1). -/135def rsBits (B N : Nat) (s : RS) : Nat → Bool := fun w =>136  if w < B * N then boardBits B s.board w else if w = B * N then s.par else if w = B * N + 1 then s.halted137  else false138139/-- Step input: registers (wires < B·N+2), reset (wire B·N+2), external board (from B·N+3). -/140def stepIn (B N : Nat) (v : Nat → Bool) (rst : Bool) (ext : List Nat) : Nat → Bool := fun w =>141  if w < B * N + 2 then v w else if w = B * N + 2 then rst else boardBits B ext (w - (B * N + 3))142143/-- One clocked update of the register vector (zero beyond the register wires). -/144def bitStep (B N : Nat) (S : BCirc) (v : Nat → Bool) (rst : Bool) (ext : List Nat) : Nat → Bool := fun w =>145  if w < B * N + 2 then eval (stepIn B N v rst ext) ((stepForms B N S).getD w (const false)) else false146147/-- What the step circuit needs from a selector S in binary format. -/148structure PolSpec (S : BCirc) (B N : Nat) (pol : List Nat → Option (Nat × Nat)) : Prop where149  idx_w : N ≤ 2 ^ S.idx.length150  val_len : S.val.length = B151  reads : ∀ c ∈ bForms S, maxInput c ≤ B * N152  sem : ∀ P : List Nat, P.length = N → Width B P → binSem S N (boardBits B P) = pol P153154theorem polSpec_polBin (B N j : Nat) : PolSpec (polBin B N j (rIdx N)) B N (policyIdx j) := by155  have hb := polBin_bound (B := B) (N := N) (j := j) (rIdx_width N)156  exact ⟨by rw [hb.idx_len]; exact rIdx_width N, hb.val_len, fun c hc => (hb.all c hc).2.2,157    fun P hP hw => (polBin_correct (rIdx_width N) hP hw).1⟩158159/-! ### Evaluation lemmas -/160161theorem stepForms_board {B N : Nat} {S : BCirc} {w : Nat} (hw : w < B * N) :162    (stepForms B N S).getD w (const false) = boardC B N S w := by163  unfold stepForms164  rw [List.getD_eq_getElem?_getD, List.getElem?_append_left (by simpa using hw), List.getElem?_map,165    List.getElem?_range hw]166  rfl167168theorem stepForms_par (B N : Nat) (S : BCirc) : (stepForms B N S).getD (B * N) (const false) = parC B N S := by169  unfold stepForms170  rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by simp)]171  simp172173theorem stepForms_halt (B N : Nat) (S : BCirc) :174    (stepForms B N S).getD (B * N + 1) (const false) = haltC B N S := by175  unfold stepForms176  rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by simp)]177  simp178179theorem any_decode (z : Nat → Bool) (idx : List Circ) {N : Nat} (hw : N ≤ 2 ^ idx.length) :180    ((List.range N).map (decodeC idx)).any (eval z) = decide (toNatBE (idx.map (eval z)) < N) := by181  apply Bool.eq_iff_iff.mpr182  rw [List.any_eq_true, decide_eq_true_iff]183  constructor184  · rintro ⟨c, hc, he⟩185    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc186    have hi' := List.mem_range.mp hi187    rw [decodeC_eval z idx (by omega), decide_eq_true_iff] at he188    omega189  · intro h190    refine ⟨decodeC idx (toNatBE (idx.map (eval z))), List.mem_map.mpr ⟨_, List.mem_range.mpr h, rfl⟩, ?_⟩191    rw [decodeC_eval z idx (by omega)]; simp192193theorem eval_mvC (S : BCirc) {N : Nat} (hw : N ≤ 2 ^ S.idx.length) (z : Nat → Bool) :194    eval z (mvC S N) = (binSem S N z).isSome := by195  unfold mvC binSem196  simp only [eval_and, eval_or, List.all_cons, List.all_nil, Bool.and_true]197  rw [any_decode z S.idx hw]198  by_cases hv : eval z S.valid199  · simp only [hv, Bool.true_and, if_true]200    by_cases ht : toNatBE (S.idx.map (eval z)) < N <;> simp [ht]201  · simp [hv]202203theorem maxInput_decodeC {idx : List Circ} {M : Nat} (h : ∀ c ∈ idx, maxInput c ≤ M) (i : Nat) :204    maxInput (decodeC idx i) ≤ M := by205  unfold decodeC206  apply ControllerBits.maxInput_and_le; intro c hc207  obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc208  have hm : getC idx q ∈ idx := getC_mem (List.mem_range.mp hq)209  unfold litEq; split <;> simp [h _ hm]210211theorem maxInput_getC_le {cs : List Circ} {M : Nat} (h : ∀ c ∈ cs, maxInput c ≤ M) (i : Nat) :212    maxInput (getC cs i) ≤ M := by213  unfold getC; rw [List.getD_eq_getElem?_getD]214  cases hc : cs[i]? with215  | none => simp216  | some c => exact h c (List.mem_of_getElem? hc)217218theorem getD_set_nat (P : List Nat) (i v k : Nat) (hi : i < P.length) :219    (P.set i v).getD k 0 = if k = i then v else P.getD k 0 := by220  simp only [List.getD_eq_getElem?_getD, List.getElem?_set]221  by_cases hk : k = i222  · subst hk; simp [hi]223  · simp [Ne.symm hk, hk]224225theorem boardBits_set {B N : Nat} {P : List Nat} (hl : P.length = N) {i w : Nat} (v : Nat) (hi : i < N)226    (hw : w < B * N) :227    boardBits B (P.set i v) w = if w / B = i then v.testBit (B - 1 - w % B) else boardBits B P w := by228  unfold boardBits229  rw [List.length_set, hl, if_pos hw, if_pos hw, getD_set_nat _ _ _ _ (by rw [hl]; exact hi)]230  by_cases h : w / B = i <;> simp [h]231232/-- ONE-STEP REFINEMENT (no reset): for every register state whose board has N heaps of233    width B, the step circuit computes the encoding of the semantic step. -/234theorem bitStep_run {S : BCirc} {B N : Nat} {pol : List Nat → Option (Nat × Nat)} (hS : PolSpec S B N pol)235    (s : RS) (hl : s.board.length = N) (hw : Width B s.board) (ext : List Nat) :236    bitStep B N S (rsBits B N s) false ext = rsBits B N (rsStep pol s) := by237  -- the input vector and its basic values238  let z := stepIn B N (rsBits B N s) false ext239  have zlow : ∀ i, i < B * N → z i = boardBits B s.board i := by240    intro i hi; simp only [z, stepIn, rsBits]; rw [if_pos (by omega), if_pos hi]241  have zpar : z (B * N) = s.par := by242    simp only [z, stepIn]; rw [if_pos (by omega)]; unfold rsBits243    rw [if_neg (by omega), if_pos rfl]244  have zhalt : z (B * N + 1) = s.halted := by245    simp only [z, stepIn]; rw [if_pos (by omega)]; unfold rsBits246    rw [if_neg (by omega), if_neg (by omega), if_pos rfl]247  have zrst : z (B * N + 2) = false := by simp [z, stepIn]248  have hcongr : ∀ c, maxInput c ≤ B * N → eval z c = eval (boardBits B s.board) c :=249    fun c hc => eval_congr_below _ _ c (fun i hi => zlow i (by omega))250  have hidx : ∀ c ∈ S.idx, maxInput c ≤ B * N := fun c hc => hS.reads c (by simp [bForms, hc])251  have hval : ∀ c ∈ S.val, maxInput c ≤ B * N := fun c hc => hS.reads c (by simp [bForms, hc])252  have hvalid : maxInput S.valid ≤ B * N := hS.reads _ (by simp [bForms])253  have hmv : eval z (mvC S N) = (pol s.board).isSome := by254    rw [hcongr _ (by255      unfold mvC; apply ControllerBits.maxInput_and_le; intro c hc256      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc257      rcases hc with rfl | rfl258      · exact hvalid259      · apply ControllerBits.maxInput_or_le; intro c hc260        obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc261        exact maxInput_decodeC hidx i), eval_mvC S hS.idx_w, hS.sem _ hl hw]262  have hact : eval z (actC B N S) = (!s.halted && (pol s.board).isSome) := by263    simp only [actC, eval_and, eval_not, eval_input, List.all_cons, List.all_nil, Bool.and_true, zhalt, hmv]264  have hdec : ∀ i', i' < N → eval z (decodeC S.idx i') =265      decide (toNatBE (S.idx.map (eval (boardBits B s.board))) = i') := by266    intro i' hi'267    rw [hcongr _ (maxInput_decodeC hidx i'), decodeC_eval _ _ (by have := hS.idx_w; omega)]268  have hvbit : ∀ p, eval z (getC S.val p) = (S.val.map (eval (boardBits B s.board))).getD p false := by269    intro p; rw [hcongr _ (maxInput_getC_le hval p), eval_getC]270  funext w271  unfold bitStep rsBits272  by_cases hw1 : w < B * N273  · -- a board wire274    rw [if_pos (by omega), stepForms_board hw1, if_pos hw1]275    show eval z (boardC B N S w) = _276    simp only [boardC, eval_mux, rstC, eval_input, zrst, Bool.false_eq_true, if_false, eval_and,277      List.all_cons, List.all_nil, Bool.and_true, hact]278    have hwi : w / B < N := by279      rcases Nat.eq_zero_or_pos B with hB | hB280      · subst hB; simp at hw1281      · exact (Nat.div_lt_iff_lt_mul hB).2 (by rw [Nat.mul_comm]; exact hw1)282    rw [zlow w hw1, hdec _ hwi]283    unfold rsStep284    by_cases hh : s.halted285    · simp [hh]286    · simp only [hh, Bool.not_false, Bool.true_and, Bool.false_eq_true, if_false]287      have hsem := hS.sem _ hl hw288      cases hp : pol s.board with289      | none => simp290      | some m =>291        obtain ⟨i, v⟩ := m292        simp only [Option.isSome_some, Bool.true_and, decide_eq_true_eq]293        -- decode the binary semantics294        rw [hp] at hsem295        unfold binSem at hsem296        split at hsem297        · split at hsem298          · next _ hlt =>299            simp only [Option.some.injEq, Prod.mk.injEq] at hsem300            obtain ⟨hi, hv⟩ := hsem301            have hiN : i < N := by rw [← hi]; exact hlt302            rw [boardBits_set hl v hiN hw1]303            by_cases hc : toNatBE (S.idx.map (eval (boardBits B s.board))) = w / B304            · rw [if_pos hc, hvbit]305              have hwi' : w / B = i := by rw [← hc, hi]306              rw [if_pos hwi', ← hv]307              have hpB : w % B < B := Nat.mod_lt _ (by308                rcases Nat.eq_zero_or_pos B with hB | hB309                · subst hB; simp at hw1310                · exact hB)311              have := testBit_toNatBE (S.val.map (eval (boardBits B s.board))) (w % B) (by simp [hS.val_len, hpB])312              simp only [List.length_map, hS.val_len] at this313              rw [this]314            · rw [if_neg hc]315              have hwi' : ¬ w / B = i := by rw [← hi]; exact fun h => hc h.symm316              rw [if_neg hwi']317          · cases hsem318        · cases hsem319  · rw [if_neg hw1]320    by_cases hw2 : w = B * N321    · subst hw2322      rw [if_pos (by omega), stepForms_par, if_pos rfl]323      show eval z (parC B N S) = _324      simp only [parC, rstC, eval_and, eval_not, eval_input, eval_xor2, List.all_cons, List.all_nil,325        Bool.and_true, zrst, Bool.not_false, Bool.true_and, hact, zpar]326      unfold rsStep327      by_cases hh : s.halted328      · simp [hh]329      · cases pol s.board <;> simp [hh]330    · rw [if_neg hw2]331      by_cases hw3 : w = B * N + 1332      · subst hw3333        rw [if_pos (by omega), stepForms_halt, if_pos rfl]334        show eval z (haltC B N S) = _335        simp only [haltC, rstC, eval_and, eval_not, eval_input, List.all_cons, List.all_nil,336          Bool.and_true, zrst, Bool.not_false, Bool.true_and, hact]337        unfold rsStep338        by_cases hh : s.halted339        · simp [hh]340        · cases pol s.board <;> simp [hh]341      · rw [if_neg hw3, if_neg (by omega)]342343/-- RESET: from ANY register vector, a reset step loads the external board and clears par344    and halt. -/345theorem bitStep_reset (B N : Nat) (S : BCirc) (v : Nat → Bool) (ext : List Nat) :346    bitStep B N S v true ext = rsBits B N ⟨ext, false, false⟩ := by347  funext w348  unfold bitStep rsBits349  have zrst : stepIn B N v true ext (B * N + 2) = true := by simp [stepIn]350  by_cases hw1 : w < B * N351  · rw [if_pos (by omega), stepForms_board hw1, if_pos hw1]352    simp only [boardC, eval_mux, rstC, eval_input, zrst, if_true]353    simp only [stepIn]354    rw [if_neg (by omega), if_neg (by omega)]355    congr 1; omega356  · rw [if_neg hw1]357    by_cases hw2 : w = B * N358    · subst hw2359      rw [if_pos (by omega), stepForms_par, if_pos rfl]360      simp [parC, rstC, zrst]361    · rw [if_neg hw2]362      by_cases hw3 : w = B * N + 1363      · subst hw3364        rw [if_pos (by omega), stepForms_halt, if_pos rfl]365        simp [haltC, rstC, zrst]366      · rw [if_neg hw3, if_neg (by omega)]367368/-! ## The scheduler at bit level -/369370/-- Generic "while halt = 0, clock the step" loop on register vectors, reading only the371    halt wire; returns the final vector and the number of clocked steps. -/372def loopUntil (step : (Nat → Bool) → (Nat → Bool)) (hw : Nat) : Nat → (Nat → Bool) → (Nat → Bool) × Nat373  | 0, v => (v, 0)374  | f + 1, v => if v hw then (v, 0) else375      ((loopUntil step hw f (step v)).1, (loopUntil step hw f (step v)).2 + 1)376377theorem loopUntil_congr {step step' : (Nat → Bool) → (Nat → Bool)} (h : ∀ v, step v = step' v) (hw : Nat) :378    ∀ f v, loopUntil step hw f v = loopUntil step' hw f v379  | 0, _ => rfl380  | f + 1, v => by simp only [loopUntil, h v, loopUntil_congr h hw f (step' v)]381382theorem rsStep_inv {S : BCirc} {B N : Nat} {pol : List Nat → Option (Nat × Nat)} (hS : PolSpec S B N pol)383    (s : RS) (hl : s.board.length = N) (hw : Width B s.board) :384    (rsStep pol s).board.length = N ∧ Width B (rsStep pol s).board := by385  unfold rsStep386  by_cases hh : s.halted387  · simp [hh, hl, hw]388  · simp only [hh, Bool.false_eq_true, if_false]389    cases hp : pol s.board with390    | none => exact ⟨hl, hw⟩391    | some m =>392      obtain ⟨i, v⟩ := m393      have hsem := hS.sem _ hl hw394      rw [hp] at hsem395      have hv : v < 2 ^ B := by396        unfold binSem at hsem397        split at hsem398        · split at hsem399          · simp only [Option.some.injEq, Prod.mk.injEq] at hsem400            rw [← hsem.2]401            have := toNatBE_lt (S.val.map (eval (boardBits B s.board)))402            simpa [hS.val_len] using this403          · cases hsem404        · cases hsem405      refine ⟨by simp [hl], fun x hx => ?_⟩406      rcases List.mem_or_eq_of_mem_set hx with h | h407      · exact hw x h408      · rw [h]; exact hv409410/-- RUN REFINEMENT: the bit-level scheduler with the step circuit computes the encoding411    of the semantic scheduler, step count included. -/412theorem loop_refines {S : BCirc} {B N : Nat} {pol : List Nat → Option (Nat × Nat)} (hS : PolSpec S B N pol) :413    ∀ (f : Nat) (s : RS), s.board.length = N → Width B s.board →414    loopUntil (fun v => bitStep B N S v false []) (B * N + 1) f (rsBits B N s) =415      (rsBits B N (untilHalt pol f s).1, (untilHalt pol f s).2)416  | 0, s, _, _ => rfl417  | f + 1, s, hl, hw => by418    have hh : rsBits B N s (B * N + 1) = s.halted := by419      unfold rsBits; rw [if_neg (by omega), if_neg (by omega), if_pos rfl]420    simp only [loopUntil, untilHalt, hh]421    by_cases hs : s.halted422    · simp [hs]423    · simp only [hs, Bool.false_eq_true, if_false]424      rw [bitStep_run hS s hl hw []]425      obtain ⟨hl', hw'⟩ := rsStep_inv hS s hl hw426      rw [loop_refines hS f (rsStep pol s) hl' hw']427428/-! ## The executor (Boolean step circuit) -/429430/-- Finite-register execution of rollout j on board P (N = |P|): one reset step loading P431    from an arbitrary register vector v0, then the halting loop with the fixed clock432    bound.  Returns the final register vector and the number of clocked policy steps. -/433def execRoll (B j : Nat) (v0 : Nat → Bool) (P : List Nat) : (Nat → Bool) × Nat :=434  loopUntil (fun v => bitStep B P.length (polBin B P.length j (rIdx P.length)) v false []) (B * P.length + 1)435    (clockBound B P.length) (bitStep B P.length (polBin B P.length j (rIdx P.length)) v0 true P)436437/-- EXECUTOR THEOREM: from any initial register contents, the finite-register executor438    ends with halt = 1, its outcome bit equal to the rollout outcome RO_{π_j}(P), after439    exactly L + 1 policy evaluations (L simulated moves and the terminal test). -/440theorem execRoll_spec {B j : Nat} (v0 : Nat → Bool) {P : List Nat} (hw : Width B P) :441    (execRoll B j v0 P).1 (B * P.length) = rolloutWinner j P ∧442    (execRoll B j v0 P).1 (B * P.length + 1) = true ∧443    (execRoll B j v0 P).2 = rolloutMoves j P + 1 := by444  unfold execRoll445  rw [bitStep_reset, loop_refines (polSpec_polBin B P.length j) _ _ rfl hw]446  obtain ⟨h1, h2, h3⟩ := untilHalt_spec j (clockBound B P.length) P false (clock_ok hw)447  refine ⟨?_, ?_, h3⟩448  · show rsBits B P.length _ (B * P.length) = _449    unfold rsBits; rw [if_neg (by omega), if_pos rfl, h1]; simp450  · show rsBits B P.length _ (B * P.length + 1) = _451    unfold rsBits; rw [if_neg (by omega), if_neg (by omega), if_pos rfl, h2]452453/-! ## The step circuit as a fixed-scale threshold network -/454455def stepNet (B N j : Nat) : List Layer := compileF (stepForms B N (polBin B N j (rIdx N)))456457def netStep (B N j : Nat) (v : Nat → Bool) (rst : Bool) (ext : List Nat) : Nat → Bool := fun w =>458  if w < B * N + 2 then evalNet (stepNet B N j) (stepIn B N v rst ext) w else false459460theorem netStep_eq (B N j : Nat) (v : Nat → Bool) (rst : Bool) (ext : List Nat) :461    netStep B N j v rst ext = bitStep B N (polBin B N j (rIdx N)) v rst ext := by462  funext w463  unfold netStep bitStep stepNet464  by_cases hw : w < B * N + 2465  · rw [if_pos hw, if_pos hw, compileF_eval _ _ (by rw [stepForms_length]; exact hw),466      List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by rw [stepForms_length]; exact hw)]467    rfl468  · rw [if_neg hw, if_neg hw]469470/-- The executor driven by the THRESHOLD NETWORK step. -/471def execRollN (B j : Nat) (v0 : Nat → Bool) (P : List Nat) : (Nat → Bool) × Nat :=472  loopUntil (fun v => netStep B P.length j v false []) (B * P.length + 1)473    (clockBound B P.length) (netStep B P.length j v0 true P)474475theorem execRollN_eq (B j : Nat) (v0 : Nat → Bool) (P : List Nat) : execRollN B j v0 P = execRoll B j v0 P := by476  unfold execRollN execRoll477  rw [netStep_eq]478  exact loopUntil_congr (fun v => netStep_eq _ _ _ v false []) _ _ _479480theorem execRollN_spec {B j : Nat} (v0 : Nat → Bool) {P : List Nat} (hw : Width B P) :481    (execRollN B j v0 P).1 (B * P.length) = rolloutWinner j P ∧482    (execRollN B j v0 P).1 (B * P.length + 1) = true ∧483    (execRollN B j v0 P).2 = rolloutMoves j P + 1 := by484  rw [execRollN_eq]; exact execRoll_spec v0 hw485486/-! ## Composition: B executed rollouts, then the compiled readout -/487488/-- The outcome bit of rollout j produced by the network executor (registers start from489    the all-zero vector; any start works by `execRollN_spec`). -/490def outBit (B j : Nat) (P : List Nat) : Bool := (execRollN B j (fun _ => false) P).1 (B * P.length)491492/-- Policy-network evaluations used by rollout j (clocked steps of the executor). -/493def polEvals (B j : Nat) (P : List Nat) : Nat := (execRollN B j (fun _ => false) P).2494495/-- THE FULLY EXECUTED MULTI-HEAD DECISION: finite-register rollouts, then the readout496    network on the board and the B executed outcome bits. -/497def mhExec (B : Nat) (P : List Nat) : Option (Nat × Nat) :=498  netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B499    (obsIn B P.length P (fun j => outBit B j P))500501def mhExecSel (B : Nat) (P : List Nat) : Option (List Nat) := applyM P (mhExec B P)502503theorem outBit_eq {B j : Nat} {P : List Nat} (hw : Width B P) : outBit B j P = rolloutWinner j P :=504  (execRollN_spec _ hw).1505506theorem mhExec_eq {B : Nat} {P : List Nat} (hw : Width B P) : mhExec B P = decisionMove P := by507  have ho : (fun j => outBit B j P) = outcomes P := by funext j; exact outBit_eq hw508  unfold mhExec; rw [ho]509  exact mhNet_correct (rIdx_width _) rfl hw510511theorem mhExec_eq_mhMove {B : Nat} {P : List Nat} (hw : Width B P) : mhExec B P = mhMove B P := by512  rw [mhExec_eq hw, mhMove_eq hw]513514theorem mhExecSel_eq {B : Nat} {P : List Nat} (hw : Width B P) : mhExecSel B P = ctrlSel P := by515  unfold mhExecSel ctrlSel; rw [mhExec_eq hw]; cases decisionMove P <;> rfl516517/-- WHOLE-GAME THEOREM FOR THE FULLY EXECUTED MULTI-HEAD PLAYER: from every nonzero board518    of width B it wins against every legal opponent; no outcome bit is supplied for free. -/519theorem mhExec_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (mhExecSel B) P :=520  wins_congr (fun Q hQ => mhExecSel_eq hQ) hw (ctrl_wins P h)521522/-- EVALUATION ACCOUNTING for one multi-head decision: rollout j makes L_j + 1 policy523    evaluations; together Σ_j (L_j + 1) = (total simulated moves) + B ≤ B·(N(2^B−1)+1);524    in addition there are B reset steps (one per rollout) and ONE readout evaluation. -/525theorem mhExec_evals {B : Nat} {P : List Nat} (hw : Width B P) :526    (∀ j, polEvals B j P = rolloutMoves j P + 1) ∧527    ((List.range B).map (fun j => polEvals B j P)).sum = totalRolloutMoves B P + B ∧528    totalRolloutMoves B P + B ≤ B * clockBound B P.length := by529  have he : ∀ j, polEvals B j P = rolloutMoves j P + 1 := fun j => (execRollN_spec _ hw).2.2530  refine ⟨he, ?_, ?_⟩531  · unfold totalRolloutMoves532    rw [List.map_congr_left (fun j _ => he j)]533    induction B with534    | zero => simp535    | succ k ih =>536      rw [List.range_succ, List.map_append, List.map_append, List.sum_append_nat, List.sum_append_nat]537      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]538      have : ((List.range k).map (fun j => rolloutMoves j P + 1)).sum = ((List.range k).map (fun j => rolloutMoves j P)).sum + k := by539        clear ih he hw540        induction k with541        | zero => simp542        | succ k ih2 =>543          rw [List.range_succ, List.map_append, List.map_append, List.sum_append_nat, List.sum_append_nat, ih2]544          simp; omega545      omega546  · have := totalRolloutMoves_le hw547    unfold clockBound; rw [Nat.mul_add, Nat.mul_one]; omega548549/-- COST CORRECTION for the phase-5 loop: `WholeGame.rollMoves` calls the policy network550    once more than it moves (the terminal test).  rollCalls counts its polStepN calls. -/551def rollCalls (B j : Nat) : Nat → List Nat → Nat552  | 0, _ => 0553  | f + 1, P => match polStepN B j P with554    | none => 1555    | some Q => rollCalls B j f Q + 1556557theorem rollCalls_eq {B j : Nat} : ∀ (f : Nat) (P : List Nat), Width B P → P.sum ≤ f →558    rollCalls B j (f + 1) P = rolloutMoves j P + 1 ∧ rollCalls B j (f + 1) P = rollMoves B j (f + 1) P + 1559  | f, P, hw, hf => by560    simp only [rollCalls, rollMoves, polStepN_eq hw]561    cases h : policyStep j P with562    | none => simp [rolloutMoves_none h]563    | some Q =>564      simp only565      have hm := policyStep_move h566      have hlt := move_sum_lt hm567      cases f with568      | zero => omega569      | succ f =>570        obtain ⟨h1, h2⟩ := rollCalls_eq (B := B) (j := j) f Q (width_move hw hm) (by omega)571        rw [rolloutMoves_some h]; omega572573/-- The phase-5 multi-head player `mhSelect` performs Σ_j (L_j + 1) policy-network calls574    and one readout call: the simulated-move count of mhSelect_cost plus B + 1. -/575theorem mhSelect_calls {B : Nat} {P : List Nat} (hw : Width B P) :576    ((List.range B).map (fun j => rollCalls B j (P.sum + 1) P)).sum + 1 = totalRolloutMoves B P + B + 1 := by577  have e := fun j => (rollCalls_eq (B := B) (j := j) P.sum P hw (Nat.le_refl _)).1578  rw [List.map_congr_left (fun j _ => e j)]579  have h := (mhExec_evals (B := B) hw).2.1580  have he := (mhExec_evals (B := B) hw).1581  rw [List.map_congr_left (fun j _ => he j)] at h582  omega583584/-- SEQUENTIAL TIME IS NOT CONSTANT: for every T there is a board (B = 1, all heaps 1)585    on which rollout 0 needs more than T clocked steps. -/586theorem unbounded_steps (T : Nat) : ∃ P : List Nat, Width 1 P ∧ T < polEvals 1 0 P := by587  refine ⟨List.replicate T 1, fun x hx => by rw [List.eq_of_mem_replicate hx]; decide, ?_⟩588  unfold polEvals589  rw [(execRollN_spec (B := 1) (j := 0) _ (fun x hx => by rw [List.eq_of_mem_replicate hx]; decide)).2.2,590    rolloutMoves_eq]591  have : rolloutCount 0 (List.replicate T 1) = T := by592    unfold rolloutCount heapCount593    induction T with594    | zero => rfl595    | succ T ih => simp [List.replicate_succ] at ih ⊢; omega596  omega597598599/-! ## Resources of the step circuit -/600601theorem depth_mux_le (c a b : Circ) : depth (mux c a b) ≤ max (depth c + 1) (max (depth a) (depth b)) + 2 := by602  simp only [mux, depth_or, depth_and, depth_not, List.map_cons, List.map_nil, listMax, List.foldr]; omega603604theorem size_mux (c a b : Circ) : size (mux c a b) = 2 * size c + size a + size b + 4 := by605  simp only [mux, size_or, size_and, size_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]; omega606607theorem maxInput_mux (c a b : Circ) : maxInput (mux c a b) ≤ max (maxInput c) (max (maxInput a) (maxInput b)) := by608  simp only [mux, maxInput_or, maxInput_and, maxInput_not, List.map_cons, List.map_nil, listMax, List.foldr]; omega609610theorem xor2_res (a b : Circ) : depth (xor2 a b) ≤ max (depth a) (depth b) + 3 ∧611    size (xor2 a b) = 2 * size a + 2 * size b + 5 ∧ maxInput (xor2 a b) ≤ max (maxInput a) (maxInput b) := by612  simp only [xor2, depth_or, depth_and, depth_not, size_or, size_and, size_not, maxInput_or, maxInput_and,613    maxInput_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr]614  refine ⟨by omega, by omega, by omega⟩615616/-- Per-formula size bound of the step circuit (r index bits, N heaps, selector size Sz). -/617def stepZ (r N Sz : Nat) : Nat :=618  2 * ((Sz + N * (r * (Sz + 1) + 1) + 2 + 3) + (r * (Sz + 1) + 1) + 1) + Sz + 13 +619    2 * (Sz + N * (r * (Sz + 1) + 1) + 2 + 3) + 10620621/-- STEP-CIRCUIT RESOURCES: from a selector with BinBound (depth ≤ D, size ≤ Sz, reading622    the board), every step formula has depth ≤ D + 11, size ≤ stepZ and reads only the623    2·B·N + 3 step inputs. -/624theorem stepForms_res {S : BCirc} {N B r D Sz : Nat} (hb : BinBound S N B r D Sz (B * N)) :625    ∀ c ∈ stepForms B N S, depth c ≤ D + 11 ∧ size c ≤ stepZ r N Sz ∧ maxInput c ≤ 2 * (B * N) + 3 := by626  have hbb := bbound_of_bin hb627  have hdec := fun i => decodeC_resources hbb i628  have hval : ∀ p, depth (getC S.val p) ≤ D ∧ size (getC S.val p) ≤ Sz + 1 ∧ maxInput (getC S.val p) ≤ B * N := by629    intro p; unfold getC; rw [List.getD_eq_getElem?_getD]630    cases h : S.val[p]? with631    | none => simp632    | some c =>633      have hm := List.mem_of_getElem? h634      exact ⟨hbb.depth_val c hm, Nat.le_succ_of_le (hbb.size_val c hm), hbb.max_val c hm⟩635  have hmv : depth (mvC S N) ≤ D + 4 ∧ size (mvC S N) ≤ Sz + N * (r * (Sz + 1) + 1) + 2 ∧636      maxInput (mvC S N) ≤ B * N := by637    have hor : depth (or ((List.range N).map (decodeC S.idx))) ≤ D + 3 ∧638        size (or ((List.range N).map (decodeC S.idx))) ≤ N * (r * (Sz + 1) + 1) + 1 ∧639        maxInput (or ((List.range N).map (decodeC S.idx))) ≤ B * N := by640      refine ⟨depth_or_le (fun c hc => ?_), ?_, ControllerBits.maxInput_or_le (fun c hc => ?_)⟩641      · obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (hdec i).1642      · rw [size_or]643        have := sum_le_len_mul (cs := (List.range N).map (decodeC S.idx)) (S := r * (Sz + 1) + 1)644          (fun c hc => by obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (hdec i).2.1)645        simp only [List.length_map, List.length_range] at this; omega646      · obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (hdec i).2.2647    unfold mvC648    simp only [depth_and, size_and, maxInput_and, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil,649      listMax, List.foldr]650    have := hbb.depth_valid; have := hbb.size_valid; have := hbb.max_valid651    refine ⟨by omega, by omega, by omega⟩652  have hact : depth (actC B N S) ≤ D + 5 ∧ size (actC B N S) ≤ Sz + N * (r * (Sz + 1) + 1) + 2 + 3 ∧653      maxInput (actC B N S) ≤ B * N + 2 := by654    unfold actC655    simp only [depth_and, size_and, maxInput_and, depth_not, size_not, maxInput_not, depth_input, size_input,656      maxInput_input, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr]657    refine ⟨by omega, by omega, by omega⟩658  intro c hc659  simp only [stepForms, List.mem_append, List.mem_map, List.mem_range, List.mem_cons, List.mem_nil_iff,660    or_false] at hc661  rcases hc with ⟨w, hw, rfl⟩ | rfl | rfl662  · -- board formula663    obtain ⟨d1, s1, m1⟩ := hdec (w / B)664    obtain ⟨d2, s2, m2⟩ := hval (w % B)665    have hc1 : depth (and [actC B N S, decodeC S.idx (w / B)]) ≤ D + 6 ∧666        size (and [actC B N S, decodeC S.idx (w / B)]) ≤ (Sz + N * (r * (Sz + 1) + 1) + 2 + 3) + (r * (Sz + 1) + 1) + 1 ∧667        maxInput (and [actC B N S, decodeC S.idx (w / B)]) ≤ B * N + 2 := by668      simp only [depth_and, size_and, maxInput_and, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil,669        listMax, List.foldr]670      refine ⟨by omega, by omega, by omega⟩671    have hin := depth_mux_le (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w)672    have hins := size_mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w)673    have hinm := maxInput_mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w)674    unfold boardC rstC675    have ho := depth_mux_le (input (B * N + 2)) (input (B * N + 3 + w))676      (mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w))677    have hos := size_mux (input (B * N + 2)) (input (B * N + 3 + w))678      (mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w))679    have hom := maxInput_mux (input (B * N + 2)) (input (B * N + 3 + w))680      (mux (and [actC B N S, decodeC S.idx (w / B)]) (getC S.val (w % B)) (input w))681    simp only [depth_input, size_input, maxInput_input] at ho hos hom hin hins hinm682    unfold stepZ683    refine ⟨by omega, by omega, by omega⟩684  · -- par685    obtain ⟨x1, x2, x3⟩ := xor2_res (actC B N S) (input (B * N))686    unfold parC rstC687    simp only [depth_and, size_and, maxInput_and, depth_not, size_not, maxInput_not, depth_input, size_input,688      maxInput_input, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr] at x1 x2 x3 ⊢689    unfold stepZ690    refine ⟨by omega, by omega, by omega⟩691  · -- halt692    unfold haltC rstC693    simp only [depth_and, size_and, maxInput_and, depth_not, size_not, maxInput_not, depth_input, size_input,694      maxInput_input, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr]695    unfold stepZ696    refine ⟨by omega, by omega, by omega⟩697698/-- Step-circuit members: index (B, (N, j)), input = registers + reset + external board. -/699def stepLen : Nat × (Nat × Nat) → Nat := fun i => 2 * (i.1 * i.2.1) + 3700def stepF (i : Nat × (Nat × Nat)) : List Circ := stepForms i.1 i.2.1 (polS i)701702def stepZE {ι : Type} : PE ι :=703  2 * ((polSzE + vN * (vr * (polSzE + 1) + 1) + 2 + 3) + (vr * (polSzE + 1) + 1) + 1) + polSzE + 13 +704    2 * (polSzE + vN * (vr * (polSzE + 1) + 1) + 2 + 3) + 10705706theorem stepLen_pos (i : Nat × (Nat × Nat)) (_hi : polAdm i) : 1 ≤ stepLen i := by unfold stepLen; omega707theorem step_leaves (k : Nat) (i : Nat × (Nat × Nat)) (hi : polAdm i) : leafBNj k i ≤ stepLen i := by708  have h := pol_leaves k i hi; unfold polLen at h; unfold stepLen; omega709710theorem stepF_tsize (i : Nat × (Nat × Nat)) :711    tsize (stepF i) ≤ (i.1 * i.2.1 + 2) * stepZ (rIdx i.2.1) i.2.1 (polSz i.1 i.2.1) := by712  have h := sum_le_len_mul (cs := stepF i) (S := stepZ (rIdx i.2.1) i.2.1 (polSz i.1 i.2.1))713    (fun c hc => (stepForms_res (pol_bound i) c hc).2.1)714  unfold stepF at h ⊢; rw [stepForms_length] at h; exact h715716/-- STEP-CIRCUIT FAMILY CERTIFICATE: depth ≤ 28, input width 2·B·N + 3, total size717    polynomial in that width (one clock step of one rollout). -/718theorem step_ac0 : AC0Fam polAdm stepLen stepF 28 := by719  refine ⟨stepLen_pos, fun i _ c hc => (stepForms_res (pol_bound i) c hc).1,720    fun i _ c hc => (stepForms_res (pol_bound i) c hc).2.2, ?_⟩721  exact polyIn_mono (fun i _ => stepF_tsize i)722    (polyE stepLen_pos leafBNj step_leaves ((vB * vN + 2) * stepZE) _ (fun _ => rfl))723724def stepN (i : Nat × (Nat × Nat)) : List Layer := stepNet i.1 i.2.1 i.2.2725726/-- STEP-NETWORK FAMILY CERTIFICATE (W = 1, ≤ 58 layers). -/727theorem step_net : NetFam polAdm stepLen stepN 1 58 := by728  have spec := fun i => compileF_spec (stepF i) (stepLen i) 28 (fun c hc => (stepForms_res (pol_bound i) c hc).2.2)729    (fun c hc => (stepForms_res (pol_bound i) c hc).1)730  have hT := polyE stepLen_pos leafBNj step_leaves ((vB * vN + 2) * stepZE)731    (fun i => (i.1 * i.2.1 + 2) * stepZ (rIdx i.2.1) i.2.1 (polSz i.1 i.2.1)) (fun _ => rfl)732  refine ⟨stepLen_pos, fun i _ => (spec i).2.2.1, fun i _ => (spec i).2.2.2.1, fun i _ => (spec i).2.2.2.2.1, ?_, ?_⟩733  · obtain ⟨c, k, h⟩ := polyIn_add stepLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (stepLen i)))734    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩735    have := stepF_tsize i; have := h i hi; dsimp only at *; unfold tsize at *; omega736  · have h2 := polyIn_add stepLen_pos (polyIn_mul (polyIn_const _ _ (2 * 28 + 1)) hT)737      (polyE stepLen_pos leafBNj step_leaves (vB * vN + 2) (fun i => i.1 * i.2.1 + 2) (fun _ => rfl))738    refine polyIn_mono (fun i _ => ?_) h2739    have g := (spec i).2.2.2.2.2.2740    have := Nat.mul_le_mul_left (2 * 28 + 1) (stepF_tsize i)741    have hl : (stepF i).length = i.1 * i.2.1 + 2 := by unfold stepF; rw [stepForms_length]742    unfold tsize at this; rw [hl] at g743    show gateCount (stepNet i.1 i.2.1 i.2.2) ≤ _744    exact Nat.le_trans g (by omega)745746/-! ## Bit work of one fully executed multi-head decision -/747748def stepSize (B N j : Nat) : Nat := tsize (stepForms B N (polBin B N j (rIdx N)))749750/-- Formula nodes evaluated: each rollout evaluates the step formulas once per clocked751    step and once for its reset; the readout formulas are evaluated once. -/752def mhWork (B : Nat) (P : List Nat) : Nat :=753  ((List.range B).map (fun j => (polEvals B j P + 1) * stepSize B P.length j)).sum +754    tsize (bForms (mhS (B, P.length)))755756theorem mhWork_le {B : Nat} {P : List Nat} (hw : Width B P) :757    mhWork B P ≤ B * ((P.length * 2 ^ B + 2) * ((B * P.length + 2) * stepZ (rIdx P.length) P.length (polSz B P.length))) +758      (1 + rIdx P.length + B) * mhSz B P.length := by759  unfold mhWork760  have h1 : ∀ j ∈ List.range B, (polEvals B j P + 1) * stepSize B P.length j ≤761      (P.length * 2 ^ B + 2) * ((B * P.length + 2) * stepZ (rIdx P.length) P.length (polSz B P.length)) := by762    intro j _763    have he := (execRollN_spec (j := j) (fun _ => false) hw).2.2764    have hc := clock_ok (j := j) hw765    have hs := stepF_tsize (B, P.length, j)766    unfold stepF at hs767    have hpe : polEvals B j P + 1 ≤ P.length * 2 ^ B + 2 := by768      unfold polEvals; rw [he]; unfold clockBound at hc769      have : P.length * (2 ^ B - 1) ≤ P.length * 2 ^ B := Nat.mul_le_mul_left P.length (Nat.sub_le (2 ^ B) 1)770      omega771    exact Nat.mul_le_mul hpe hs772  have h2 := sum_map_le_mem (l := List.range B) (f := fun j => (polEvals B j P + 1) * stepSize B P.length j)773    (g := fun _ => (P.length * 2 ^ B + 2) * ((B * P.length + 2) * stepZ (rIdx P.length) P.length (polSz B P.length))) h1774  rw [List.map_const', List.sum_replicate_nat, List.length_range] at h2775  have h3 := PriorityEncoder.totalSize_le (mh_bound (B, P.length))776  rw [← tsize_bForms] at h3777  exact Nat.add_le_add h2 h3778779theorem polyIn_comp {ι : Type} {adm : ι → Prop} {len1 len2 : ι → Nat} {f : ι → Nat}780    (h : PolyIn adm len1 f) {c' k' : Nat} (hl : ∀ i, adm i → len1 i ≤ c' * len2 i ^ k') : PolyIn adm len2 f := by781  obtain ⟨c, k, hf⟩ := h782  refine ⟨c * c' ^ k, k' * k, fun i hi => ?_⟩783  calc f i ≤ c * len1 i ^ k := hf i hi784    _ ≤ c * (c' * len2 i ^ k') ^ k := Nat.mul_le_mul_left c (Nat.pow_le_pow_left (hl i hi) k)785    _ = c * c' ^ k * len2 i ^ (k' * k) := by rw [Nat.mul_pow, ← Nat.pow_mul, Nat.mul_assoc]786787/-- Leaves for the work bound: 0 ↦ B, 1 ↦ N, 2 ↦ r, otherwise ↦ 2^B. -/788def leafW : Nat → Nat × Nat → Nat789  | 0, i => i.1790  | 1, i => i.2791  | 2, i => rIdx i.2792  | _, i => 2 ^ i.1793794def workLen : Nat × Nat → Nat := fun i => i.1 * i.2 + 2 ^ i.1795796theorem work_leaves (k : Nat) (i : Nat × Nat) (hi : restAdm i) : leafW k i ≤ workLen i := by797  have hB := Nat.mul_le_mul_left i.1 hi.2798  have hN := Nat.mul_le_mul_right i.2 hi.1799  have hr := rIdx_le hi.2800  have h2 := Nat.two_pow_pos i.1801  match k with802  | 0 => show i.1 ≤ workLen i; unfold workLen; simp at hB; omega803  | 1 => show i.2 ≤ workLen i; unfold workLen; simp at hN; omega804  | 2 => show rIdx i.2 ≤ workLen i; unfold workLen; simp at hN; omega805  | _ + 3 => show 2 ^ i.1 ≤ workLen i; unfold workLen; omega806807/-- BIT WORK IS POLYNOMIAL IN B·N + 2^B (exponential in B in general). -/808theorem mhWork_poly : ∃ c k, ∀ B : Nat, ∀ P : List Nat, 1 ≤ B → 1 ≤ P.length → Width B P →809    mhWork B P ≤ c * (B * P.length + 2 ^ B) ^ k := by810  have hp : ∀ i, restAdm i → 1 ≤ workLen i := fun i hi => by811    show 1 ≤ i.1 * i.2 + 2 ^ i.1; have := Nat.two_pow_pos i.1; omega812  obtain ⟨c, k, h⟩ := polyE hp leafW work_leaves813    (vB * ((vN * PE.v 3 + 2) * ((vB * vN + 2) * stepZE)) + (1 + vr + vB) * mhSzE)814    (fun i => i.1 * ((i.2 * 2 ^ i.1 + 2) * ((i.1 * i.2 + 2) * stepZ (rIdx i.2) i.2 (polSz i.1 i.2))) +815      (1 + rIdx i.2 + i.1) * mhSz i.1 i.2) (fun _ => rfl)816  exact ⟨c, k, fun B P hB hN hw => Nat.le_trans (mhWork_le hw) (h (B, P.length) ⟨hB, hN⟩)⟩817818/-- For B = O(log N), i.e. 2^B ≤ (N+1)^a with a fixed, the bit work of one fully819    executed multi-head decision is polynomial in N. -/820theorem mhWork_poly_logB (a : Nat) : ∃ c k, ∀ B : Nat, ∀ P : List Nat, 1 ≤ B → 1 ≤ P.length → Width B P →821    2 ^ B ≤ (P.length + 1) ^ a → mhWork B P ≤ c * P.length ^ k := by822  have hp : ∀ i, (restAdm i ∧ 2 ^ i.1 ≤ (i.2 + 1) ^ a) → 1 ≤ workLen i :=823    fun i hi => by show 1 ≤ i.1 * i.2 + 2 ^ i.1; have := Nat.two_pow_pos i.1; omega824  have hW := polyE hp leafW (fun k i hi => work_leaves k i hi.1)825    (vB * ((vN * PE.v 3 + 2) * ((vB * vN + 2) * stepZE)) + (1 + vr + vB) * mhSzE)826    (fun i => i.1 * ((i.2 * 2 ^ i.1 + 2) * ((i.1 * i.2 + 2) * stepZ (rIdx i.2) i.2 (polSz i.1 i.2))) +827      (1 + rIdx i.2 + i.1) * mhSz i.1 i.2) (fun _ => rfl)828  have hl : ∀ i, (restAdm i ∧ 2 ^ i.1 ≤ (i.2 + 1) ^ a) → workLen i ≤ (2 * 2 ^ a + 1) * i.2 ^ (a + 1) := by829    intro i ⟨⟨hB, hN⟩, h2⟩830    have hBlt : i.1 < 2 ^ i.1 := Nat.lt_two_pow_self831    have e1 : (i.2 + 1) ^ a ≤ 2 ^ a * i.2 ^ a := by832      rw [← Nat.mul_pow]; exact Nat.pow_le_pow_left (by omega) a833    have e2 : i.2 ^ a ≤ i.2 ^ (a + 1) := Nat.pow_le_pow_right (by omega) (by omega)834    have e3 : i.1 * i.2 ≤ 2 ^ a * i.2 ^ a * i.2 := Nat.mul_le_mul_right _ (by omega)835    have e4 : 2 ^ a * i.2 ^ a * i.2 = 2 ^ a * i.2 ^ (a + 1) := by rw [Nat.mul_assoc, ← Nat.pow_succ]836    have e5 : 2 ^ a * i.2 ^ a ≤ 2 ^ a * i.2 ^ (a + 1) := Nat.mul_le_mul_left _ e2837    have e6 : (2 * 2 ^ a + 1) * i.2 ^ (a + 1) = 2 * (2 ^ a * i.2 ^ (a + 1)) + i.2 ^ (a + 1) := by838      rw [Nat.add_mul, Nat.one_mul, Nat.mul_assoc]839    unfold workLen; omega840  obtain ⟨c, k, h⟩ := polyIn_comp hW hl841  exact ⟨c, k, fun B P hB hN hw h2 => Nat.le_trans (mhWork_le hw) (h (B, P.length) ⟨⟨hB, hN⟩, h2⟩)⟩842843/-! ## Axiom audit -/844845#print axioms untilHalt_halted846#print axioms rolloutWinner_none'847#print axioms rolloutWinner_some'848#print axioms untilHalt_spec849#print axioms clock_ok850#print axioms eval_mux851#print axioms stepForms_length852#print axioms polSpec_polBin853#print axioms stepForms_board854#print axioms stepForms_par855#print axioms stepForms_halt856#print axioms any_decode857#print axioms eval_mvC858#print axioms maxInput_decodeC859#print axioms maxInput_getC_le860#print axioms getD_set_nat861#print axioms boardBits_set862#print axioms bitStep_run863#print axioms bitStep_reset864#print axioms loopUntil_congr865#print axioms rsStep_inv866#print axioms loop_refines867#print axioms execRoll_spec868#print axioms netStep_eq869#print axioms execRollN_eq870#print axioms execRollN_spec871#print axioms outBit_eq872#print axioms mhExec_eq873#print axioms mhExec_eq_mhMove874#print axioms mhExecSel_eq875#print axioms mhExec_wins876#print axioms mhExec_evals877#print axioms rollCalls_eq878#print axioms mhSelect_calls879#print axioms unbounded_steps880#print axioms depth_mux_le881#print axioms size_mux882#print axioms maxInput_mux883#print axioms xor2_res884#print axioms stepForms_res885#print axioms stepLen_pos886#print axioms step_leaves887#print axioms stepF_tsize888#print axioms step_ac0889#print axioms step_net890#print axioms mhWork_le891#print axioms polyIn_comp892#print axioms work_leaves893#print axioms mhWork_poly894#print axioms mhWork_poly_logB895896