ThresholdInst

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 ThresholdNet2import PriorityEncoder34/- Phase 5, task 2 (instances): the threshold-network compiler applied to the5   recurrent controller's per-update circuits and to the binary selectors.6   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.78   * THRESHOLD UPDATE.  One fixed-scale network (W = 1) computes all9     4 + 5B + 3r next-state bits and all 4 + 3B + r output bits of the controller10     from the 6 + 6B + 3r input wires (state wires, row flag, reset flag, row value).11     `tstep_eq`: the threshold update equals the bit-level update `bstep` for EVERY12     state vector and token, so run refinement, reset from arbitrary bit states,13     the stream/game theorems and the register bounds transfer verbatim.14   * BINARY SELECTORS AS NETWORKS.  Any binary readout (valid, r index bits, B value15     bits) compiles to a network whose output wires 0, 1..r, r+1..r+B decode to the same16     move; instantiated for attainability, local restoration, π_j and multi-head. -/1718namespace NimAudit19namespace ThresholdInst2021open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit22  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet FiniteNet2324/-! ## The controller's output wires in a fixed order -/2526/-- Output wire j: 0 summary flag; 1..B summary bits; B+1..2B difference bits;27    2B+1 difference-valid; 2B+2 move flag; 2B+3 move-valid; 2B+4.. index bits (r);28    2B+4+r.. move value bits (B). -/29def outAt (B r j : Nat) : Circ :=30  if j = 0 then sumOutC B r31  else if j < 1 + B then sumBitC (j - 1)32  else if j < 1 + 2 * B then diffBitC B (j - (1 + B))33  else if j = 1 + 2 * B then ControllerBits.diffValidC B34  else if j = 2 + 2 * B then moveOutC B r35  else if j = 3 + 2 * B then moveValidC B r36  else if j < 4 + 2 * B + r then moveIC B r (j - (4 + 2 * B))37  else if j < 4 + 3 * B + r then moveVC B r (j - (4 + 2 * B + r))38  else const false3940def outCount (B r : Nat) : Nat := 4 + 3 * B + r41def inWidth (B r : Nat) : Nat := 6 + 6 * B + 3 * r4243/-- Decoding the output wires into a controller output (bit reading only). -/44def outDecode (B r : Nat) (w : Nat → Bool) : Option COut :=45  if w 0 then46    some (COut.summary (ofBits B (fun k => w (1 + k)))47      (if w (1 + 2 * B) then some (ofBits B (fun k => w (1 + B + k))) else none))48  else if w (2 + 2 * B) then49    some (COut.move (if w (3 + 2 * B) then50      some (ofBits r (fun q => w (4 + 2 * B + q)), ofBits B (fun k => w (4 + 2 * B + r + k))) else none))51  else none5253theorem ofBits_congr (B : Nat) (f g : Nat → Bool) (h : ∀ k < B, f k = g k) : ofBits B f = ofBits B g := by54  induction B with55  | zero => rfl56  | succ B ih =>57    simp only [ofBits]58    rw [h B (by omega), ih (fun k hk => h k (by omega))]5960theorem outDecode_congr (B r : Nat) (w w' : Nat → Bool) (h : ∀ k < outCount B r, w k = w' k) :61    outDecode B r w = outDecode B r w' := by62  unfold outCount at h63  unfold outDecode64  rw [h 0 (by omega), h (1 + 2 * B) (by omega), h (2 + 2 * B) (by omega), h (3 + 2 * B) (by omega),65    ofBits_congr B (fun k => w (1 + k)) (fun k => w' (1 + k)) (fun k hk => h _ (by omega)),66    ofBits_congr B (fun k => w (1 + B + k)) (fun k => w' (1 + B + k)) (fun k hk => h _ (by omega)),67    ofBits_congr r (fun q => w (4 + 2 * B + q)) (fun q => w' (4 + 2 * B + q)) (fun q hq => h _ (by omega)),68    ofBits_congr B (fun k => w (4 + 2 * B + r + k)) (fun k => w' (4 + 2 * B + r + k)) (fun k hk => h _ (by omega))]6970theorem outDecode_eval (B r : Nat) (z : Nat → Bool) :71    outDecode B r (fun j => eval z (outAt B r j)) = decodeOut B r z := by72  unfold outDecode decodeOut73  have e0 : outAt B r 0 = sumOutC B r := by simp [outAt]74  have e1 : outAt B r (1 + 2 * B) = ControllerBits.diffValidC B := by75    simp (disch := omega) only [outAt, if_neg, if_pos, ↓reduceIte]76  have e2 : outAt B r (2 + 2 * B) = moveOutC B r := by77    simp (disch := omega) only [outAt, if_neg, if_pos, ↓reduceIte]78  have e3 : outAt B r (3 + 2 * B) = moveValidC B r := by79    simp (disch := omega) only [outAt, if_neg, if_pos, ↓reduceIte]80  have hs : ofBits B (fun k => eval z (outAt B r (1 + k))) = ofBits B (fun k => eval z (sumBitC k)) :=81    ofBits_congr _ _ _ (fun k hk => by82      simp (disch := omega) only [outAt, if_neg, if_pos]; congr 2; omega)83  have hd : ofBits B (fun k => eval z (outAt B r (1 + B + k))) = ofBits B (fun k => eval z (diffBitC B k)) :=84    ofBits_congr _ _ _ (fun k hk => by85      simp (disch := omega) only [outAt, if_neg, if_pos]; congr 2; omega)86  have hi : ofBits r (fun q => eval z (outAt B r (4 + 2 * B + q))) = ofBits r (fun q => eval z (moveIC B r q)) :=87    ofBits_congr _ _ _ (fun q hq => by88      simp (disch := omega) only [outAt, if_neg, if_pos]; congr 2; omega)89  have hv : ofBits B (fun k => eval z (outAt B r (4 + 2 * B + r + k))) =90      ofBits B (fun k => eval z (moveVC B r k)) :=91    ofBits_congr _ _ _ (fun k hk => by92      simp (disch := omega) only [outAt, if_neg, if_pos]; congr 2; omega)93  simp only [e0, e1, e2, e3, hs, hd, hi, hv]9495theorem outAt_res (B r j : Nat) (hj : j < outCount B r) :96    size (outAt B r j) ≤ 16 ∧ depth (outAt B r j) ≤ 3 ∧ maxInput (outAt B r j) ≤ inWidth B r := by97  unfold outCount at hj98  unfold outAt inWidth99  by_cases h0 : j = 0100  · rw [if_pos h0]; simp [sumOutC, Ec, Mc, listMax]; omega101  by_cases h1 : j < 1 + B102  · rw [if_neg h0, if_pos h1]; simp [sumBitC]; omega103  by_cases h2 : j < 1 + 2 * B104  · rw [if_neg h0, if_neg h1, if_pos h2]; simp [diffBitC, xor2, listMax]; omega105  by_cases h3 : j = 1 + 2 * B106  · rw [if_neg h0, if_neg h1, if_neg h2, if_pos h3]; simp [ControllerBits.diffValidC]; omega107  by_cases h4 : j = 2 + 2 * B108  · rw [if_neg h0, if_neg h1, if_neg h2, if_neg h3, if_pos h4]; simp [moveOutC, Ec, Mc, listMax]; omega109  by_cases h5 : j = 3 + 2 * B110  · rw [if_neg h0, if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_pos h5]; simp [moveValidC, listMax]; omega111  by_cases h6 : j < 4 + 2 * B + r112  · rw [if_neg h0, if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_pos h6]113    simp [moveIC, mux, listMax]; omega114  have h7 : j < 4 + 3 * B + r := by omega115  rw [if_neg h0, if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_pos h7]116  simp [moveVC, mux, listMax]; omega117118/-! ## The threshold update -/119120/-- All formulas of one controller update: next-state wires, then output wires. -/121def ctrlForms (B r : Nat) : List Circ :=122  (List.range (stateWidth B r + outCount B r)).map123    (fun k => if k < stateWidth B r then nextC B r k else outAt B r (k - stateWidth B r))124125/-- THE CONTROLLER'S FIXED-SCALE THRESHOLD NETWORK. -/126def ctrlNet (B r : Nat) : List Layer := compileF (ctrlForms B r)127128/-- One update of the threshold-network controller. -/129def tstep (B r : Nat) (v : Nat → Bool) (t : Tok) : (Nat → Bool) × Option COut :=130  ((fun j => if j < stateWidth B r then evalNet (ctrlNet B r) (inp B r v t) j else false),131   outDecode B r (fun k => evalNet (ctrlNet B r) (inp B r v t) (stateWidth B r + k)))132133theorem ctrlForms_get (B r k : Nat) (hk : k < (ctrlForms B r).length) :134    (ctrlForms B r)[k] = if k < stateWidth B r then nextC B r k else outAt B r (k - stateWidth B r) := by135  simp [ctrlForms]136137theorem ctrlForms_length (B r : Nat) : (ctrlForms B r).length = stateWidth B r + outCount B r := by138  simp [ctrlForms]139140/-- THRESHOLD REFINEMENT: the network update equals the bit-level update for every141    state vector and every token. -/142theorem tstep_eq (B r : Nat) (v : Nat → Bool) (t : Tok) : tstep B r v t = bstep B r v t := by143  unfold tstep bstep144  congr 1145  · funext j146    by_cases hj : j < stateWidth B r147    · rw [if_pos hj, ctrlNet, compileF_eval (ctrlForms B r) _ (by rw [ctrlForms_length]; omega),148        ctrlForms_get, if_pos hj]149    · rw [if_neg hj, nextC_beyond B r j (by omega)]; simp150  · rw [outDecode_congr B r _ (fun j => eval (inp B r v t) (outAt B r j)) (fun k hk => by151      rw [ctrlNet, compileF_eval (ctrlForms B r) _ (by rw [ctrlForms_length]; omega), ctrlForms_get,152        if_neg (by omega), Nat.add_sub_cancel_left])]153    exact outDecode_eval B r _154155/-- Runs of the threshold controller. -/156def trun (B r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool) × List COut157  | v, [] => (v, [])158  | v, t :: ts => ((trun B r (tstep B r v t).1 ts).1, (tstep B r v t).2.toList ++ (trun B r (tstep B r v t).1 ts).2)159160theorem trun_eq (B r : Nat) : ∀ (v : Nat → Bool) (ts : List Tok), trun B r v ts = brun B r v ts161  | _, [] => rfl162  | v, t :: ts => by simp only [trun, brun, tstep_eq, trun_eq B r _ ts]163164theorem trun_append (B r : Nat) (v : Nat → Bool) (ts us : List Tok) :165    trun B r v (ts ++ us) =166      ((trun B r (trun B r v ts).1 us).1, (trun B r v ts).2 ++ (trun B r (trun B r v ts).1 us).2) := by167  simp only [trun_eq]; exact brun_append B r v ts us168169/-- RUN REFINEMENT (threshold level): from the canonical encoding of a semantic state,170    the threshold controller tracks the semantic controller along every run satisfying171    the width side conditions. -/172theorem trun_refines {B r : Nat} (s : CState) (ts : List Tok) (h : AllDec B r s ts) :173    trun B r (sbits B r s) ts = (sbits B r (crun s ts).1, (crun s ts).2) := by174  rw [trun_eq]; exact brun_refines s ts h175176/-- STREAM THEOREM (threshold level). -/177theorem trun_stream {B r N : Nat} (hN : N < 2 ^ r) (Ps : List (List Nat))178    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) :179    (trun B r (sbits B r cinit) (stream Ps)).2 = ctrlOuts false 0 Ps := by180  rw [trun_eq]; exact bits_stream hN Ps hP181182/-- RESET FROM ARBITRARY BIT STATES and GAMES (threshold level). -/183theorem tstep_reset (B r : Nat) (v : Nat → Bool) : tstep B r v Tok.reset = (sbits B r cinit, none) := by184  rw [tstep_eq]; exact bstep_reset B r v185186theorem trun_games (B r : Nat) (v : Nat → Bool) (gs : List (List (List Nat)))187    (h : ∀ g ∈ gs, ∃ N, N < 2 ^ r ∧ ∀ P ∈ g, P.length = N ∧ Width B P) :188    (trun B r v (gameStream gs)).2 = gs.flatMap (ctrlOuts false 0) := by189  rw [trun_eq]; exact bits_games B r v gs h190191theorem crunStates_prefix : ∀ (s : CState) (ts us : List Tok), ∀ st ∈ crunStates s ts,192    st ∈ crunStates s (ts ++ us)193  | s, [], us, st, h => by simp [crunStates] at h; subst h; exact self_mem_crunStates st us194  | s, t :: ts, us, st, h => by195    simp only [crunStates, List.mem_cons] at h196    simp only [List.cons_append, crunStates, List.mem_cons]197    rcases h with rfl | h198    · left; rfl199    · right; exact crunStates_prefix _ ts us st h200201/-- WIDTH PRESERVATION and LOSSLESS STATE (threshold level): after EVERY prefix of a202    well-formed stream, the threshold controller's state vector is the canonical encoding203    of a reachable semantic state whose registers fit (counter included, no overflow) and204    which is recovered exactly from the vector. -/205theorem trun_states_fit {B r N : Nat} (hN : N < 2 ^ r) (Ps : List (List Nat))206    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) : ∀ k, ∃ st ∈ crunStates cinit (stream Ps),207      (trun B r (sbits B r cinit) ((stream Ps).take k)).1 = sbits B r st ∧208      FitsR B r st ∧ decodeS B r (sbits B r st) = st := by209  intro k210  have hfit0 : Fits B N cinit :=211    ⟨Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.zero_le _, by simp [cinit], by simp [cinit]⟩212  have hfits := stream_fits cinit cinit_idle hfit0 Ps hP213  have e := List.take_append_drop k (stream Ps)214  have hpre : ∀ st ∈ crunStates cinit ((stream Ps).take k), st ∈ crunStates cinit (stream Ps) := by215    intro st h216    have := crunStates_prefix cinit _ ((stream Ps).drop k) st h217    rwa [e] at this218  have hall : AllDec B r cinit ((stream Ps).take k) :=219    allDec_of_fits hN cinit _ (fun st h => hfits st (hpre st h))220      (fun t ht => tok_bound_stream Ps (fun P h => (hP P h).2) t (List.mem_of_mem_take ht))221  have hmem := hpre _ (crun_mem_states cinit ((stream Ps).take k))222  refine ⟨(crun cinit ((stream Ps).take k)).1, hmem, ?_, reachable_lossless hN Ps hP _ hmem⟩223  rw [trun_refines _ _ hall]224225theorem trun_one_board {B r : Nat} (P : List Nat) (hN : P.length < 2 ^ r) (hw : Width B P) :226    (trun B r (sbits B r cinit) (dtoks P)).2 = [COut.summary (nimSum P) none, COut.move (decisionMove P)] := by227  rw [trun_eq]; exact bits_one_board P hN hw228229/-! ## Resources of the controller network -/230231theorem ctrlForms_res (B r : Nat) :232    ∀ c ∈ ctrlForms B r, depth c ≤ 8 ∧ size c ≤ cellSize B r + 16 ∧ maxInput c ≤ inWidth B r := by233  intro c hc234  simp only [ctrlForms, List.mem_map, List.mem_range] at hc235  obtain ⟨k, hk, rfl⟩ := hc236  by_cases hs : k < stateWidth B r237  · rw [if_pos hs]238    obtain ⟨a, b, d⟩ := nextC_resources B r k239    exact ⟨b, by omega, by unfold inWidth; omega⟩240  · rw [if_neg hs]241    obtain ⟨a, b, d⟩ := outAt_res B r (k - stateWidth B r) (by omega)242    exact ⟨by omega, by omega, d⟩243244theorem ctrlForms_size (B r : Nat) :245    ((ctrlForms B r).map size).sum ≤ (stateWidth B r + outCount B r) * (cellSize B r + 16) := by246  have := sum_le_len_mul (cs := ctrlForms B r) (S := cellSize B r + 16) (fun c hc => (ctrlForms_res B r c hc).2.1)247  rwa [ctrlForms_length] at this248249/-- CONTROLLER NETWORK RESOURCES: W = 1, wired at the input width 6 + 6B + 3r, at most250    18 layers, layer widths and fan-ins ≤ S + 6 + 6B + 3r with251    S ≤ (8 + 8B + 4r)(2B² + 8B + 2r + 57), and at most 17·S + 8 + 8B + 4r gates. -/252theorem ctrlNet_res (B r : Nat) :253    NetValid 1 (ctrlNet B r) ∧ Wired (inWidth B r) (ctrlNet B r) ∧ (ctrlNet B r).length ≤ 18 ∧254    NetBounded (((ctrlForms B r).map size).sum + inWidth B r) (ctrlNet B r) ∧255    gateCount (ctrlNet B r) ≤ 17 * ((ctrlForms B r).map size).sum + (stateWidth B r + outCount B r) ∧256    ((ctrlForms B r).map size).sum ≤ (stateWidth B r + outCount B r) * (cellSize B r + 16) := by257  unfold ctrlNet258  obtain ⟨_, _, h3, h4, h5, h6, h7⟩ := compileF_spec (ctrlForms B r) (inWidth B r) 8259    (fun c hc => (ctrlForms_res B r c hc).2.2) (fun c hc => (ctrlForms_res B r c hc).1)260  rw [ctrlForms_length] at h7261  exact ⟨h3, h4, by omega, h6, h7, ctrlForms_size B r⟩262263/-- Memory and update counts are those of the bit-level controller: 4 + 5B + 3r state264    bits (7 + 5B + 3·log₂N with r = log₂N + 1), 2N + 2 network updates per decision,265    one extra update per reset token. -/266theorem ctrl_counts (B N : Nat) (P : List Nat) :267    stateWidth B (N.log2 + 1) = 7 + 5 * B + 3 * N.log2 ∧ N < 2 ^ (N.log2 + 1) ∧268    (dtoks P).length = 2 * P.length + 2 :=269  ⟨(counter_width (B := B) N).2, (counter_width (B := B) N).1, dtoks_length P⟩270271/-! ## Summary-only corollary -/272273/-- The summary mechanism's formulas: mode, acc (B), prev (B), valid, and the summary274    outputs (flag, B summary bits, B difference bits, difference-valid). -/275def summaryForms (B r : Nat) : List Circ :=276  [modeN B r] ++ (List.range B).map (accN B r) ++ (List.range B).map (prevN B r) ++ [validN B r] ++277    [sumOutC B r] ++ (List.range B).map sumBitC ++ (List.range B).map (diffBitC B) ++ [ControllerBits.diffValidC B]278279theorem summaryForms_res (B r : Nat) :280    ∀ c ∈ summaryForms B r, depth c ≤ 8 ∧ size c ≤ 35 ∧ maxInput c ≤ inWidth B r := by281  intro c hc282  simp only [summaryForms, List.mem_append, List.mem_cons, List.mem_map, List.mem_range, List.not_mem_nil,283    or_false] at hc284  unfold inWidth285  rcases hc with ((((((rfl | ⟨k, hk, rfl⟩) | ⟨k, hk, rfl⟩) | rfl) | rfl) | ⟨k, hk, rfl⟩) | ⟨k, hk, rfl⟩) | rfl286  · refine ⟨?_, by have := (summary_resources B r 0).1; omega, ?_⟩ <;> simp [modeN, Rc, Wc, Ec, Mc, listMax] <;> omega287  · refine ⟨?_, by have := (summary_resources B r k).2.1; omega, ?_⟩ <;> simp [accN, Rc, Wc, Ec, Mc, xI, xor2, listMax] <;> omega288  · refine ⟨?_, by have := (summary_resources B r k).2.2.1; omega, ?_⟩ <;> simp [prevN, mux, Rc, Wc, Ec, Mc, listMax] <;> omega289  · refine ⟨?_, by have := (summary_resources B r 0).2.2.2; omega, ?_⟩ <;> simp [validN, Rc, Wc, Ec, Mc, listMax] <;> omega290  · refine ⟨?_, ?_, ?_⟩ <;> simp [sumOutC, Ec, Mc, listMax] <;> omega291  · refine ⟨?_, ?_, ?_⟩ <;> simp [sumBitC] <;> omega292  · refine ⟨?_, ?_, ?_⟩ <;> simp [diffBitC, xor2, listMax] <;> omega293  · refine ⟨?_, ?_, ?_⟩ <;> simp [ControllerBits.diffValidC] <;> omega294295theorem summaryForms_length (B r : Nat) : (summaryForms B r).length = 4 + 4 * B := by296  simp [summaryForms]; omega297298/-- SUMMARY-ONLY NETWORK: the summary registers' updates and summary outputs are computed299    by a W = 1 network with at most 18 layers and at most 17·35·(4+4B) + 4 + 4B gates,300    i.e. O(B) gates (the replay part is what adds the B² and log N terms). -/301theorem summaryNet_res (B r : Nat) :302    (∀ x : Nat → Bool, ∀ k (hk : k < (summaryForms B r).length),303      evalNet (compileF (summaryForms B r)) x k = eval x (summaryForms B r)[k]) ∧304    NetValid 1 (compileF (summaryForms B r)) ∧ (compileF (summaryForms B r)).length ≤ 18 ∧305    gateCount (compileF (summaryForms B r)) ≤ 17 * (35 * (4 + 4 * B)) + (4 + 4 * B) := by306  obtain ⟨h1, _, h3, _, h5, _, h7⟩ := compileF_spec (summaryForms B r) (inWidth B r) 8307    (fun c hc => (summaryForms_res B r c hc).2.2) (fun c hc => (summaryForms_res B r c hc).1)308  have hs := sum_le_len_mul (cs := summaryForms B r) (S := 35) (fun c hc => (summaryForms_res B r c hc).2.1)309  rw [summaryForms_length] at hs h7310  refine ⟨h1, h3, by omega, ?_⟩311  have : 17 * ((summaryForms B r).map size).sum ≤ 17 * (35 * (4 + 4 * B)) := by312    exact Nat.mul_le_mul_left _ (by rw [Nat.mul_comm]; exact hs)313  omega314315/-! ## Binary selectors as threshold networks -/316317/-- Output order: wire 0 valid, wires 1..r index bits, wires r+1..r+B value bits. -/318def bForms (S : BCirc) : List Circ := S.valid :: (S.idx ++ S.val)319320def binNet (S : BCirc) : List Layer := compileF (bForms S)321322/-- Decoding the output wires of a binary-selector network (bit reading only). -/323def netBinSem (net : List Layer) (N r B : Nat) (x : Nat → Bool) : Option (Nat × Nat) :=324  if evalNet net x 0 then325    if toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))) < N then326      some (toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))),327        toNatBE ((List.range B).map (fun k => evalNet net x (1 + r + k))))328    else none329  else none330331theorem map_range_eq {r : Nat} (l : List Circ) (hl : l.length = r) (f : Nat → Bool) (x : Nat → Bool)332    (h : ∀ q (hq : q < r), f q = eval x (l[q]'(by omega))) : (List.range r).map f = l.map (eval x) := by333  apply List.ext_getElem (by simp [hl])334  intro n h1 h2335  simp only [List.getElem_map, List.getElem_range]336  exact h n (by simpa using h1)337338/-- NETWORK = BINARY SELECTOR, on every input. -/339theorem binNet_correct (S : BCirc) {N r B : Nat} (hr : S.idx.length = r) (hB : S.val.length = B)340    (x : Nat → Bool) : netBinSem (binNet S) N r B x = binSem S N x := by341  have hlen : (bForms S).length = 1 + r + B := by simp [bForms, hr, hB]; omega342  have h0 : evalNet (binNet S) x 0 = eval x S.valid := by343    rw [binNet, compileF_eval _ _ (by omega)]; rfl344  have hi : (List.range r).map (fun q => evalNet (binNet S) x (1 + q)) = S.idx.map (eval x) := by345    apply map_range_eq S.idx hr346    intro q hq347    rw [binNet, compileF_eval _ _ (by omega)]348    have e : (bForms S)[1 + q]? = S.idx[q]? := by349      simp [bForms, show 1 + q = q + 1 by omega, List.getElem?_append_left (show q < S.idx.length by omega)]350    rw [List.getElem?_eq_getElem (by omega), List.getElem?_eq_getElem (by omega)] at e351    rw [Option.some.inj e]352  have hv : (List.range B).map (fun k => evalNet (binNet S) x (1 + r + k)) = S.val.map (eval x) := by353    apply map_range_eq S.val hB354    intro k hk355    rw [binNet, compileF_eval _ _ (by omega)]356    have e : (bForms S)[1 + r + k]? = S.val[k]? := by357      simp [bForms, show 1 + r + k = (r + k) + 1 by omega,358        List.getElem?_append_right (show S.idx.length ≤ r + k by omega), hr]359    rw [List.getElem?_eq_getElem (by omega), List.getElem?_eq_getElem (by omega)] at e360    rw [Option.some.inj e]361  unfold netBinSem binSem362  rw [h0, hi, hv]363364/-- NETWORK RESOURCES of a compiled binary selector. -/365theorem binNet_res {S : BCirc} {N B r D Sz M : Nat} (h : BinBound S N B r D Sz M) :366    NetValid 1 (binNet S) ∧ Wired M (binNet S) ∧ (binNet S).length ≤ 2 * D + 2 ∧367    NetBounded ((1 + r + B) * Sz + M) (binNet S) ∧368    gateCount (binNet S) ≤ (2 * D + 1) * ((1 + r + B) * Sz) + (1 + r + B) := by369  unfold binNet370  have hall : ∀ c ∈ bForms S, depth c ≤ D ∧ size c ≤ Sz ∧ maxInput c ≤ M := fun c hc => h.all c hc371  have hlen : (bForms S).length = 1 + r + B := by simp [bForms, h.idx_len, h.val_len]; omega372  obtain ⟨_, _, h3, h4, h5, h6, h7⟩ := compileF_spec (bForms S) M D (fun c hc => (hall c hc).2.2)373    (fun c hc => (hall c hc).1)374  have hs := sum_le_len_mul (cs := bForms S) (S := Sz) (fun c hc => (hall c hc).2.1)375  rw [hlen] at hs h7376  refine ⟨h3, h4, h5, ?_, ?_⟩377  · intro l hl378    obtain ⟨a, b⟩ := h6 l hl379    exact ⟨by omega, fun g hg => by have := b g hg; omega⟩380  · have : (2 * D + 1) * ((bForms S).map size).sum ≤ (2 * D + 1) * ((1 + r + B) * Sz) :=381      Nat.mul_le_mul_left _ hs382    omega383384/-- Local restoration as a fixed-scale network on the two frames. -/385def restNet (B N r : Nat) : List Layer := binNet (restBin B N r)386387theorem restNet_correct {B N r : Nat} (hr : N ≤ 2 ^ r) {Q Q' : List Nat} (hQ : Q.length = N)388    (hQ' : Q'.length = N) (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :389    ∃ i v, netBinSem (restNet B N r) N r B (LocalRestore.tf B N Q Q') = some (i, v) ∧390      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by391  have hb := restBin_bound (B := B) (N := N) hr392  rw [restNet, binNet_correct _ hb.idx_len hb.val_len]393  exact restBin_correct hr hQ hQ' hw hw' h0 hm394395theorem restNet_res {B N r : Nat} (hr : N ≤ 2 ^ r) :396    NetValid 1 (restNet B N r) ∧ Wired (2 * (B * N)) (restNet B N r) ∧ (restNet B N r).length ≤ 2 * 20 + 2 :=397  let h := binNet_res (restBin_bound (B := B) (N := N) hr)398  ⟨h.1, h.2.1, h.2.2.1⟩399400/-- The multi-head selector as a fixed-scale network on board and outcome wires. -/401def mhNet (B N r : Nat) : List Layer := binNet (mhBin B N r)402403theorem mhNet_correct {B N r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) :404    netBinSem (mhNet B N r) N r B (obsIn B N P (outcomes P)) = decisionMove P := by405  have hb := mhBin_bound (B := B) (N := N) hr406  rw [mhNet, binNet_correct _ hb.idx_len hb.val_len]407  exact mhBin_outcomes hr hP hw408409theorem mhNet_res {B N r : Nat} (hr : N ≤ 2 ^ r) :410    NetValid 1 (mhNet B N r) ∧ Wired (B * N + B) (mhNet B N r) ∧ (mhNet B N r).length ≤ 2 * 19 + 2 :=411  let h := binNet_res (mhBin_bound (B := B) (N := N) hr)412  ⟨h.1, h.2.1, h.2.2.1⟩413414/-- The π_j policy step as a fixed-scale network on the board wires. -/415def polNet (B N j r : Nat) : List Layer := binNet (polBin B N j r)416417theorem polNet_correct {B N j r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) :418    applyM P (netBinSem (polNet B N j r) N r B (boardBits B P)) = policyStep j P := by419  have hb := polBin_bound (B := B) (N := N) (j := j) hr420  rw [polNet, binNet_correct _ hb.idx_len hb.val_len]421  exact (polBin_correct hr hP hw).2422423theorem polNet_res {B N j r : Nat} (hr : N ≤ 2 ^ r) :424    NetValid 1 (polNet B N j r) ∧ Wired (B * N) (polNet B N j r) ∧ (polNet B N j r).length ≤ 2 * 17 + 2 :=425  let h := binNet_res (polBin_bound (B := B) (N := N) (j := j) hr)426  ⟨h.1, h.2.1, h.2.2.1⟩427428/-- Attainability as fixed-scale networks: exact success 2/(2^B − 1) retained. -/429def attainNet (B N r a0 a1 : Nat) (b : Bool) : List Layer := binNet (attainBin B N r a0 a1 b)430431theorem attainNet_correct {B N r a0 a1 : Nat} (h0 : a0 ≠ 0) (h1 : a1 ≠ 0) (hl0 : a0 < 2 ^ B)432    (hl1 : a1 < 2 ^ B) (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) (b : Bool) :433    netBinSem (attainNet B N r a0 a1 b) N r B (boardBits B P) = attainF a0 a1 P b := by434  have hb := attainBin_bound h0 h1 hl0 hl1 hr b435  rw [attainNet, binNet_correct _ hb.idx_len hb.val_len, ← binReadoutOf_eq]436  exact attainBin_correct h0 h1 hl0 hl1 hr hP hw b437438439/-! ## Axiom audit -/440441#print axioms ofBits_congr442#print axioms outDecode_congr443#print axioms outDecode_eval444#print axioms outAt_res445#print axioms ctrlForms_get446#print axioms ctrlForms_length447#print axioms tstep_eq448#print axioms trun_eq449#print axioms trun_append450#print axioms trun_refines451#print axioms trun_stream452#print axioms tstep_reset453#print axioms trun_games454#print axioms crunStates_prefix455#print axioms trun_states_fit456#print axioms trun_one_board457#print axioms ctrlForms_res458#print axioms ctrlForms_size459#print axioms ctrlNet_res460#print axioms ctrl_counts461#print axioms summaryForms_res462#print axioms summaryForms_length463#print axioms summaryNet_res464#print axioms map_range_eq465#print axioms binNet_correct466#print axioms binNet_res467#print axioms restNet_correct468#print axioms restNet_res469#print axioms mhNet_correct470#print axioms mhNet_res471#print axioms polNet_correct472#print axioms polNet_res473#print axioms attainNet_correct474end ThresholdInst475end NimAudit