Shootout

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 Misc2import BoardStore34/- Phase 7, Part A: the outer shootout controller in bounded binary registers, composed5   with the actual rollout executor.  Written by Claude (10 October 2026).6   Lean 4.26.0, core/Std only.78   ONE MACHINE, TWO SCHEDULES.  The register vector holds9     * the rollout registers of RolloutExec (board B·N bits, outcome parity, halt),10     * run (1 = running, 0 = done/hold), dec (OR of the outcomes consumed so far),11     * the head index j (r bits, LSB first; B ≤ 2^r), and12     * B stored outcome bits o₀ … o_{B−1}.13   Per tick the update reads the registers, a reset bit and the ORIGINAL BOARD P (B·N input14   wires, present at every tick; nothing else).  The schedule flag `early` is a15   construction parameter:16     early = true   the figure's controller: stop at the first outcome 1, or after head B−1;17     early = false  all heads in turn, retaining every outcome (needed for move selection).18   A tick does exactly one of: reset (load P, j := 0); one policy step of head j19   (multiplexed over the B certified step circuits); CONSUME a finished rollout (store its20   outcome, update dec, then stop, or advance j and reload P); hold when done.21   Nothing else enters: no outcome oracle, no nim-sum, no P.sum, no arithmetic primitive.22   Semantics (ostep) → bit formulas (cForms) → compiled network (cNet), with refinement,23   reset from arbitrary bits, termination, exact tick counts, refinement to Misc.shootout,24   and the all-head composition with the existing readout equal to mhExec. -/2526namespace NimAudit27namespace Shootout2829open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit30  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame31  Family Barrier RolloutExec3233/-! ## A1. Semantic registers and one tick -/3435structure OS where36  rs : RS37  run : Bool38  dec : Bool39  j : Nat40  outs : Nat → Bool4142/-- Total reset (from any register contents): load the board, head 0, nothing stored.43    Convention B = 0: there are no heads, run = 0 at once and dec = 0. -/44def initOS (B : Nat) (P : List Nat) : OS := ⟨⟨P, false, false⟩, decide (1 ≤ B), false, 0, fun _ => false⟩4546/-- Stop condition when a rollout has finished: outcome 1 (early schedule) or last head. -/47def coreB (early : Bool) (B : Nat) (s : OS) : Bool := (early && s.rs.par) || decide (s.j = B - 1)4849/-- One tick of the outer controller with its embedded rollout registers. -/50def ostep (early : Bool) (B : Nat) (P : List Nat) (rst : Bool) (s : OS) : OS :=51  if rst then initOS B P52  else if s.run = false then s53  else if s.rs.halted = false then { s with rs := rsStep (policyIdx s.j) s.rs }54  else if coreB early B s then55    { s with run := false, dec := s.dec || s.rs.par, outs := fun h => if h = s.j then s.rs.par else s.outs h }56  else57    ⟨⟨P, false, false⟩, true, s.dec || s.rs.par, s.j + 1, fun h => if h = s.j then s.rs.par else s.outs h⟩5859/-- Valid states: the board has N heaps of width B, the index fits in r bits, and a60    running controller points at an existing head.  (Encodings with j ≥ B are unused; the61    reset maps every bit pattern to a valid state and valid states stay valid.) -/62structure Valid (B N r : Nat) (s : OS) : Prop where63  len : s.rs.board.length = N64  width : Width B s.rs.board65  jfit : s.j < 2 ^ r66  jrun : s.run = true → s.j < B6768/-! ## Binary layout -/6970def SW (B N r : Nat) : Nat := B * N + 4 + r + B71def jW (B N q : Nat) : Nat := B * N + 4 + q72def oW (B N r h : Nat) : Nat := B * N + 4 + r + h7374/-- Register encoding: rollout registers (wires < BN+2), run (BN+2), dec (BN+3), head index75    bits (BN+4 …), stored outcomes (BN+4+r …); zero beyond SW. -/76def enc (B N r : Nat) (s : OS) : Nat → Bool := fun w =>77  if w < B * N + 2 then rsBits B N s.rs w78  else if w = B * N + 2 then s.run79  else if w = B * N + 3 then s.dec80  else if w < B * N + 4 + r then s.j.testBit (w - (B * N + 4))81  else if w < SW B N r then s.outs (w - (B * N + 4 + r))82  else false8384/-- Per-tick input: registers (< SW), reset bit (SW), original board P (SW+1 …). -/85def zIn (B N r : Nat) (x : Nat → Bool) (rst : Bool) (P : List Nat) : Nat → Bool := fun w =>86  if w < SW B N r then x w else if w = SW B N r then rst else boardBits B P (w - (SW B N r + 1))8788/-- Total input width of one update. -/89def IW (B N r : Nat) : Nat := SW B N r + 1 + B * N9091/-! ## A2. The update formulas -/9293def jlit (B N h q : Nat) : Circ := if h.testBit q then input (jW B N q) else not (input (jW B N q))94/-- Equality decoder j = h. -/95def isH (B N r h : Nat) : Circ := and ((List.range r).map (jlit B N h))96/-- Bit q of j + 1: bit q XOR (AND of all lower bits), constant depth. -/97def incB (B N q : Nat) : Circ := xor2 (input (jW B N q)) (and ((List.range q).map (fun t => input (jW B N t))))98/-- Renaming of a rollout step formula into the register layout (reset wire and external99    board of the step circuit are tied to 0: reloading is done by the outer multiplexer). -/100def σR (B N : Nat) : Nat → Circ := fun i => if i < B * N + 2 then input i else const false101/-- Head h's certified rollout step (RolloutExec.stepForms with the binary policy polBin). -/102def hstep (B N h w : Nat) : Circ := subst (σR B N) ((stepForms B N (polBin B N h (rIdx N))).getD w (const false))103/-- HEAD SELECTION: the step of the head named by the index register. -/104def mstep (B N r w : Nat) : Circ := or ((List.range B).map (fun h => and [isH B N r h, hstep B N h w]))105106def rstI (B N r : Nat) : Circ := input (SW B N r)107def parI (B N : Nat) : Circ := input (B * N)108def haltI (B N : Nat) : Circ := input (B * N + 1)109def runI (B N : Nat) : Circ := input (B * N + 2)110def decI (B N : Nat) : Circ := input (B * N + 3)111def lastC (B N r : Nat) : Circ := isH B N r (B - 1)112def coreC (early : Bool) (B N r : Nat) : Circ := if early then or [parI B N, lastC B N r] else lastC B N r113def consC (B N : Nat) : Circ := and [runI B N, haltI B N]114def stepC (B N : Nat) : Circ := and [runI B N, not (haltI B N)]115def stopC (early : Bool) (B N r : Nat) : Circ := and [consC B N, coreC early B N r]116def contC (early : Bool) (B N r : Nat) : Circ := and [consC B N, not (coreC early B N r)]117def loadC (early : Bool) (B N r : Nat) : Circ := or [rstI B N r, contC early B N r]118119def boardF (early : Bool) (B N r w : Nat) : Circ :=120  RolloutExec.mux (loadC early B N r) (input (SW B N r + 1 + w)) (RolloutExec.mux (stepC B N) (mstep B N r w) (input w))121def parF (early : Bool) (B N r : Nat) : Circ :=122  RolloutExec.mux (loadC early B N r) (const false) (RolloutExec.mux (stepC B N) (mstep B N r (B * N)) (input (B * N)))123def haltF (early : Bool) (B N r : Nat) : Circ :=124  RolloutExec.mux (loadC early B N r) (const false) (RolloutExec.mux (stepC B N) (mstep B N r (B * N + 1)) (input (B * N + 1)))125def runF (early : Bool) (B N r : Nat) : Circ :=126  RolloutExec.mux (rstI B N r) (const (decide (1 ≤ B))) (and [runI B N, not (stopC early B N r)])127def decF (B N r : Nat) : Circ := RolloutExec.mux (rstI B N r) (const false) (or [decI B N, and [consC B N, parI B N]])128def jF (early : Bool) (B N r q : Nat) : Circ :=129  RolloutExec.mux (rstI B N r) (const false) (RolloutExec.mux (contC early B N r) (incB B N q) (input (jW B N q)))130def oF (B N r h : Nat) : Circ :=131  RolloutExec.mux (rstI B N r) (const false) (RolloutExec.mux (and [consC B N, isH B N r h]) (parI B N) (input (oW B N r h)))132133/-- THE UPDATE: SW = BN + 4 + r + B formulas, one per register bit. -/134def cForms (early : Bool) (B N r : Nat) : List Circ :=135  (List.range (B * N)).map (boardF early B N r) ++136    ([parF early B N r, haltF early B N r, runF early B N r, decF B N r] ++137      ((List.range r).map (jF early B N r) ++ (List.range B).map (oF B N r)))138139/-- One clocked bit-level update. -/140def cstep (early : Bool) (B N r : Nat) (P : List Nat) (rst : Bool) (x : Nat → Bool) : Nat → Bool := fun w =>141  if w < SW B N r then eval (zIn B N r x rst P) ((cForms early B N r).getD w (const false)) else false142143theorem cForms_length (early : Bool) (B N r : Nat) : (cForms early B N r).length = SW B N r := by144  simp [cForms, SW]; omega145146theorem cF_board {early : Bool} {B N r w : Nat} (hw : w < B * N) :147    (cForms early B N r).getD w (const false) = boardF early B N r w := by148  unfold cForms149  rw [List.getD_eq_getElem?_getD, List.getElem?_append_left (by simpa using hw), List.getElem?_map,150    List.getElem?_range hw]; rfl151152theorem cF_mid (early : Bool) (B N r k : Nat) (hk : k < 4) :153    (cForms early B N r).getD (B * N + k) (const false) =154      [parF early B N r, haltF early B N r, runF early B N r, decF B N r].getD k (const false) := by155  unfold cForms156  rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by simp), List.getElem?_append_left (by simp; omega)]157  simp [List.getD_eq_getElem?_getD]158159theorem cF_par (early : Bool) (B N r : Nat) : (cForms early B N r).getD (B * N) (const false) = parF early B N r := by160  have := cF_mid early B N r 0 (by omega); simpa using this161theorem cF_halt (early : Bool) (B N r : Nat) : (cForms early B N r).getD (B * N + 1) (const false) = haltF early B N r := by162  have := cF_mid early B N r 1 (by omega); simpa using this163theorem cF_run (early : Bool) (B N r : Nat) : (cForms early B N r).getD (B * N + 2) (const false) = runF early B N r := by164  have := cF_mid early B N r 2 (by omega); simpa using this165theorem cF_dec (early : Bool) (B N r : Nat) : (cForms early B N r).getD (B * N + 3) (const false) = decF B N r := by166  have := cF_mid early B N r 3 (by omega); simpa using this167168theorem cF_j {early : Bool} {B N r q : Nat} (hq : q < r) :169    (cForms early B N r).getD (jW B N q) (const false) = jF early B N r q := by170  unfold cForms jW171  rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by simp; omega),172    List.getElem?_append_right (by simp; omega), List.getElem?_append_left (by simp; omega)]173  simp only [List.length_map, List.length_range, List.length_cons, List.length_nil]174  rw [show B * N + 4 + q - B * N - 4 = q by omega, List.getElem?_map, List.getElem?_range hq]; rfl175176theorem cF_o {early : Bool} {B N r h : Nat} (hh : h < B) :177    (cForms early B N r).getD (oW B N r h) (const false) = oF B N r h := by178  unfold cForms oW179  rw [List.getD_eq_getElem?_getD, List.getElem?_append_right (by simp; omega),180    List.getElem?_append_right (by simp; omega), List.getElem?_append_right (by simp; omega)]181  simp only [List.length_map, List.length_range, List.length_cons, List.length_nil]182  rw [show B * N + 4 + r + h - B * N - 4 - r = h by omega, List.getElem?_map, List.getElem?_range hh]; rfl183184/-! ## Signal evaluation -/185186section Signals187188variable {B N r : Nat} (s : OS) (rst : Bool) (P : List Nat)189190theorem z_low {w : Nat} (hw : w < B * N + 2) : zIn B N r (enc B N r s) rst P w = rsBits B N s.rs w := by191  unfold zIn enc SW; rw [if_pos (by omega), if_pos hw]192193theorem z_par : zIn B N r (enc B N r s) rst P (B * N) = s.rs.par := by194  rw [z_low s rst P (by omega)]; unfold rsBits; rw [if_neg (by omega), if_pos rfl]195196theorem z_halt : zIn B N r (enc B N r s) rst P (B * N + 1) = s.rs.halted := by197  rw [z_low s rst P (by omega)]; unfold rsBits; rw [if_neg (by omega), if_neg (by omega), if_pos rfl]198199theorem z_run : zIn B N r (enc B N r s) rst P (B * N + 2) = s.run := by200  unfold zIn enc SW; rw [if_pos (by omega), if_neg (by omega), if_pos rfl]201202theorem z_dec : zIn B N r (enc B N r s) rst P (B * N + 3) = s.dec := by203  unfold zIn enc SW; rw [if_pos (by omega), if_neg (by omega), if_neg (by omega), if_pos rfl]204205theorem z_j {q : Nat} (hq : q < r) : zIn B N r (enc B N r s) rst P (jW B N q) = s.j.testBit q := by206  unfold zIn enc SW jW; rw [if_pos (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega),207    if_pos (by omega)]; congr 1; omega208209theorem z_o {h : Nat} (hh : h < B) : zIn B N r (enc B N r s) rst P (oW B N r h) = s.outs h := by210  unfold zIn enc SW oW; rw [if_pos (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega),211    if_neg (by omega), if_pos (by omega)]; congr 1; omega212213theorem z_rst (x : Nat → Bool) : zIn B N r x rst P (SW B N r) = rst := by214  unfold zIn; rw [if_neg (by omega), if_pos rfl]215216theorem z_P (x : Nat → Bool) (w : Nat) : zIn B N r x rst P (SW B N r + 1 + w) = boardBits B P w := by217  unfold zIn; rw [if_neg (by omega), if_neg (by omega)]; congr 1; omega218219theorem eval_isH_bits (h : Nat) :220    eval (zIn B N r (enc B N r s) rst P) (isH B N r h) = decide (∀ q < r, s.j.testBit q = h.testBit q) := by221  unfold isH222  rw [eval_and]223  apply Bool.eq_iff_iff.mpr224  rw [List.all_eq_true, decide_eq_true_iff]225  constructor226  · intro hall q hq227    have := hall (jlit B N h q) (List.mem_map.mpr ⟨q, List.mem_range.mpr hq, rfl⟩)228    unfold jlit at this229    split at this <;> simp_all [z_j s rst P hq]230  · intro hall c hc231    obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc232    have hq' := List.mem_range.mp hq233    unfold jlit; have := hall q hq'234    split <;> simp_all [z_j s rst P hq']235236theorem eval_isH {h : Nat} (hj : s.j < 2 ^ r) (hh : h < 2 ^ r) :237    eval (zIn B N r (enc B N r s) rst P) (isH B N r h) = decide (s.j = h) := by238  rw [eval_isH_bits]239  apply Bool.eq_iff_iff.mpr240  simp only [decide_eq_true_iff]241  exact ⟨fun hb => BoardStore.eq_of_low_bits hj hh hb, fun e q _ => by rw [e]⟩242243theorem eval_incB {q : Nat} (hq : q < r) :244    eval (zIn B N r (enc B N r s) rst P) (incB B N q) = (s.j + 1).testBit q := by245  unfold incB246  rw [CorrBridge.eval_xor2, eval_input, z_j s rst P hq, ControllerBits.testBit_succ, eval_and]247  congr 1248  apply Bool.eq_iff_iff.mpr249  rw [List.all_eq_true, decide_eq_true_iff]250  constructor251  · intro hall t ht252    have := hall (input (jW B N t)) (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩)253    rwa [eval_input, z_j s rst P (by omega)] at this254  · intro hall c hc255    obtain ⟨t, ht, rfl⟩ := List.mem_map.mp hc256    have ht' := List.mem_range.mp ht257    rw [eval_input, z_j s rst P (by omega)]; exact hall t ht'258259theorem eval_hstep (hl : s.rs.board.length = N) (hwd : Width B s.rs.board) (h : Nat) {w : Nat}260    (hw : w < B * N + 2) :261    eval (zIn B N r (enc B N r s) rst P) (hstep B N h w) = rsBits B N (rsStep (policyIdx h) s.rs) w := by262  unfold hstep263  rw [eval_subst]264  have e : (fun i => eval (zIn B N r (enc B N r s) rst P) (σR B N i)) = stepIn B N (rsBits B N s.rs) false [] := by265    funext i; unfold σR stepIn266    by_cases hi : i < B * N + 2267    · rw [if_pos hi, if_pos hi, eval_input, z_low s rst P hi]268    · rw [if_neg hi, if_neg hi, eval_const]269      split270      · rfl271      · simp [boardBits]272  rw [e]273  have := congrFun (bitStep_run (polSpec_polBin B N h) s.rs hl hwd []) w274  unfold bitStep at this; rw [if_pos hw] at this; exact this275276theorem eval_mstep (hBr : B ≤ 2 ^ r) (hl : s.rs.board.length = N) (hwd : Width B s.rs.board) (hj : s.j < B)277    {w : Nat} (hw : w < B * N + 2) :278    eval (zIn B N r (enc B N r s) rst P) (mstep B N r w) = rsBits B N (rsStep (policyIdx s.j) s.rs) w := by279  unfold mstep280  rw [eval_or]281  apply Bool.eq_iff_iff.mpr282  rw [List.any_eq_true]283  constructor284  · rintro ⟨c, hc, he⟩285    obtain ⟨h, hh, rfl⟩ := List.mem_map.mp hc286    have hh' := List.mem_range.mp hh287    simp only [eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true] at he288    rw [eval_isH s rst P (by omega) (by omega), decide_eq_true_iff] at he289    obtain ⟨rfl, he2⟩ := he290    rwa [eval_hstep s rst P hl hwd _ hw] at he2291  · intro he292    refine ⟨and [isH B N r s.j, hstep B N s.j w], List.mem_map.mpr ⟨s.j, List.mem_range.mpr hj, rfl⟩, ?_⟩293    simp only [eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true]294    rw [eval_isH s rst P (by omega) (by omega), eval_hstep s rst P hl hwd _ hw]295    exact ⟨by simp, he⟩296297end Signals298299/-- ostep without reset, as one flat record of Boolean cases. -/300theorem ostep_flat (early : Bool) (B : Nat) (P : List Nat) (s : OS) :301    ostep early B P false s =302      ⟨if (s.run && s.rs.halted && !coreB early B s) then ⟨P, false, false⟩303        else if (s.run && !s.rs.halted) then rsStep (policyIdx s.j) s.rs else s.rs,304       s.run && !(s.run && s.rs.halted && coreB early B s),305       s.dec || (s.run && s.rs.halted && s.rs.par),306       if (s.run && s.rs.halted && !coreB early B s) then s.j + 1 else s.j,307       fun h => if (s.run && s.rs.halted && decide (h = s.j)) then s.rs.par else s.outs h⟩ := by308  obtain ⟨rs, run, dec, j, outs⟩ := s309  unfold ostep310  cases run <;> cases hh : rs.halted <;> simp only [Bool.false_eq_true, if_false, if_true, Bool.false_and,311    Bool.and_false, Bool.true_and, Bool.not_false, Bool.not_true, Bool.or_false, Bool.and_true, hh] <;>312    (try rfl) <;> (cases hc : coreB early B ⟨rs, true, dec, j, outs⟩ <;> simp [hc])313314/-! ## A1/A2. Reset from arbitrary bits and one-tick refinement -/315316theorem enc_low (B N r : Nat) (s : OS) {w : Nat} (hw : w < B * N + 2) : enc B N r s w = rsBits B N s.rs w := by317  unfold enc; rw [if_pos hw]318319theorem rsBits_board (B N : Nat) (t : RS) {w : Nat} (hw : w < B * N) : rsBits B N t w = boardBits B t.board w := by320  unfold rsBits; rw [if_pos hw]321322theorem rsBits_par (B N : Nat) (t : RS) : rsBits B N t (B * N) = t.par := by323  unfold rsBits; rw [if_neg (by omega), if_pos rfl]324325theorem rsBits_halt (B N : Nat) (t : RS) : rsBits B N t (B * N + 1) = t.halted := by326  unfold rsBits; rw [if_neg (by omega), if_neg (by omega), if_pos rfl]327328theorem enc_run (B N r : Nat) (s : OS) : enc B N r s (B * N + 2) = s.run := by329  unfold enc; rw [if_neg (by omega), if_pos rfl]330331theorem enc_dec (B N r : Nat) (s : OS) : enc B N r s (B * N + 3) = s.dec := by332  unfold enc; rw [if_neg (by omega), if_neg (by omega), if_pos rfl]333334theorem enc_j (B N r : Nat) (s : OS) {q : Nat} (hq : q < r) : enc B N r s (jW B N q) = s.j.testBit q := by335  unfold enc jW; rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_pos (by omega)]; congr 1; omega336337theorem enc_o (B N r : Nat) (s : OS) {h : Nat} (hh : h < B) : enc B N r s (oW B N r h) = s.outs h := by338  unfold enc oW SW; rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega),339    if_pos (by omega)]; congr 1; omega340341theorem enc_high (B N r : Nat) (s : OS) {w : Nat} (hw : SW B N r ≤ w) : enc B N r s w = false := by342  unfold enc SW at *; rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega),343    if_neg (by omega)]344345/-- Every wire below SW is a board, par, halt, run, dec, index or outcome wire. -/346theorem wire_cases (B N r w : Nat) (hw : w < SW B N r) :347    w < B * N ∨ w = B * N ∨ w = B * N + 1 ∨ w = B * N + 2 ∨ w = B * N + 3 ∨348    (∃ q, q < r ∧ w = jW B N q) ∨ (∃ h, h < B ∧ w = oW B N r h) := by349  unfold SW at hw350  by_cases h1 : w < B * N + 4351  · omega352  · by_cases h2 : w < B * N + 4 + r353    · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl ⟨w - (B * N + 4), by omega, by unfold jW; omega⟩)))))354    · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨w - (B * N + 4 + r), by omega, by unfold oW; omega⟩)))))355356/-- TOTAL RESET: from ARBITRARY register bits, a reset tick yields the encoding of the357    initial state (board P loaded, head 0, run = [B ≥ 1], nothing stored). -/358theorem cstep_reset (early : Bool) (B N r : Nat) (P : List Nat) (x : Nat → Bool) :359    cstep early B N r P true x = enc B N r (initOS B P) := by360  funext w361  unfold cstep362  by_cases hw : w < SW B N r363  · rw [if_pos hw]364    have hload : eval (zIn B N r x true P) (loadC early B N r) = true := by365      simp [loadC, rstI, z_rst]366    have hrst : eval (zIn B N r x true P) (rstI B N r) = true := by simp [rstI, z_rst]367    rcases wire_cases B N r w hw with h | h | h | h | h | ⟨q, hq, rfl⟩ | ⟨k, hk, rfl⟩368    · rw [cF_board h, enc_low _ _ _ _ (by omega), rsBits_board _ _ _ h]369      simp only [boardF, eval_mux, hload, if_true, eval_input, z_P]; rfl370    · subst h; rw [cF_par, enc_low _ _ _ _ (by omega), rsBits_par]371      simp [parF, eval_mux, hload, initOS]372    · subst h; rw [cF_halt, enc_low _ _ _ _ (by omega), rsBits_halt]373      simp [haltF, eval_mux, hload, initOS]374    · subst h; rw [cF_run, enc_run]375      simp [runF, eval_mux, hrst, initOS]376    · subst h; rw [cF_dec, enc_dec]377      simp [decF, eval_mux, hrst, initOS]378    · rw [cF_j hq, enc_j _ _ _ _ hq]379      simp [jF, eval_mux, hrst, initOS]380    · rw [cF_o hk, enc_o _ _ _ _ hk]381      simp [oF, eval_mux, hrst, initOS]382  · rw [if_neg hw, enc_high _ _ _ _ (by omega)]383384/-- ONE-TICK REFINEMENT (no reset): on every valid state the update formulas compute the385    encoding of the semantic tick. -/386theorem cstep_enc (early : Bool) {B N r : Nat} (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N)387    {s : OS} (hv : Valid B N r s) :388    cstep early B N r P false (enc B N r s) = enc B N r (ostep early B P false s) := by389  rw [ostep_flat]390  funext w391  unfold cstep392  have hB1 : B - 1 < 2 ^ r := by have := Nat.one_le_two_pow (n := r); omega393  have hr0 : eval (zIn B N r (enc B N r s) false P) (rstI B N r) = false := by simp [rstI, z_rst]394  have hst : eval (zIn B N r (enc B N r s) false P) (stepC B N) = (s.run && !s.rs.halted) := by395    simp [stepC, runI, haltI, z_run, z_halt]396  have hcs : eval (zIn B N r (enc B N r s) false P) (consC B N) = (s.run && s.rs.halted) := by simp [consC, runI, haltI, z_run, z_halt]397  have hcore : eval (zIn B N r (enc B N r s) false P) (coreC early B N r) = coreB early B s := by398    unfold coreC coreB lastC399    cases early400    · simp only [if_false, Bool.false_and, Bool.false_or]; exact eval_isH s false P hv.jfit hB1401    · simp only [if_true, Bool.true_and, eval_or, List.any_cons, List.any_nil, Bool.or_false]402      rw [eval_isH s false P hv.jfit hB1]; simp [parI, z_par]403  have hcont : eval (zIn B N r (enc B N r s) false P) (contC early B N r) = (s.run && s.rs.halted && !coreB early B s) := by404    simp only [contC, eval_and, eval_not, List.all_cons, List.all_nil, Bool.and_true, hcs, hcore]405  have hload : eval (zIn B N r (enc B N r s) false P) (loadC early B N r) = (s.run && s.rs.halted && !coreB early B s) := by406    simp only [loadC, eval_or, List.any_cons, List.any_nil, Bool.or_false, hr0, hcont, Bool.false_or]407  have hstop : eval (zIn B N r (enc B N r s) false P) (stopC early B N r) = (s.run && s.rs.halted && coreB early B s) := by408    simp only [stopC, eval_and, List.all_cons, List.all_nil, Bool.and_true, hcs, hcore]409  have hms : ∀ w, w < B * N + 2 → s.run = true →410      eval (zIn B N r (enc B N r s) false P) (mstep B N r w) = rsBits B N (rsStep (policyIdx s.j) s.rs) w :=411    fun w hw hrun => eval_mstep s false P hBr hv.len hv.width (hv.jrun hrun) hw412  by_cases hw : w < SW B N r413  · rw [if_pos hw]414    rcases wire_cases B N r w hw with h | h | h | h | h | ⟨q, hq, rfl⟩ | ⟨k, hk, rfl⟩415    · rw [cF_board h, enc_low _ _ _ _ (by omega), rsBits_board _ _ _ h]416      show eval (zIn B N r (enc B N r s) false P) (boardF early B N r w) = _417      simp only [boardF, eval_mux, hload, hst, eval_input]418      rw [z_P, z_low s false P (by omega), rsBits_board _ _ _ h]419      by_cases c1 : (s.run && s.rs.halted && !coreB early B s) = true420      · rw [if_pos c1, if_pos c1]421      · rw [if_neg c1, if_neg c1]422        by_cases c2 : (s.run && !s.rs.halted) = true423        · rw [if_pos c2, if_pos c2, hms w (by omega) (by simp at c2; exact c2.1), rsBits_board _ _ _ h]424        · rw [if_neg c2, if_neg c2]425    · subst h; rw [cF_par, enc_low _ _ _ _ (by omega), rsBits_par]426      show eval (zIn B N r (enc B N r s) false P) (parF early B N r) = _427      simp only [parF, eval_mux, hload, hst, eval_input, eval_const]428      rw [z_par]429      by_cases c1 : (s.run && s.rs.halted && !coreB early B s) = true430      · rw [if_pos c1, if_pos c1]431      · rw [if_neg c1, if_neg c1]432        by_cases c2 : (s.run && !s.rs.halted) = true433        · rw [if_pos c2, if_pos c2, hms _ (by omega) (by simp at c2; exact c2.1), rsBits_par]434        · rw [if_neg c2, if_neg c2]435    · subst h; rw [cF_halt, enc_low _ _ _ _ (by omega), rsBits_halt]436      show eval (zIn B N r (enc B N r s) false P) (haltF early B N r) = _437      simp only [haltF, eval_mux, hload, hst, eval_input, eval_const]438      rw [z_halt]439      by_cases c1 : (s.run && s.rs.halted && !coreB early B s) = true440      · rw [if_pos c1, if_pos c1]441      · rw [if_neg c1, if_neg c1]442        by_cases c2 : (s.run && !s.rs.halted) = true443        · rw [if_pos c2, if_pos c2, hms _ (by omega) (by simp at c2; exact c2.1), rsBits_halt]444        · rw [if_neg c2, if_neg c2]445    · subst h; rw [cF_run, enc_run]446      show eval (zIn B N r (enc B N r s) false P) (runF early B N r) = _447      simp only [runF, eval_mux, hr0, eval_and, eval_not, List.all_cons, List.all_nil, Bool.and_true, hstop,448        eval_input, Bool.false_eq_true, if_false]449      rw [show runI B N = input (B * N + 2) from rfl, eval_input, z_run]450    · subst h; rw [cF_dec, enc_dec]451      show eval (zIn B N r (enc B N r s) false P) (decF B N r) = _452      simp only [decF, eval_mux, hr0, eval_or, eval_and, List.any_cons, List.any_nil, List.all_cons,453        List.all_nil, Bool.and_true, Bool.or_false, hcs, eval_input, Bool.false_eq_true, if_false]454      rw [show decI B N = input (B * N + 3) from rfl, show parI B N = input (B * N) from rfl, eval_input,455        eval_input, z_dec, z_par]456    · rw [cF_j hq, enc_j _ _ _ _ hq]457      show eval (zIn B N r (enc B N r s) false P) (jF early B N r q) = _458      simp only [jF, eval_mux, hr0, hcont, eval_input, Bool.false_eq_true, if_false]459      rw [z_j s false P hq]460      by_cases c1 : (s.run && s.rs.halted && !coreB early B s) = true461      · rw [if_pos c1, if_pos c1, eval_incB s false P hq]462      · rw [if_neg c1, if_neg c1]463    · rw [cF_o hk, enc_o _ _ _ _ hk]464      show eval (zIn B N r (enc B N r s) false P) (oF B N r k) = _465      simp only [oF, eval_mux, hr0, eval_and, List.all_cons, List.all_nil, Bool.and_true, hcs, eval_input,466        Bool.false_eq_true, if_false]467      rw [eval_isH s false P hv.jfit (by omega), z_o s false P hk]468      show (if (s.run && s.rs.halted && decide (s.j = k)) = true then eval (zIn B N r (enc B N r s) false P) (parI B N) else s.outs k) = _469      rw [show parI B N = input (B * N) from rfl, eval_input, z_par]470      by_cases c : (s.run && s.rs.halted) = true471      · by_cases e : s.j = k472        · subst e; simp [c]473        · have e' : ¬ k = s.j := fun h => e h.symm474          simp [c, e, e']475      · have : (s.run && s.rs.halted) = false := by simpa using c476        simp [this]477  · rw [if_neg hw, enc_high _ _ _ _ (by omega)]478479/-! ## Invariant, runs and the bit-level/semantic correspondence -/480481theorem initOS_valid {B N r : Nat} {P : List Nat} (hP : P.length = N) (hwP : Width B P) :482    Valid B N r (initOS B P) :=483  ⟨hP, hwP, Nat.two_pow_pos r, fun h => by simp [initOS] at h; simp [initOS]; omega⟩484485theorem ostep_valid (early : Bool) {B N r : Nat} (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N)486    (hwP : Width B P) {s : OS} (hv : Valid B N r s) : Valid B N r (ostep early B P false s) := by487  obtain ⟨hl, hw, hjf, hjr⟩ := hv488  unfold ostep489  cases hr : s.run490  · simp only [Bool.false_eq_true, if_false, if_true]; exact ⟨hl, hw, hjf, hjr⟩491  · have hj := hjr hr492    cases hh : s.rs.halted493    · simp only [Bool.false_eq_true, if_false, if_true]494      obtain ⟨h1, h2⟩ := rsStep_inv (polSpec_polBin B N s.j) s.rs hl hw495      exact ⟨h1, h2, hjf, fun _ => hj⟩496    · cases hc : coreB early B s497      · simp only [Bool.false_eq_true, Bool.true_eq_false, if_false, if_true]498        have hne : s.j ≠ B - 1 := by intro e; unfold coreB at hc; simp [e] at hc499        refine ⟨hP, hwP, ?_, fun _ => ?_⟩ <;> dsimp only <;> omega500      · simp only [Bool.false_eq_true, Bool.true_eq_false, if_false, if_true]501        exact ⟨hl, hw, hjf, fun h => by simp at h⟩502503/-- Semantic run of k ticks (no reset). -/504def arun (early : Bool) (B : Nat) (P : List Nat) : Nat → OS → OS505  | 0, s => s506  | k + 1, s => arun early B P k (ostep early B P false s)507508/-- Bit-level run of k ticks (no reset). -/509def brun (early : Bool) (B N r : Nat) (P : List Nat) : Nat → (Nat → Bool) → (Nat → Bool)510  | 0, x => x511  | k + 1, x => brun early B N r P k (cstep early B N r P false x)512513theorem arun_add (early : Bool) (B : Nat) (P : List Nat) : ∀ a b s, arun early B P (a + b) s = arun early B P b (arun early B P a s)514  | 0, b, s => by simp [arun]515  | a + 1, b, s => by rw [show a + 1 + b = (a + b) + 1 by omega]; simp only [arun]; exact arun_add early B P a b _516517/-- RUN REFINEMENT: from a valid state, k bit-level ticks compute the encoding of k518    semantic ticks, and the state stays valid. -/519theorem brun_enc (early : Bool) {B N r : Nat} (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N)520    (hwP : Width B P) : ∀ (k : Nat) (s : OS), Valid B N r s →521    brun early B N r P k (enc B N r s) = enc B N r (arun early B P k s) ∧ Valid B N r (arun early B P k s)522  | 0, s, hv => ⟨rfl, hv⟩523  | k + 1, s, hv => by524    simp only [brun, arun]525    rw [cstep_enc early hBr hP hv]526    exact brun_enc early hBr hP hwP k _ (ostep_valid early hBr hP hwP hv)527528theorem arun_one (early : Bool) (B : Nat) (P : List Nat) (s : OS) : arun early B P 1 s = ostep early B P false s := rfl529530/-- HOLD: a stopped controller (run = 0) is a fixed point of the tick. -/531theorem ostep_hold (early : Bool) (B : Nat) (P : List Nat) (s : OS) (h : s.run = false) :532    ostep early B P false s = s := by533  unfold ostep; simp [h]534535theorem arun_hold (early : Bool) (B : Nat) (P : List Nat) (s : OS) (h : s.run = false) : ∀ k, arun early B P k s = s536  | 0 => rfl537  | k + 1 => by simp only [arun]; rw [ostep_hold early B P s h]; exact arun_hold early B P s h k538539/-! ## A3. One rollout of head j inside the controller -/540541/-- While the embedded rollout runs, each tick is one step of head j's policy and nothing542    else changes; untilHalt counts these ticks. -/543theorem arun_untilHalt (early : Bool) (B : Nat) (P : List Nat) (s : OS) (hrun : s.run = true) :544    ∀ (f : Nat) (t : RS),545      arun early B P (untilHalt (policyIdx s.j) f t).2 { s with rs := t } = { s with rs := (untilHalt (policyIdx s.j) f t).1 } ∧546      ∀ u, u ≤ (untilHalt (policyIdx s.j) f t).2 → (arun early B P u { s with rs := t }).run = true547  | 0, t => by548    refine ⟨rfl, fun u hu => ?_⟩549    obtain rfl : u = 0 := by simpa [untilHalt] using hu550    simpa [arun] using hrun551  | f + 1, t => by552    by_cases ht : t.halted = true553    · simp only [untilHalt, ht, if_true]554      refine ⟨rfl, fun u hu => ?_⟩555      obtain rfl : u = 0 := by omega556      simpa [arun] using hrun557    · have ht' : t.halted = false := by simpa using ht558      simp only [untilHalt, ht', Bool.false_eq_true, if_false]559      have hs : ostep early B P false { s with rs := t } = { s with rs := rsStep (policyIdx s.j) t } := by560        unfold ostep; simp [hrun, ht']561      obtain ⟨ih1, ih2⟩ := arun_untilHalt early B P s hrun f (rsStep (policyIdx s.j) t)562      refine ⟨by simp only [arun]; rw [hs]; exact ih1, fun u hu => ?_⟩563      rcases u with _ | u564      · simpa [arun] using hrun565      · simp only [arun]; rw [hs]; exact ih2 u (by omega)566567/-- ROLLOUT PHASE: from the board Q freshly loaded for head j, after exactly L + 1 ticks568    (L = rolloutMoves j Q simulated moves, then the terminal test) the embedded registers569    hold the outcome RO_{π_j}(Q) with halt = 1; run stays 1 throughout. -/570theorem roll_phase (early : Bool) (B : Nat) (P : List Nat) (s : OS) (hrun : s.run = true) (Q : List Nat) :571    ∃ Qe, arun early B P (rolloutMoves s.j Q + 1) { s with rs := ⟨Q, false, false⟩ } =572        { s with rs := ⟨Qe, rolloutWinner s.j Q, true⟩ } ∧573      ∀ u, u ≤ rolloutMoves s.j Q + 1 → (arun early B P u { s with rs := ⟨Q, false, false⟩ }).run = true := by574  obtain ⟨h1, h2, h3⟩ := untilHalt_spec s.j (rolloutMoves s.j Q + 1) Q false (Nat.le_refl _)575  obtain ⟨e1, e2⟩ := arun_untilHalt early B P s hrun (rolloutMoves s.j Q + 1) ⟨Q, false, false⟩576  rw [h3] at e1 e2577  refine ⟨(untilHalt (policyIdx s.j) (rolloutMoves s.j Q + 1) ⟨Q, false, false⟩).1.board, ?_, e2⟩578  rw [e1]579  congr 1580  generalize (untilHalt (policyIdx s.j) (rolloutMoves s.j Q + 1) ⟨Q, false, false⟩).1 = t at h1 h2 ⊢581  obtain ⟨bd, pr, hl⟩ := t582  simp only at h1 h2583  rw [h1, h2]; simp584585/-! ## A4. Macro step: one complete query of head j -/586587/-- The controller with the original board freshly loaded for head j. -/588def ld (P : List Nat) (j : Nat) (dec : Bool) (outs : Nat → Bool) : OS := ⟨⟨P, false, false⟩, true, dec, j, outs⟩589590def upd (outs : Nat → Bool) (j : Nat) (o : Bool) : Nat → Bool := fun h => if h = j then o else outs h591592/-- ONE QUERY = L_j + 2 ticks: L_j moves, the terminal test, and one consume tick that593    stores the outcome and then stops or advances to head j+1 with the board reloaded. -/594theorem query_step (early : Bool) (B : Nat) (P : List Nat) (j : Nat) (dec : Bool) (outs : Nat → Bool) :595    ∃ Qe, arun early B P (rolloutMoves j P + 2) (ld P j dec outs) =596        (if ((early && rolloutWinner j P) || decide (j = B - 1)) then597          ⟨⟨Qe, rolloutWinner j P, true⟩, false, dec || rolloutWinner j P, j, upd outs j (rolloutWinner j P)⟩598        else ld P (j + 1) (dec || rolloutWinner j P) (upd outs j (rolloutWinner j P))) ∧599      ∀ u, u ≤ rolloutMoves j P + 1 → (arun early B P u (ld P j dec outs)).run = true := by600  obtain ⟨Qe, h1, h2⟩ := roll_phase early B P (ld P j dec outs) rfl P601  simp only [ld] at h1 h2602  refine ⟨Qe, ?_, fun u hu => by simp only [ld]; exact h2 u hu⟩603  rw [show rolloutMoves j P + 2 = (rolloutMoves j P + 1) + 1 from rfl, arun_add]604  simp only [ld]605  rw [h1, arun_one]606  unfold ostep coreB607  simp only [Bool.true_eq_false, Bool.false_eq_true, if_false, if_true]608  rfl609610/-! ## A4. The early-exit schedule refines Misc.shootout -/611612/-- Ticks used by the early-exit schedule from head j with k + 1 heads left. -/613def eeT (B : Nat) (P : List Nat) : Nat → Nat → Nat614  | 0, j => rolloutMoves j P + 2615  | k + 1, j => if rolloutWinner j P then rolloutMoves j P + 2 else rolloutMoves j P + 2 + eeT B P k (j + 1)616617/-- Rollouts (head queries) executed by the early-exit schedule. -/618def eeR (P : List Nat) : Nat → Nat → Nat619  | 0, _ => 1620  | k + 1, j => if rolloutWinner j P then 1 else eeR P k (j + 1) + 1621622theorem ee_run (B : Nat) (P : List Nat) : ∀ (k j : Nat), j + (k + 1) = B → ∀ outs : Nat → Bool,623    (arun true B P (eeT B P k j) (ld P j false outs)).run = false ∧624    (arun true B P (eeT B P k j) (ld P j false outs)).dec = (List.range' j (k + 1)).any (fun h => rolloutWinner h P) ∧625    (∀ u, u < eeT B P k j → (arun true B P u (ld P j false outs)).run = true) ∧626    (arun true B P (eeT B P k j) (ld P j false outs)).j + 1 = j + eeR P k j627  | 0, j, hj, outs => by628    obtain ⟨Qe, h1, h2⟩ := query_step true B P j false outs629    have hl : decide (j = B - 1) = true := by simp; omega630    rw [hl, Bool.or_true, if_pos rfl] at h1631    simp only [eeT]632    rw [h1]633    refine ⟨rfl, by simp, fun u hu => h2 u (by omega), by simp [eeR]⟩634  | k + 1, j, hj, outs => by635    obtain ⟨Qe, h1, h2⟩ := query_step true B P j false outs636    have hl : decide (j = B - 1) = false := by simp; omega637    rw [hl, Bool.or_false] at h1638    simp only [eeT]639    cases ho : rolloutWinner j P640    · have h1' : arun true B P (rolloutMoves j P + 2) (ld P j false outs) = ld P (j + 1) false (upd outs j false) := by641        rw [h1, ho]; rfl642      rw [if_neg (by simp), arun_add, h1']643      obtain ⟨i1, i2, i3, i4⟩ := ee_run B P k (j + 1) (by omega) (upd outs j false)644      have hd : (List.range' (j + 1) (k + 1)).any (fun h => rolloutWinner h P) =645          (List.range' j (k + 1 + 1)).any (fun h => rolloutWinner h P) := by646        rw [show List.range' j (k + 1 + 1) = j :: List.range' (j + 1) (k + 1) from List.range'_succ,647          List.any_cons, ho, Bool.false_or]648      refine ⟨i1, by rw [i2, hd], fun u hu => ?_, by simp only [eeR, ho, Bool.false_eq_true, if_false]; omega⟩649      by_cases hu' : u ≤ rolloutMoves j P + 1650      · exact h2 u hu'651      · obtain ⟨v, rfl⟩ : ∃ v, u = (rolloutMoves j P + 2) + v := ⟨u - (rolloutMoves j P + 2), by omega⟩652        rw [arun_add, h1']; exact i3 v (by omega)653    · have h1' : arun true B P (rolloutMoves j P + 2) (ld P j false outs) =654          ⟨⟨Qe, true, true⟩, false, true, j, upd outs j true⟩ := by655        rw [h1, ho]; rfl656      rw [if_pos rfl, h1']657      refine ⟨rfl, ?_, fun u hu => h2 u (by omega), by simp [eeR, ho]⟩658      show true = _659      rw [List.range'_succ, List.any_cons, ho, Bool.true_or]660661/-- REFINEMENT TO Misc.shootout: the number of head queries of the binary controller is662    the query count of the abstract FSM, and the decision is the FSM's decision. -/663theorem eeR_shootout (B : Nat) (P : List Nat) : ∀ (k j : Nat), j + (k + 1) = B →664    eeR P k j = ((Misc.shootout B).run (fun h => rolloutWinner h P) (k + 2) j).2665  | 0, j, hj => by666    rw [Misc.run_query _ (by omega)]667    cases ho : rolloutWinner j P668    · simp only [Bool.false_eq_true, if_false]669      rw [if_neg (show ¬ j + 1 < B by omega), Misc.run_no]; rfl670    · simp only [if_true]; rw [Misc.run_yes]; rfl671  | k + 1, j, hj => by672    rw [Misc.run_query _ (by omega)]673    simp only [eeR]674    cases ho : rolloutWinner j P675    · simp only [Bool.false_eq_true, if_false]676      rw [if_pos (show j + 1 < B by omega), ← eeR_shootout B P k (j + 1) (by omega)]677    · simp only [if_true]; rw [Misc.run_yes]678679theorem eeR_le (P : List Nat) : ∀ k j, eeR P k j ≤ k + 1680  | 0, _ => by simp [eeR]681  | k + 1, j => by682    simp only [eeR]; have := eeR_le P k (j + 1); split <;> omega683684/-- EXACT TICK COUNT: the early-exit schedule uses Σ (L_h + 2) over the queried heads. -/685theorem eeT_sum (B : Nat) (P : List Nat) : ∀ k j,686    eeT B P k j = ((List.range' j (eeR P k j)).map (fun h => rolloutMoves h P + 2)).sum687  | 0, j => by simp [eeT, eeR]688  | k + 1, j => by689    simp only [eeT, eeR]690    cases rolloutWinner j P691    · simp only [Bool.false_eq_true, if_false]692      rw [List.range'_succ, List.map_cons, List.sum_cons, eeT_sum B P k (j + 1)]693    · simp694695theorem eeT_le (B : Nat) {P : List Nat} (hw : Width B P) : ∀ k j, eeT B P k j ≤ (k + 1) * (clockBound B P.length + 1)696  | 0, j => by have := clock_ok (j := j) hw; simp only [eeT]; omega697  | k + 1, j => by698    have := clock_ok (j := j) hw699    have ih := eeT_le B hw k (j + 1)700    simp only [eeT]; split701    · have : clockBound B P.length + 1 ≤ (k + 1 + 1) * (clockBound B P.length + 1) :=702        Nat.le_mul_of_pos_left _ (by omega)703      omega704    · rw [Nat.succ_mul]; omega705706/-- The fixed padded clock (ticks after the reset tick): B·(N(2^B − 1) + 2). -/707def Tmax (B N : Nat) : Nat := B * (clockBound B N + 1)708709/-- EARLY-EXIT SEMANTIC THEOREM (B ≥ 1): after the reset, the controller stops after exactly710    T = eeT ticks (running at every earlier tick), with decision dec = [nim(P) ≠ 0]; the711    decision and the number of queries are those of Misc.shootout run on the actual712    rollout outcomes; T ≤ Tmax. -/713theorem ee_spec {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :714    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).run = false ∧715    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).dec = decide (nimSum P ≠ 0) ∧716    (∀ u, u < eeT B P (B - 1) 0 → (arun true B P u (initOS B P)).run = true) ∧717    some (arun true B P (eeT B P (B - 1) 0) (initOS B P)).dec =718      ((Misc.shootout B).run (fun h => rolloutWinner h P) (B + 1) 0).1 ∧719    eeR P (B - 1) 0 = ((Misc.shootout B).run (fun h => rolloutWinner h P) (B + 1) 0).2 ∧720    eeR P (B - 1) 0 ≤ B ∧ eeT B P (B - 1) 0 ≤ Tmax B P.length ∧721    (arun true B P (eeT B P (B - 1) 0) (initOS B P)).j + 1 = eeR P (B - 1) 0 := by722  have hinit : initOS B P = ld P 0 false (fun _ => false) := by723    simp [initOS, ld]; omega724  rw [hinit]725  obtain ⟨h1, h2, h3, h4⟩ := ee_run B P (B - 1) 0 (by omega) (fun _ => false)726  have hsh := Misc.shootout_from (B := B) (fun h => rolloutWinner h P) (B - 1) 0 (by omega)727  rw [show B - 1 + 2 = B + 1 by omega] at hsh728  have hR := eeR_shootout B P (B - 1) 0 (by omega)729  rw [show B - 1 + 2 = B + 1 by omega] at hR730  refine ⟨h1, ?_, h3, ?_, hR, by have := eeR_le P (B - 1) 0; omega, ?_, by rw [h4]; omega⟩731  · rw [h2, show B - 1 + 1 = B by omega, ← List.range_eq_range']; exact Misc.channels_or hB hw732  · rw [hsh, h2]733  · have := eeT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega] at this; exact this734735/-! ## A3/A4. The bit-level early-exit implementation -/736737/-- THE IMPLEMENTATION: one reset tick from arbitrary register bits x₀, then T clocked738    ticks of the update formulas (input: registers, reset bit 0, the board P). -/739def impl (early : Bool) (B N r : Nat) (P : List Nat) (T : Nat) (x0 : Nat → Bool) : Nat → Bool :=740  brun early B N r P T (cstep early B N r P true x0)741742theorem impl_enc (early : Bool) {B N r : Nat} (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N)743    (hwP : Width B P) (T : Nat) (x0 : Nat → Bool) :744    impl early B N r P T x0 = enc B N r (arun early B P T (initOS B P)) := by745  unfold impl; rw [cstep_reset]; exact (brun_enc early hBr hP hwP T _ (initOS_valid hP hwP)).1746747theorem nimSum_width0 {P : List Nat} (hw : Width 0 P) : nimSum P = 0 := by748  have := nimSum_lt hw; simp at this; exact this749750/-- EARLY-EXIT CLASSIFIER, BIT LEVEL: for every B (B = 0 by the stated convention), every751    board of N heaps of width B, every initial register content and every clock752    T ≥ eeT (in particular the fixed padded clock Tmax B N), the dec wire holds753    [nim(P) ≠ 0] and the run wire is 0. -/754theorem ee_impl (B N r : Nat) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)755    (x0 : Nat → Bool) (T : Nat) (hT : 1 ≤ B → eeT B P (B - 1) 0 ≤ T) :756    impl true B N r P T x0 (B * N + 3) = decide (nimSum P ≠ 0) ∧ impl true B N r P T x0 (B * N + 2) = false := by757  rw [impl_enc true hBr hP hw, enc_dec, enc_run]758  rcases Nat.eq_zero_or_pos B with hB | hB759  · subst hB760    have hrun : (initOS 0 P).run = false := by simp [initOS]761    rw [arun_hold true 0 P _ hrun]762    simp [initOS, nimSum_width0 hw]763  · obtain ⟨h1, h2, _⟩ := ee_spec hB hw764    obtain ⟨d, rfl⟩ : ∃ d, T = eeT B P (B - 1) 0 + d := ⟨T - eeT B P (B - 1) 0, by have := hT hB; omega⟩765    rw [arun_add, arun_hold true B P _ h1]766    exact ⟨h2, h1⟩767768/-- The padded clock suffices. -/769theorem ee_impl_padded (B N r : Nat) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)770    (x0 : Nat → Bool) :771    impl true B N r P (Tmax B N) x0 (B * N + 3) = decide (nimSum P ≠ 0) :=772  (ee_impl B N r hBr hP hw x0 (Tmax B N) (fun hB => by have := (ee_spec hB hw).2.2.2.2.2.2.1; rwa [hP] at this)).1773774/-! ## Early stopping: a halting loop on the run wire, with exact tick count -/775776/-- Clock the update while the run wire is 1 (fuel f); returns the registers and the number777    of ticks executed. -/778def loopRun (step : (Nat → Bool) → (Nat → Bool)) (hw : Nat) : Nat → (Nat → Bool) → (Nat → Bool) × Nat779  | 0, x => (x, 0)780  | f + 1, x => if x hw = true then ((loopRun step hw f (step x)).1, (loopRun step hw f (step x)).2 + 1) else (x, 0)781782theorem loopRun_spec (early : Bool) {B N r : Nat} (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N)783    (hwP : Width B P) : ∀ (T f : Nat) (s : OS), Valid B N r s → T ≤ f →784    (∀ u, u < T → (arun early B P u s).run = true) → (arun early B P T s).run = false →785    loopRun (cstep early B N r P false) (B * N + 2) f (enc B N r s) = (enc B N r (arun early B P T s), T)786  | 0, f, s, hv, _, _, hstop => by787    cases f with788    | zero => rfl789    | succ f => simp only [loopRun, enc_run]; simp only [arun] at hstop; simp [hstop, arun]790  | T + 1, f, s, hv, hTf, hrun, hstop => by791    obtain ⟨f, rfl⟩ : ∃ f', f = f' + 1 := ⟨f - 1, by omega⟩792    have h0 : s.run = true := by simpa [arun] using hrun 0 (by omega)793    simp only [loopRun, enc_run, h0, if_true]794    rw [cstep_enc early hBr hP hv]795    have ih := loopRun_spec early hBr hP hwP T f (ostep early B P false s) (ostep_valid early hBr hP hwP hv) (by omega)796      (fun u hu => hrun (u + 1) (by omega)) hstop797    rw [ih]; rfl798799/-- EARLY STOPPING, BIT LEVEL: the halting loop on the run wire stops after exactly800    1 (reset) + eeT ticks, Σ over the queried heads of (L_h + 2), with the decision on the801    dec wire.  (The padded clock instead always runs Tmax ticks; both give the same802    registers, ostep_hold.) -/803theorem ee_loop {B N r : Nat} (hB : 1 ≤ B) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)804    (x0 : Nat → Bool) :805    (loopRun (cstep true B N r P false) (B * N + 2) (Tmax B N) (cstep true B N r P true x0)).2 = eeT B P (B - 1) 0 ∧806    (loopRun (cstep true B N r P false) (B * N + 2) (Tmax B N) (cstep true B N r P true x0)).1 (B * N + 3) =807      decide (nimSum P ≠ 0) := by808  obtain ⟨h1, h2, h3, _, _, _, h7, _⟩ := ee_spec hB hw809  rw [cstep_reset, loopRun_spec true hBr hP hw _ _ _ (initOS_valid hP hw) (by rw [← hP]; exact h7) h3 h1]810  exact ⟨rfl, by show enc B N r _ (B * N + 3) = _; rw [enc_dec, h2]⟩811812/-! ## A5. All heads retained, then the existing readout: the move path -/813814/-- Ticks of the all-head schedule from head j with k + 1 heads left. -/815def ahT (P : List Nat) : Nat → Nat → Nat816  | 0, j => rolloutMoves j P + 2817  | k + 1, j => rolloutMoves j P + 2 + ahT P k (j + 1)818819theorem ah_run (B : Nat) (P : List Nat) : ∀ (k j : Nat), j + (k + 1) = B → ∀ (dec : Bool) (outs : Nat → Bool),820    (∀ h, h < j → outs h = rolloutWinner h P) →821    (arun false B P (ahT P k j) (ld P j dec outs)).run = false ∧822    (∀ h, h < B → (arun false B P (ahT P k j) (ld P j dec outs)).outs h = rolloutWinner h P) ∧823    (∀ u, u < ahT P k j → (arun false B P u (ld P j dec outs)).run = true)824  | 0, j, hj, dec, outs, ho => by825    obtain ⟨Qe, h1, h2⟩ := query_step false B P j dec outs826    have hl : decide (j = B - 1) = true := by simp; omega827    rw [Bool.false_and, Bool.false_or, hl, if_pos rfl] at h1828    simp only [ahT]; rw [h1]829    refine ⟨rfl, fun h hh => ?_, fun u hu => h2 u (by omega)⟩830    simp only [upd]; split831    · subst_vars; rfl832    · exact ho h (by omega)833  | k + 1, j, hj, dec, outs, ho => by834    obtain ⟨Qe, h1, h2⟩ := query_step false B P j dec outs835    have hl : decide (j = B - 1) = false := by simp; omega836    rw [Bool.false_and, Bool.false_or, hl, if_neg (by simp)] at h1837    simp only [ahT]838    rw [arun_add, h1]839    have ho' : ∀ h, h < j + 1 → upd outs j (rolloutWinner j P) h = rolloutWinner h P := by840      intro h hh; simp only [upd]; split841      · subst_vars; rfl842      · exact ho h (by omega)843    obtain ⟨i1, i2, i3⟩ := ah_run B P k (j + 1) (by omega) _ _ ho'844    refine ⟨i1, i2, fun u hu => ?_⟩845    by_cases hu' : u ≤ rolloutMoves j P + 1846    · exact h2 u hu'847    · obtain ⟨v, rfl⟩ : ∃ v, u = (rolloutMoves j P + 2) + v := ⟨u - (rolloutMoves j P + 2), by omega⟩848      rw [arun_add, h1]; exact i3 v (by omega)849850theorem ahT_sum (P : List Nat) : ∀ k j, ahT P k j = ((List.range' j (k + 1)).map (fun h => rolloutMoves h P)).sum + 2 * (k + 1)851  | 0, j => by simp [ahT]852  | k + 1, j => by853    rw [ahT, ahT_sum P k (j + 1), show List.range' j (k + 1 + 1) = j :: List.range' (j + 1) (k + 1) from List.range'_succ]854    simp only [List.map_cons, List.sum_cons]; omega855856/-- ALL-HEAD TICKS: exactly totalRolloutMoves + 2B ticks after the reset. -/857theorem ahT_total {B : Nat} (hB : 1 ≤ B) (P : List Nat) : ahT P (B - 1) 0 = totalRolloutMoves B P + 2 * B := by858  rw [ahT_sum, totalRolloutMoves, List.range_eq_range', show B - 1 + 1 = B by omega]859860theorem ahT_le (B : Nat) {P : List Nat} (hw : Width B P) : ∀ k j, ahT P k j ≤ (k + 1) * (clockBound B P.length + 1)861  | 0, j => by have := clock_ok (j := j) hw; simp only [ahT]; omega862  | k + 1, j => by863    have := clock_ok (j := j) hw; have := ahT_le B hw k (j + 1)864    simp only [ahT]; rw [Nat.succ_mul]; omega865866theorem reconstruct_congr {B : Nat} {o1 o2 : Nat → Bool} (h : ∀ j, j < B → o1 j = o2 j) :867    reconstruct B o1 = reconstruct B o2 := by868  unfold reconstruct869  have key : ∀ k, k ≤ B → ofBits k (recoverBit o1) = ofBits k (recoverBit o2) := by870    intro k871    induction k with872    | zero => intro _; rfl873    | succ k ih =>874      intro hk875      simp only [ofBits]876      rw [ih (by omega)]877      congr 2878      unfold recoverBit879      split880      · rw [h 0 (by omega)]881      · rw [h k (by omega), h 0 (by omega)]882  exact key B (Nat.le_refl _)883884/-- The all-head move: run the all-head schedule on the padded clock from a reset, then885    evaluate the EXISTING readout network on the board and the stored outcome bits. -/886def ahMove (B : Nat) (P : List Nat) : Option (Nat × Nat) :=887  netBinSem (mhN (B, P.length)) P.length (rIdx P.length) B888    (obsIn B P.length P (fun h => impl false B P.length (rIdx B) P (Tmax B P.length) (fun _ => false) (oW B P.length (rIdx B) h)))889890def ahSel (B : Nat) (P : List Nat) : Option (List Nat) := applyM P (ahMove B P)891892/-- IMPLEMENTATION EQUALITY: the binary outer controller with retained outcomes followed by893    the readout network computes exactly mhExec (hence decisionMove). -/894theorem ahMove_eq {B : Nat} {P : List Nat} (hw : Width B P) : ahMove B P = mhExec B P := by895  have hBr : B ≤ 2 ^ rIdx B := Nat.le_of_lt (rIdx_counter B)896  unfold ahMove mhExec897  rw [(mh_semantics rfl hw _).2.1]898  show attainT _ P = netBinSem (mhN (B, P.length)) P.length (rIdx P.length) B _899  rw [(mh_semantics rfl hw _).2.1]900  congr 1901  apply reconstruct_congr902  intro h hh903  rw [outBit_eq hw, impl_enc false hBr rfl hw]904  have hB : 1 ≤ B := by omega905  obtain ⟨h1, h2, _⟩ := ah_run B P (B - 1) 0 (by omega) false (fun _ => false) (fun h hh => by omega)906  have hinit : initOS B P = ld P 0 false (fun _ => false) := by simp [initOS, ld]; omega907  have hle : ahT P (B - 1) 0 ≤ Tmax B P.length := by908    have := ahT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega] at this; exact this909  obtain ⟨d, hd⟩ : ∃ d, Tmax B P.length = ahT P (B - 1) 0 + d := ⟨Tmax B P.length - ahT P (B - 1) 0, by omega⟩910  rw [hd, hinit, arun_add, arun_hold false B P _ h1, enc_o _ _ _ _ hh, h2 h hh]911912/-- WINNING: the implemented all-head controller plus readout wins from every nonzero913    position against every legal opponent (reusing the whole-game theorem mhExec_wins). -/914theorem ahSel_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (ahSel B) P :=915  wins_congr (fun Q hQ => by unfold ahSel mhExecSel; rw [ahMove_eq hQ]) hw (mhExec_wins hw h)916917/-- EARLY EXIT DOES NOT SUPPLY THE MOVE: for B = 2 and P = (1), the early-exit schedule stops918    after head 0 (outcome 1) with stored bit o₁ = 0, whereas RO_{π₁}(P) = 1; so its stored919    bits are not the readout's input.  Winning-move selection needs the all-head path. -/920theorem early_exit_not_move :921    rolloutWinner 0 [1] = true ∧ rolloutWinner 1 [1] = true ∧922    ∃ s', arun true 2 [1] (rolloutMoves 0 [1] + 2) (initOS 2 [1]) = s' ∧ s'.run = false ∧ s'.outs 1 = false := by923  have h0 : rolloutWinner 0 [1] = true := by rw [rolloutWinner_channel]; decide924  have h1 : rolloutWinner 1 [1] = true := by rw [rolloutWinner_channel]; decide925  refine ⟨h0, h1, ?_⟩926  obtain ⟨Qe, e1, _⟩ := query_step true 2 [1] 0 false (fun _ => false)927  have hinit : initOS 2 [1] = ld [1] 0 false (fun _ => false) := rfl928  rw [h0] at e1929  refine ⟨_, rfl, ?_⟩930  rw [hinit, e1]931  simp [upd]932933/-! ## A2. The compiled fixed-scale network: same formulas -/934935def cNet (early : Bool) (B N r : Nat) : List Layer := compileF (cForms early B N r)936937/-- One tick of the threshold network (registers = its first SW outputs). -/938def nstep (early : Bool) (B N r : Nat) (P : List Nat) (rst : Bool) (x : Nat → Bool) : Nat → Bool := fun w =>939  if w < SW B N r then evalNet (cNet early B N r) (zIn B N r x rst P) w else false940941theorem nstep_eq (early : Bool) (B N r : Nat) (P : List Nat) (rst : Bool) (x : Nat → Bool) :942    nstep early B N r P rst x = cstep early B N r P rst x := by943  funext w944  unfold nstep cstep cNet945  by_cases hw : w < SW B N r946  · rw [if_pos hw, if_pos hw, compileF_eval _ _ (by rw [cForms_length]; exact hw),947      List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by rw [cForms_length]; exact hw)]948    rfl949  · rw [if_neg hw, if_neg hw]950951/-- Network implementation: reset tick, then T network ticks. -/952def nrun (early : Bool) (B N r : Nat) (P : List Nat) : Nat → (Nat → Bool) → (Nat → Bool)953  | 0, x => x954  | k + 1, x => nrun early B N r P k (nstep early B N r P false x)955956def nimpl (early : Bool) (B N r : Nat) (P : List Nat) (T : Nat) (x0 : Nat → Bool) : Nat → Bool :=957  nrun early B N r P T (nstep early B N r P true x0)958959theorem nimpl_eq (early : Bool) (B N r : Nat) (P : List Nat) (T : Nat) (x0 : Nat → Bool) :960    nimpl early B N r P T x0 = impl early B N r P T x0 := by961  unfold nimpl impl962  rw [nstep_eq]963  generalize cstep early B N r P true x0 = x964  induction T generalizing x with965  | zero => rfl966  | succ T ih => simp only [nrun, brun]; rw [nstep_eq]; exact ih _967968/-- THE NETWORK-EXECUTED CLASSIFIER and MOVE: the same theorems hold for the threshold969    network implementation. -/970theorem ee_net (B N r : Nat) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) (x0 : Nat → Bool) :971    nimpl true B N r P (Tmax B N) x0 (B * N + 3) = decide (nimSum P ≠ 0) := by972  rw [nimpl_eq]; exact ee_impl_padded B N r hBr hP hw x0973974/-! ## A2. Resources of the update formulas -/975976def R3 (d s m : Nat) (c : Circ) : Prop := depth c ≤ d ∧ size c ≤ s ∧ maxInput c ≤ m977978theorem and_res {cs : List Circ} {d s m : Nat} (h : ∀ c ∈ cs, R3 d s m c) : R3 (d + 1) (cs.length * s + 1) m (and cs) :=979  ⟨depth_and_le (fun c hc => (h c hc).1), ControllerBits.size_and_le' (fun c hc => (h c hc).2.1),980    ControllerBits.maxInput_and_le (fun c hc => (h c hc).2.2)⟩981982theorem or_res {cs : List Circ} {d s m : Nat} (h : ∀ c ∈ cs, R3 d s m c) : R3 (d + 1) (cs.length * s + 1) m (or cs) :=983  ⟨depth_or_le (fun c hc => (h c hc).1), ControllerBits.size_or_le' (fun c hc => (h c hc).2.1),984    ControllerBits.maxInput_or_le (fun c hc => (h c hc).2.2)⟩985986theorem R3_mono {d s m d' s' m' : Nat} {c : Circ} (h : R3 d s m c) (hd : d ≤ d') (hs : s ≤ s') (hm : m ≤ m') :987    R3 d' s' m' c := ⟨by have := h.1; omega, by have := h.2.1; omega, by have := h.2.2; omega⟩988989theorem not_res {c : Circ} {d s m : Nat} (h : R3 d s m c) : R3 (d + 1) (s + 1) m (not c) := by990  refine ⟨?_, ?_, ?_⟩ <;> simp only [depth_not, size_not, maxInput_not] <;> have := h.1 <;> have := h.2.1 <;>991    have := h.2.2 <;> omega992993theorem inp3 {i m : Nat} (h : i + 1 ≤ m) : R3 0 1 m (input i) := BoardStore.inp_res h994theorem cst3 (b : Bool) (m : Nat) : R3 0 1 m (const b) := by refine ⟨?_, ?_, ?_⟩ <;> simp995996theorem mux3 {c a b : Circ} {dc sc mc da sa ma db sb mb : Nat} (hc : R3 dc sc mc c) (ha : R3 da sa ma a)997    (hb : R3 db sb mb b) : R3 (max (dc + 1) (max da db) + 2) (2 * sc + sa + sb + 4) (max mc (max ma mb))998      (RolloutExec.mux c a b) := BoardStore.mux_res hc ha hb9991000/-- Size bound of one rollout-step formula of head h (from the certified policy circuit). -/1001def S1 (B N : Nat) : Nat := stepZ (rIdx N) N (polSz B N)10021003theorem S1_pos (B N : Nat) : 1 ≤ S1 B N := by unfold S1 stepZ; omega10041005theorem hstep_res (B N h w : Nat) : R3 28 (S1 B N) (B * N + 2) (hstep B N h w) := by1006  unfold hstep1007  have hleaf : ∀ i, IsLeaf (σR B N i) := fun i => by unfold σR; split <;> trivial1008  have hc : R3 28 (S1 B N) (2 * (B * N) + 3) ((stepForms B N (polBin B N h (rIdx N))).getD w (const false)) := by1009    rw [List.getD_eq_getElem?_getD]1010    cases hg : (stepForms B N (polBin B N h (rIdx N)))[w]? with1011    | none => simp only [Option.getD_none]; exact ⟨by simp, by simp; exact S1_pos B N, by simp⟩1012    | some c => exact stepForms_res (polBin_bound (j := h) (rIdx_width N)) c (List.mem_of_getElem? hg)1013  refine ⟨by rw [depth_subst_leaf _ hleaf]; exact hc.1, by rw [size_subst_leaf _ hleaf]; exact hc.2.1, ?_⟩1014  apply maxInput_subst_le1015  intro i; unfold σR; split1016  · simp; omega1017  · simp10181019theorem isH_res (B N r h : Nat) : R3 2 (2 * r + 1) (B * N + 4 + r) (isH B N r h) := by1020  have := and_res (cs := (List.range r).map (jlit B N h)) (d := 1) (s := 2) (m := B * N + 4 + r) (by1021    intro c hc; obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc1022    have hq' := List.mem_range.mp hq1023    unfold jlit jW; split1024    · exact R3_mono (inp3 (by omega)) (by omega) (by omega) (Nat.le_refl _)1025    · exact not_res (inp3 (by omega)))1026  simp only [List.length_map, List.length_range] at this1027  exact R3_mono this (Nat.le_refl _) (by omega) (Nat.le_refl _)10281029/-- Every update formula has depth ≤ 34, size ≤ Fz and reads only the IW input wires. -/1030def Fz (B N r : Nat) : Nat := B * (2 * (2 * r + 1 + S1 B N) + 1) + 1 + 32 * r + 6010311032theorem mstep_res (B N r w : Nat) : R3 30 (B * (2 * (2 * r + 1 + S1 B N) + 1) + 1) (IW B N r) (mstep B N r w) := by1033  have := or_res (cs := (List.range B).map (fun h => and [isH B N r h, hstep B N h w])) (d := 29)1034    (s := 2 * (2 * r + 1 + S1 B N) + 1) (m := IW B N r) (by1035      intro c hc; obtain ⟨h, _, rfl⟩ := List.mem_map.mp hc1036      have := and_res (cs := [isH B N r h, hstep B N h w]) (d := 28) (s := 2 * r + 1 + S1 B N) (m := IW B N r) (by1037        intro c hc1038        simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1039        rcases hc with rfl | rfl1040        · exact R3_mono (isH_res B N r h) (by omega) (by omega) (by unfold IW SW; omega)1041        · exact R3_mono (hstep_res B N h w) (Nat.le_refl _) (by omega) (by unfold IW SW; omega))1042      simpa using this)1043  simpa using this10441045theorem cForms_res (early : Bool) (B N r : Nat) :1046    ∀ c ∈ cForms early B N r, R3 34 (Fz B N r) (IW B N r) c := by1047  have hM : ∀ i, i < SW B N r → R3 0 1 (IW B N r) (input i) := fun i hi => inp3 (by unfold IW; omega)1048  have hpar := hM (B * N) (by unfold SW; omega)1049  have hhalt := hM (B * N + 1) (by unfold SW; omega)1050  have hrun := hM (B * N + 2) (by unfold SW; omega)1051  have hdec := hM (B * N + 3) (by unfold SW; omega)1052  have hrst : R3 0 1 (IW B N r) (rstI B N r) := inp3 (by unfold IW; omega)1053  have hisH : ∀ h, R3 2 (2 * r + 1) (IW B N r) (isH B N r h) :=1054    fun h => R3_mono (isH_res B N r h) (Nat.le_refl _) (Nat.le_refl _) (by unfold IW SW; omega)1055  have hcons : R3 1 3 (IW B N r) (consC B N) := by1056    have := and_res (cs := [runI B N, haltI B N]) (by1057      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1058      rcases hc with rfl | rfl <;> assumption)1059    simpa using this1060  have hstepC : R3 2 5 (IW B N r) (stepC B N) := by1061    have := and_res (cs := [runI B N, not (haltI B N)]) (d := 1) (s := 2) (by1062      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1063      rcases hc with rfl | rfl1064      · exact R3_mono hrun (by omega) (by omega) (Nat.le_refl _)1065      · exact not_res hhalt)1066    simpa using this1067  have hcore : R3 3 (4 * r + 3) (IW B N r) (coreC early B N r) := by1068    unfold coreC lastC; cases early1069    · exact R3_mono (hisH _) (by omega) (by omega) (Nat.le_refl _)1070    · have := or_res (cs := [parI B N, isH B N r (B - 1)]) (d := 2) (s := 2 * r + 1) (by1071        intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1072        rcases hc with rfl | rfl1073        · exact R3_mono hpar (by omega) (by omega) (Nat.le_refl _)1074        · exact hisH _)1075      simp only [if_true, List.length_cons, List.length_nil] at this ⊢1076      exact R3_mono this (Nat.le_refl _) (by omega) (Nat.le_refl _)1077  have hcont : R3 5 (8 * r + 9) (IW B N r) (contC early B N r) := by1078    have := and_res (cs := [consC B N, not (coreC early B N r)]) (d := 4) (s := 4 * r + 4) (by1079      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1080      rcases hc with rfl | rfl1081      · exact R3_mono hcons (by omega) (by omega) (Nat.le_refl _)1082      · exact not_res hcore)1083    simp only [List.length_cons, List.length_nil] at this1084    exact R3_mono this (Nat.le_refl _) (by omega) (Nat.le_refl _)1085  have hload : R3 6 (16 * r + 19) (IW B N r) (loadC early B N r) := by1086    have := or_res (cs := [rstI B N r, contC early B N r]) (d := 5) (s := 8 * r + 9) (by1087      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1088      rcases hc with rfl | rfl1089      · exact R3_mono hrst (by omega) (by omega) (Nat.le_refl _)1090      · exact hcont)1091    simp only [List.length_cons, List.length_nil] at this1092    exact R3_mono this (Nat.le_refl _) (by omega) (Nat.le_refl _)1093  have hstop : R3 4 (8 * r + 7) (IW B N r) (stopC early B N r) := by1094    have := and_res (cs := [consC B N, coreC early B N r]) (d := 3) (s := 4 * r + 3) (by1095      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1096      rcases hc with rfl | rfl1097      · exact R3_mono hcons (by omega) (by omega) (Nat.le_refl _)1098      · exact hcore)1099    simp only [List.length_cons, List.length_nil] at this1100    exact R3_mono this (Nat.le_refl _) (by omega) (Nat.le_refl _)1101  have hms := fun w => mstep_res B N r w1102  -- the three rollout-register formulas1103  have hreg : ∀ (a : Circ) (w : Nat), R3 0 1 (IW B N r) a → w < SW B N r →1104      R3 34 (Fz B N r) (IW B N r) (RolloutExec.mux (loadC early B N r) a (RolloutExec.mux (stepC B N) (mstep B N r w) (input w))) := by1105    intro a w ha hw1106    have inner := mux3 hstepC (hms w) (hM w hw)1107    have outer := mux3 hload ha inner1108    exact R3_mono outer (by omega) (by unfold Fz; omega) (by omega)1109  intro c hc1110  unfold cForms at hc1111  simp only [List.mem_append, List.mem_map, List.mem_range, List.mem_cons, List.mem_nil_iff, or_false] at hc1112  rcases hc with ⟨w, hw, rfl⟩ | (rfl | rfl | rfl | rfl) | ⟨q, hq, rfl⟩ | ⟨h, hh, rfl⟩1113  · exact hreg _ w (inp3 (by unfold IW; omega)) (by unfold SW; omega)1114  · exact hreg _ (B * N) (cst3 false (IW B N r)) (by unfold SW; omega)1115  · exact hreg _ (B * N + 1) (cst3 false (IW B N r)) (by unfold SW; omega)1116  · have h1 := and_res (cs := [runI B N, not (stopC early B N r)]) (d := 5) (s := 8 * r + 8) (by1117      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1118      rcases hc with rfl | rfl1119      · exact R3_mono hrun (by omega) (by omega) (Nat.le_refl _)1120      · exact not_res hstop)1121    simp only [List.length_cons, List.length_nil] at h11122    have := mux3 hrst (R3_mono (cst3 (decide (1 ≤ B)) (IW B N r)) (Nat.le_refl _) (Nat.le_refl _) (Nat.le_refl _)) h11123    exact R3_mono this (by omega) (by unfold Fz; omega) (by omega)1124  · have h1 := and_res (cs := [consC B N, parI B N]) (d := 1) (s := 3) (by1125      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1126      rcases hc with rfl | rfl1127      · exact hcons1128      · exact R3_mono hpar (by omega) (by omega) (Nat.le_refl _))1129    have h2 := or_res (cs := [decI B N, and [consC B N, parI B N]]) (d := 2) (s := 7) (by1130      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1131      rcases hc with rfl | rfl1132      · exact R3_mono hdec (by omega) (by omega) (Nat.le_refl _)1133      · simpa using h1)1134    simp only [List.length_cons, List.length_nil] at h21135    have := mux3 hrst (cst3 false (IW B N r)) h21136    exact R3_mono this (by omega) (by unfold Fz; omega) (by omega)1137  · have hinc : R3 4 (2 * r + 9) (IW B N r) (incB B N q) := by1138      have ha := and_res (cs := (List.range q).map (fun t => input (jW B N t))) (d := 0) (s := 1) (m := IW B N r) (by1139        intro c hc; obtain ⟨t, ht, rfl⟩ := List.mem_map.mp hc1140        have := List.mem_range.mp ht1141        exact inp3 (by unfold jW IW SW; omega))1142      simp only [List.length_map, List.length_range] at ha1143      have := BoardStore.xor2_res' (inp3 (m := IW B N r) (i := jW B N q) (by unfold jW IW SW; omega)) ha1144      exact R3_mono this (by omega) (by omega) (by omega)1145    have inner := mux3 hcont hinc (inp3 (m := IW B N r) (i := jW B N q) (by unfold jW IW SW; omega))1146    have := mux3 hrst (cst3 false (IW B N r)) inner1147    exact R3_mono this (by omega) (by unfold Fz; omega) (by omega)1148  · have hc1 := and_res (cs := [consC B N, isH B N r h]) (d := 2) (s := 2 * r + 3) (by1149      intro c hc; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc1150      rcases hc with rfl | rfl1151      · exact R3_mono hcons (by omega) (by omega) (Nat.le_refl _)1152      · exact R3_mono (hisH h) (Nat.le_refl _) (by omega) (Nat.le_refl _))1153    simp only [List.length_cons, List.length_nil] at hc11154    have inner := mux3 hc1 hpar (inp3 (m := IW B N r) (i := oW B N r h) (by unfold oW IW SW; omega))1155    have := mux3 hrst (cst3 false (IW B N r)) inner1156    exact R3_mono this (by omega) (by unfold Fz; omega) (by omega)11571158/-! ## A2. Family certificates over (B, N), index width r = rIdx B -/11591160/-- Input width of one update of the (B, N) controller (registers, reset, board). -/1161def shLen (i : Nat × Nat) : Nat := IW i.1 i.2 (rIdx i.1)1162def shF (early : Bool) (i : Nat × Nat) : List Circ := cForms early i.1 i.2 (rIdx i.1)1163def shN (early : Bool) (i : Nat × Nat) : List Layer := cNet early i.1 i.2 (rIdx i.1)11641165/-- Leaves: 0 ↦ B, 1 ↦ N, 2 ↦ rIdx N, 3 ↦ r = rIdx B. -/1166def leafS : Nat → Nat × Nat → Nat1167  | 0, i => i.11168  | 1, i => i.21169  | 2, i => rIdx i.21170  | _, i => rIdx i.111711172def vRB {ι : Type} : PE ι := PE.v 311731174theorem shLen_pos (i : Nat × Nat) (_hi : restAdm i) : 1 ≤ shLen i := by unfold shLen IW SW; omega11751176theorem sh_leaves (k : Nat) (i : Nat × Nat) (hi : restAdm i) : leafS k i ≤ shLen i := by1177  have hB := Nat.mul_le_mul_left i.1 hi.21178  have hN := Nat.mul_le_mul_right i.2 hi.11179  have hr := rIdx_le hi.21180  unfold shLen IW SW1181  match k with1182  | 0 => show i.1 ≤ _; omega1183  | 1 => show i.2 ≤ _; simp at hN; omega1184  | 2 => show rIdx i.2 ≤ _; simp at hN; omega1185  | _ + 3 => show rIdx i.1 ≤ _; omega11861187theorem shF_tsize (early : Bool) (i : Nat × Nat) :1188    tsize (shF early i) ≤ SW i.1 i.2 (rIdx i.1) * Fz i.1 i.2 (rIdx i.1) := by1189  have h := sum_le_len_mul (cs := shF early i) (S := Fz i.1 i.2 (rIdx i.1))1190    (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.1)1191  unfold shF at h ⊢; rw [cForms_length] at h; exact h11921193def shSizeE {ι : Type} : PE ι :=1194  (vB * vN + 4 + vRB + vB) * (vB * (2 * (2 * vRB + 1 + stepZE) + 1) + 1 + 32 * vRB + 60)11951196/-- AC0 FAMILY CERTIFICATE of the outer controller's update (either schedule): depth ≤ 34,1197    input width IW = 2BN + B + r + 5, total size polynomial in IW (uniformly in B and N). -/1198theorem sh_ac0 (early : Bool) : AC0Fam restAdm shLen (shF early) 34 := by1199  refine ⟨shLen_pos, fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1,1200    fun i _ c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2, ?_⟩1201  exact polyIn_mono (fun i _ => shF_tsize early i) (polyE shLen_pos leafS sh_leaves shSizeE _ (fun _ => rfl))12021203/-- NETWORK FAMILY CERTIFICATE: W = 1 (weights and thresholds in {0,1}), ≤ 70 layers,1204    polynomial widths, fan-ins and gate count; the network's outputs are the formulas. -/1205theorem sh_net (early : Bool) : NetFam restAdm shLen (shN early) 1 70 := by1206  have spec := fun i => compileF_spec (shF early i) (shLen i) 341207    (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).2.2) (fun c hc => (cForms_res early i.1 i.2 (rIdx i.1) c hc).1)1208  have hT := polyE shLen_pos leafS sh_leaves shSizeE1209    (fun i => SW i.1 i.2 (rIdx i.1) * Fz i.1 i.2 (rIdx i.1)) (fun _ => rfl)1210  refine ⟨shLen_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, ?_, ?_⟩1211  · obtain ⟨c, k, h⟩ := polyIn_add shLen_pos hT (polyIn_leaf (fun i _ => Nat.le_refl (shLen i)))1212    refine ⟨c, k, fun i hi => netBounded_mono (spec i).2.2.2.2.2.1 ?_⟩1213    have := shF_tsize early i; have := h i hi; dsimp only at *; unfold tsize at *; omega1214  · have h2 := polyIn_add shLen_pos (polyIn_mul (polyIn_const _ _ (2 * 34 + 1)) hT)1215      (polyE shLen_pos leafS sh_leaves (vB * vN + 4 + vRB + vB) (fun i => SW i.1 i.2 (rIdx i.1)) (fun _ => rfl))1216    refine polyIn_mono (fun i _ => ?_) h21217    have g := (spec i).2.2.2.2.2.21218    have := Nat.mul_le_mul_left (2 * 34 + 1) (shF_tsize early i)1219    have hl : (shF early i).length = SW i.1 i.2 (rIdx i.1) := by unfold shF; rw [cForms_length]1220    unfold tsize at this; rw [hl] at g1221    show gateCount (cNet early i.1 i.2 (rIdx i.1)) ≤ _1222    exact Nat.le_trans g (by omega)12231224/-! ## A6. Exact counts and work -/12251226theorem sum_plus_two (f : Nat → Nat) : ∀ (j n : Nat),1227    ((List.range' j n).map (fun h => f h + 2)).sum = ((List.range' j n).map f).sum + 2 * n1228  | j, 0 => by simp1229  | j, n + 1 => by1230    rw [List.range'_succ, List.map_cons, List.map_cons, List.sum_cons, List.sum_cons, sum_plus_two f (j + 1) n]1231    omega12321233/-- COUNTS, EARLY EXIT (B ≥ 1): with R = number of heads queried (R ≤ B, R = 1 when1234    RO_{π₀}(P) = 1), the controller executes 1 reset tick + Σ_{h<R} L_h policy steps that1235    are legal simulated moves + R terminal-test steps + R consume ticks (R − 1 of which also1236    reload the board for the next head; the last stops) — i.e. 1 + Σ_{h<R} L_h + 2R ticks —1237    and then holds.  The padded clock runs 1 + Tmax ticks instead. -/1238theorem ee_counts {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :1239    eeT B P (B - 1) 0 = ((List.range (eeR P (B - 1) 0)).map (fun h => rolloutMoves h P)).sum + 2 * eeR P (B - 1) 0 ∧1240    eeR P (B - 1) 0 ≤ B ∧ (rolloutWinner 0 P = true → eeR P (B - 1) 0 = 1) ∧1241    eeT B P (B - 1) 0 ≤ Tmax B P.length := by1242  refine ⟨by rw [eeT_sum, sum_plus_two, List.range_eq_range'], (ee_spec hB hw).2.2.2.2.2.1, fun h0 => ?_,1243    (ee_spec hB hw).2.2.2.2.2.2.1⟩1244  obtain ⟨k, hk⟩ : ∃ k, B - 1 = k := ⟨_, rfl⟩1245  rw [hk]; cases k with1246  | zero => rfl1247  | succ k => simp [eeR, h0]12481249/-- COUNTS, ALL HEADS (move path, B ≥ 1): 1 reset tick + totalRolloutMoves legal moves + B1250    terminal tests + B consume ticks = totalRolloutMoves + 2B + 1 controller ticks, then ONE1251    readout-network evaluation: totalRolloutMoves + 2B + 2 network evaluations in all1252    (phase 6's functional composition counted totalRolloutMoves + 2B + 1: B separate1253    resets instead of 1 reset + B consume/reload ticks). -/1254theorem ah_counts {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :1255    1 + ahT P (B - 1) 0 = totalRolloutMoves B P + 2 * B + 1 ∧1256    ahT P (B - 1) 0 ≤ Tmax B P.length ∧1257    totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1)) := by1258  refine ⟨by rw [ahT_total hB]; omega, ?_, totalRolloutMoves_le hw⟩1259  have := ahT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega] at this; exact this12601261/-- WORK PER TICK: formula-node work tsize(cForms) ≤ SW·Fz; compiled network gates1262    ≤ 69·tsize + SW.  Work of a run = (number of ticks) × (work per tick). -/1263theorem tick_work (early : Bool) (B N r : Nat) :1264    tsize (cForms early B N r) ≤ SW B N r * Fz B N r ∧1265    gateCount (cNet early B N r) ≤ (2 * 34 + 1) * tsize (cForms early B N r) + SW B N r := by1266  have h := sum_le_len_mul (cs := cForms early B N r) (S := Fz B N r) (fun c hc => (cForms_res early B N r c hc).2.1)1267  rw [cForms_length] at h1268  refine ⟨h, ?_⟩1269  have g := (compileF_spec (cForms early B N r) (IW B N r) 34 (fun c hc => (cForms_res early B N r c hc).2.2)1270    (fun c hc => (cForms_res early B N r c hc).1)).2.2.2.2.2.21271  rw [cForms_length] at g; exact g12721273/-- SEQUENTIAL TIME IS NOT CONSTANT: each update is one AC0 evaluation, but for B = 1 and1274    the board of T ones the early-exit controller needs more than T ticks. -/1275theorem ticks_unbounded (T : Nat) : ∃ P : List Nat, Width 1 P ∧ T < eeT 1 P 0 0 := by1276  refine ⟨List.replicate T 1, fun x hx => by rw [List.eq_of_mem_replicate hx]; decide, ?_⟩1277  simp only [eeT]1278  rw [rolloutMoves_eq]1279  have : rolloutCount 0 (List.replicate T 1) = T := by1280    unfold rolloutCount heapCount1281    induction T with1282    | zero => rfl1283    | succ T ih => simp [List.replicate_succ] at ih ⊢; omega1284  omega12851286/-! ## The complete maps are not AC0 (the bypass statement is preserved) -/12871288theorem nimSum_bits : ∀ y : List Bool, nimSum (y.map (fun b => if b then 1 else 0)) = if par y then 1 else 01289  | [] => rfl1290  | b :: y => by1291    simp only [List.map_cons, nimSum, par, nimSum_bits y]1292    cases b <;> by_cases hp : par y = true <;> simp [hp]12931294/-- Under ParityNotAC0, no AC0 formula family (any fixed depth, polynomial size) computes the1295    complete P/N CLASSIFICATION on all boards — not even on boards of one-bit heaps, where it1296    is parity. -/1297theorem no_ac0_classifier (hard : ParityNotAC0) (F : Nat → Circ) (d c k : Nat)1298    (hd : ∀ m, depth (F m) ≤ d) (hs : ∀ m, size (F m) ≤ c * m ^ k) (hm : ∀ m, maxInput (F m) ≤ m)1299    (hcorr : ∀ (m : Nat) (y : List Bool), y.length = m →1300      eval (vfun y) (F m) = decide (nimSum (y.map (fun b => if b then 1 else 0)) ≠ 0)) : False := by1301  obtain ⟨m0, hm0⟩ := hard d c k1302  obtain ⟨y, hy, hne⟩ := hm0 m0 (Nat.le_refl _) (F m0) (hd m0) (hs m0) (hm m0)1303  apply hne1304  rw [hcorr m0 y (mem_bitvecs_length hy), nimSum_bits]1305  cases par y <;> rfl13061307/-- Under ParityNotAC0 the complete board-to-move map of the implemented all-head controller1308    with readout (ahMove) is not computed by any AC0 binary selector family on all width-21309    boards (it equals mhExec, Bypass.no_ac0_mhExec_allBoards). -/1310theorem no_ac0_ahMove (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)1311    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)1312    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)1313    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P →1314      ParityCircuit.binMove (S m) (m + 1) P = ahMove 2 P) : False :=1315  Bypass.no_ac0_mhExec_allBoards hard S r d hfam hidx (fun m hm P hP hw => (hcomp m hm P hP hw).trans (ahMove_eq hw))13161317/-! ## Further interface statements -/13181319/-- RESET FROM ARBITRARY BITS lands in a valid encoded state (unused encodings, e.g. head1320    indices ≥ B, are never reached afterwards: brun_enc preserves validity). -/1321theorem reset_valid (early : Bool) {B N r : Nat} {P : List Nat} (hP : P.length = N) (hwP : Width B P)1322    (x : Nat → Bool) : ∃ s, Valid B N r s ∧ cstep early B N r P true x = enc B N r s :=1323  ⟨initOS B P, initOS_valid hP hwP, cstep_reset early B N r P x⟩13241325/-- The all-head move path executed by the THRESHOLD NETWORK (both the controller ticks and1326    the readout are network evaluations) equals mhExec. -/1327def ahMoveN (B : Nat) (P : List Nat) : Option (Nat × Nat) :=1328  netBinSem (mhN (B, P.length)) P.length (rIdx P.length) B1329    (obsIn B P.length P (fun h => nimpl false B P.length (rIdx B) P (Tmax B P.length) (fun _ => false) (oW B P.length (rIdx B) h)))13301331theorem ahMoveN_eq {B : Nat} {P : List Nat} (hw : Width B P) : ahMoveN B P = mhExec B P := by1332  unfold ahMoveN; simp only [nimpl_eq]; exact ahMove_eq hw13331334/-! ## A5/A6. The all-head move path with early stopping (halting loop) -/13351336/-- ALL-HEAD HALTING LOOP: after the reset, the loop on the run wire stops after exactly1337    ahT = totalRolloutMoves + 2B ticks with every outcome stored. -/1338theorem ah_loop {B N r : Nat} (hB : 1 ≤ B) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)1339    (x0 : Nat → Bool) :1340    (loopRun (cstep false B N r P false) (B * N + 2) (Tmax B N) (cstep false B N r P true x0)).2 = ahT P (B - 1) 0 ∧1341    ∀ h, h < B → (loopRun (cstep false B N r P false) (B * N + 2) (Tmax B N) (cstep false B N r P true x0)).11342      (oW B N r h) = rolloutWinner h P := by1343  have hinit : initOS B P = ld P 0 false (fun _ => false) := by simp [initOS, ld]; omega1344  obtain ⟨h1, h2, h3⟩ := ah_run B P (B - 1) 0 (by omega) false (fun _ => false) (fun h hh => by omega)1345  have hle : ahT P (B - 1) 0 ≤ Tmax B N := by1346    have := ahT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega, hP] at this; exact this1347  rw [← hinit] at h1 h2 h31348  rw [cstep_reset, loopRun_spec false hBr hP hw _ _ _ (initOS_valid hP hw) hle h3 h1]1349  exact ⟨rfl, fun h hh => by show enc B N r _ (oW B N r h) = _; rw [enc_o _ _ _ _ hh, h2 h hh]⟩13501351/-- The all-head move with early stopping: halting loop, then the existing readout. -/1352def ahMoveL (B : Nat) (P : List Nat) : Option (Nat × Nat) :=1353  netBinSem (mhN (B, P.length)) P.length (rIdx P.length) B1354    (obsIn B P.length P (fun h => (loopRun (cstep false B P.length (rIdx B) P false) (B * P.length + 2)1355      (Tmax B P.length) (cstep false B P.length (rIdx B) P true (fun _ => false))).1 (oW B P.length (rIdx B) h)))13561357theorem ahMoveL_eq {B : Nat} {P : List Nat} (hw : Width B P) : ahMoveL B P = mhExec B P := by1358  have hBr : B ≤ 2 ^ rIdx B := Nat.le_of_lt (rIdx_counter B)1359  unfold ahMoveL mhExec1360  rw [(mh_semantics rfl hw _).2.1]1361  show attainT _ P = netBinSem (mhN (B, P.length)) P.length (rIdx P.length) B _1362  rw [(mh_semantics rfl hw _).2.1]1363  congr 11364  apply reconstruct_congr1365  intro h hh1366  rw [outBit_eq hw, (ah_loop (by omega) hBr rfl hw _).2 h hh]13671368/-- COUNTS OF THE EXECUTED MOVE PATH (B ≥ 1): 1 reset tick + exactly totalRolloutMoves + 2B1369    loop ticks (Σ L_h legal moves, B terminal tests, B consume ticks), then one readout. -/1370theorem ahL_counts {B N r : Nat} (hB : 1 ≤ B) (hBr : B ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)1371    (x0 : Nat → Bool) :1372    1 + (loopRun (cstep false B N r P false) (B * N + 2) (Tmax B N) (cstep false B N r P true x0)).2 =1373      totalRolloutMoves B P + 2 * B + 1 := by1374  rw [(ah_loop hB hBr hP hw x0).1, ahT_total hB]; omega13751376/-- WORK OF A RUN (formula nodes evaluated, reset tick included): early exit and all heads,1377    with the exact tick counts, are bounded by the padded-clock work (1 + Tmax)·SW·Fz. -/1378theorem run_work {B N r : Nat} (hB : 1 ≤ B) {P : List Nat} (hP : P.length = N) (hw : Width B P) (early : Bool) :1379    (1 + eeT B P (B - 1) 0) * tsize (cForms early B N r) ≤ (1 + Tmax B N) * (SW B N r * Fz B N r) ∧1380    (1 + ahT P (B - 1) 0) * tsize (cForms early B N r) ≤ (1 + Tmax B N) * (SW B N r * Fz B N r) := by1381  have hT := (tick_work early B N r).11382  have h1 : eeT B P (B - 1) 0 ≤ Tmax B N := by have := (ee_spec hB hw).2.2.2.2.2.2.1; rwa [hP] at this1383  have h2 : ahT P (B - 1) 0 ≤ Tmax B N := by1384    have := ahT_le B hw (B - 1) 0; unfold Tmax; rw [show B - 1 + 1 = B by omega, hP] at this; exact this1385  exact ⟨Nat.mul_le_mul (by omega) hT, Nat.mul_le_mul (by omega) hT⟩13861387/-! ## Axiom audit -/13881389#print axioms cForms_length1390#print axioms cF_board1391#print axioms cF_mid1392#print axioms cF_par1393#print axioms cF_halt1394#print axioms cF_run1395#print axioms cF_dec1396#print axioms cF_j1397#print axioms cF_o1398#print axioms z_low1399#print axioms z_par1400#print axioms z_halt1401#print axioms z_run1402#print axioms z_dec1403#print axioms z_j1404#print axioms z_o1405#print axioms z_rst1406#print axioms z_P1407#print axioms eval_isH_bits1408#print axioms eval_isH1409#print axioms eval_incB1410#print axioms eval_hstep1411#print axioms eval_mstep1412#print axioms ostep_flat1413#print axioms enc_low1414#print axioms rsBits_board1415#print axioms rsBits_par1416#print axioms rsBits_halt1417#print axioms enc_run1418#print axioms enc_dec1419#print axioms enc_j1420#print axioms enc_o1421#print axioms enc_high1422#print axioms wire_cases1423#print axioms cstep_reset1424#print axioms cstep_enc1425#print axioms initOS_valid1426#print axioms ostep_valid1427#print axioms arun_add1428#print axioms brun_enc1429#print axioms arun_one1430#print axioms ostep_hold1431#print axioms arun_hold1432#print axioms arun_untilHalt1433#print axioms roll_phase1434#print axioms query_step1435#print axioms ee_run1436#print axioms eeR_shootout1437#print axioms eeR_le1438#print axioms eeT_sum1439#print axioms eeT_le1440#print axioms ee_spec1441#print axioms impl_enc1442#print axioms nimSum_width01443#print axioms ee_impl1444#print axioms ee_impl_padded1445#print axioms loopRun_spec1446#print axioms ee_loop1447#print axioms ah_run1448#print axioms ahT_sum1449#print axioms ahT_total1450#print axioms ahT_le1451#print axioms reconstruct_congr1452#print axioms ahMove_eq1453#print axioms ahSel_wins1454#print axioms early_exit_not_move1455#print axioms nstep_eq1456#print axioms nimpl_eq1457#print axioms ee_net1458#print axioms and_res1459#print axioms or_res1460#print axioms R3_mono1461#print axioms not_res1462#print axioms inp31463#print axioms cst31464#print axioms mux31465#print axioms S1_pos1466#print axioms hstep_res1467#print axioms isH_res1468#print axioms mstep_res1469#print axioms cForms_res1470#print axioms shLen_pos1471#print axioms sh_leaves1472#print axioms shF_tsize1473#print axioms sh_ac01474#print axioms sh_net1475#print axioms sum_plus_two1476#print axioms ee_counts1477#print axioms ah_counts1478#print axioms tick_work1479#print axioms ticks_unbounded1480#print axioms nimSum_bits1481#print axioms no_ac0_classifier1482#print axioms no_ac0_ahMove1483#print axioms reset_valid1484#print axioms ahMoveN_eq1485#print axioms ah_loop1486#print axioms ahMoveL_eq1487#print axioms ahL_counts1488#print axioms run_work14891490end Shootout1491end NimAudit