BinaryReadout

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 FiniteNet2import NimCorrBridge34/- Phase 4, Priority 2a: binary-index readouts.  Written by Claude (10 October 2026).5   Lean 4.26.0, core/Std only.67   The paper's readout outputs a move as (valid bit, binary heap index, binary new8   value).  `BCirc` packages formulas for these bits; `binReadoutOf` is the induced9   phase-2 Readout (an index ≥ N is an invalid move).  An equality decoder turns the10   r index bits into N selection formulas; we prove agreement with the binary11   semantics for every encoding (valid indices, out-of-range indices, N = 0, N = 1),12   given only that the index width suffices (N ≤ 2^r).  Resources propagate to the13   phase-3 `RBound`, so `circuit_readout_bound` applies.  Finally, readouts computed14   by threshold networks are compiled with the repaired finite-input compiler15   (FiniteNet.netFormula) and the conditional success bound is stated for them. -/1617namespace NimAudit18namespace BinReadout1920open Prob AC0 AC0.Circ Game Bridge Rollout CorrBridge FiniteNet2122attribute [local simp] Rat.add_zero Rat.zero_add2324/-- Binary readout formulas for one observed bit. -/25structure BCirc where26  valid : Circ27  idx : List Circ28  val : List Circ2930/-- The readout defined by binary readout formulas (index ≥ N is invalid). -/31def binReadoutOf (B N : Nat) (R : Bool → BCirc) : Readout := fun P b =>32  if eval (boardBits B P) (R b).valid then33    if toNatBE ((R b).idx.map (eval (boardBits B P))) < N then34      some (toNatBE ((R b).idx.map (eval (boardBits B P))),35        toNatBE ((R b).val.map (eval (boardBits B P))))36    else none37  else none3839def litEq (c : Circ) (bit : Bool) : Circ := if bit then c else not c4041/-- Equality decoder: the r index bits encode i (big-endian). -/42def decodeC (idx : List Circ) (i : Nat) : Circ :=43  and ((List.range idx.length).map (fun q => litEq (getC idx q) (i.testBit (idx.length - 1 - q))))4445/-- Adapter to the phase-3 selection-formula interface. -/46def toRCirc (N : Nat) (R : BCirc) : RCirc := ⟨R.valid, (List.range N).map (decodeC R.idx), R.val⟩4748theorem toNatBE_eq_iff (v : List Bool) {i : Nat} (hi : i < 2 ^ v.length) :49    toNatBE v = i ↔ ∀ q < v.length, v.getD q false = i.testBit (v.length - 1 - q) := by50  constructor51  · intro h q hq52    rw [← h, testBit_toNatBE v q hq]53  · intro h54    apply Nat.eq_of_testBit_eq55    intro k56    rcases Nat.lt_or_ge k v.length with hk | hk57    · have := testBit_toNatBE v (v.length - 1 - k) (by omega)58      rw [show v.length - 1 - (v.length - 1 - k) = k by omega] at this59      rw [this, h _ (by omega), show v.length - 1 - (v.length - 1 - k) = k by omega]60    · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le (toNatBE_lt v) (Nat.pow_le_pow_right (by decide) hk)),61        Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hi (Nat.pow_le_pow_right (by decide) hk))]6263/-- DECODER SEMANTICS: for i < 2^r the decoder fires iff the index bits encode i. -/64theorem decodeC_eval (z : Nat → Bool) (idx : List Circ) {i : Nat} (hi : i < 2 ^ idx.length) :65    eval z (decodeC idx i) = decide (toNatBE (idx.map (eval z)) = i) := by66  have hl : (idx.map (eval z)).length = idx.length := by simp67  apply Bool.eq_iff_iff.mpr68  rw [decide_eq_true_iff, toNatBE_eq_iff _ (by rw [hl]; exact hi), hl]69  unfold decodeC70  simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp]71  have hg : ∀ q, q < idx.length → eval z (getC idx q) = (idx.map (eval z)).getD q false := by72    intro q _; rw [eval_getC]73  constructor74  · intro h q hq75    have := h q hq76    rw [← hg q hq]77    unfold litEq at this78    split at this79    · next hb => rw [hb]; exact this80    · next hb => simp only [eval_not, Bool.not_eq_true'] at this; rw [this]; simpa using hb81  · intro h q hq82    have := h q hq83    rw [← hg q hq] at this84    unfold litEq85    split86    · next hb => rw [this, hb]87    · next hb => simp only [eval_not, Bool.not_eq_true']; rw [this]; simpa using hb8889theorem firstTrue_eqs (N v : Nat) :90    firstTrue ((List.range N).map (fun i => decide (v = i))) = if v < N then some v else none := by91  by_cases hv : v < N92  · simp only [hv, if_true]93    rw [firstTrue_some_iff]94    simp only [List.length_map, List.length_range]95    refine ⟨hv, ?_, ?_⟩96    · simp [List.getD_eq_getElem?_getD, List.getElem?_range hv]97    · intro i hi98      simp [List.getD_eq_getElem?_getD, List.getElem?_range (show i < N by omega)]; omega99  · simp only [hv, if_false]100    cases hf : firstTrue ((List.range N).map (fun i => decide (v = i))) with101    | none => rfl102    | some i =>103      exfalso104      obtain ⟨hl, hb, _⟩ := (firstTrue_some_iff _ i).1 hf105      simp only [List.length_map, List.length_range] at hl106      simp [List.getD_eq_getElem?_getD, List.getElem?_range hl] at hb107      omega108109/-- ADAPTER CORRECTNESS: with index width N ≤ 2^r, the selection-formula readout of110    the decoded circuits equals the binary readout on every board (all encodings,111    including out-of-range indices and N = 0, 1). -/112theorem toRCirc_correct (B N : Nat) (R : Bool → BCirc) (hN : ∀ b, N ≤ 2 ^ (R b).idx.length)113    (P : List Nat) (b : Bool) :114    readoutOf B (fun b => toRCirc N (R b)) P b = binReadoutOf B N R P b := by115  unfold readoutOf binReadoutOf toRCirc116  simp only117  have hsel : ((List.range N).map (decodeC (R b).idx)).map (eval (boardBits B P)) =118      (List.range N).map (fun i => decide (toNatBE ((R b).idx.map (eval (boardBits B P))) = i)) := by119    rw [List.map_map]120    apply List.map_congr_left121    intro i hi122    exact decodeC_eval _ _ (Nat.lt_of_lt_of_le (List.mem_range.mp hi) (hN b))123  rw [hsel, firstTrue_eqs]124  by_cases hv : eval (boardBits B P) (R b).valid = true125  · simp only [hv, if_true]126    by_cases hlt : toNatBE ((R b).idx.map (eval (boardBits B P))) < N127    · simp [hlt]128    · simp [hlt]129  · simp [hv]130131/-- Resource bounds for binary readout formulas. -/132structure BBound (R : BCirc) (N B r d s : Nat) : Prop where133  idx_len : R.idx.length = r134  val_len : R.val.length = B135  width : N ≤ 2 ^ r136  depth_valid : depth R.valid ≤ d137  depth_idx : ∀ c ∈ R.idx, depth c ≤ d138  depth_val : ∀ c ∈ R.val, depth c ≤ d139  size_valid : size R.valid ≤ s140  size_idx : ∀ c ∈ R.idx, size c ≤ s141  size_val : ∀ c ∈ R.val, size c ≤ s142  max_valid : maxInput R.valid ≤ B * N143  max_idx : ∀ c ∈ R.idx, maxInput c ≤ B * N144  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N145146theorem getC_mem {cs : List Circ} {q : Nat} (hq : q < cs.length) : getC cs q ∈ cs := by147  unfold getC148  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hq]149  simp150151/-- DECODER RESOURCES: depth ≤ d + 2, size ≤ r (s+1) + 1, inputs as the index formulas. -/152theorem decodeC_resources {R : BCirc} {N B r d s : Nat} (hb : BBound R N B r d s) (i : Nat) :153    depth (decodeC R.idx i) ≤ d + 2 ∧ size (decodeC R.idx i) ≤ r * (s + 1) + 1 ∧154    maxInput (decodeC R.idx i) ≤ B * N := by155  have hlit : ∀ q, q < R.idx.length → ∀ bit,156      depth (litEq (getC R.idx q) bit) ≤ d + 1 ∧ size (litEq (getC R.idx q) bit) ≤ s + 1 ∧157      maxInput (litEq (getC R.idx q) bit) ≤ B * N := by158    intro q hq bit159    have hm := getC_mem hq160    unfold litEq161    split162    · exact ⟨by have := hb.depth_idx _ hm; omega, by have := hb.size_idx _ hm; omega, hb.max_idx _ hm⟩163    · simp only [depth_not, size_not, maxInput_not]164      exact ⟨by have := hb.depth_idx _ hm; omega, by have := hb.size_idx _ hm; omega, hb.max_idx _ hm⟩165  unfold decodeC166  refine ⟨?_, ?_, ?_⟩167  · apply depth_and_le168    intro c hc169    obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc170    exact (hlit q (List.mem_range.mp hq) _).1171  · simp only [size_and]172    have h := sum_le_len_mul (cs := (List.range R.idx.length).map173      (fun q => litEq (getC R.idx q) (i.testBit (R.idx.length - 1 - q)))) (S := s + 1) (by174        intro c hc175        obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc176        exact (hlit q (List.mem_range.mp hq) _).2.1)177    simp only [List.length_map, List.length_range] at h178    rw [hb.idx_len] at h ⊢179    omega180  · simp only [maxInput_and]181    apply listMax_le182    intro a ha183    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha184    obtain ⟨q, hq, rfl⟩ := List.mem_map.mp hc185    exact (hlit q (List.mem_range.mp hq) _).2.2186187/-- The adapted circuits satisfy the phase-3 resource bounds with188    d' = d + 2 and s' = (r+1)(s+1). -/189theorem toRCirc_RBound {R : BCirc} {N B r d s : Nat} (hb : BBound R N B r d s) :190    RBound (toRCirc N R) N B (d + 2) ((r + 1) * (s + 1)) := by191  have hs : s ≤ (r + 1) * (s + 1) := by192    have := Nat.le_mul_of_pos_left (s + 1) (show 0 < r + 1 by omega); omega193  have hd : r * (s + 1) + 1 ≤ (r + 1) * (s + 1) := by rw [Nat.add_mul, Nat.one_mul]; omega194  refine ⟨by simp [toRCirc], hb.val_len, by have := hb.depth_valid; simp [toRCirc]; omega, ?_, ?_,195    Nat.le_trans hb.size_valid hs, ?_, ?_, hb.max_valid, ?_, hb.max_val⟩196  · intro c hc; simp only [toRCirc, List.mem_map, List.mem_range] at hc197    obtain ⟨i, _, rfl⟩ := hc; exact (decodeC_resources hb i).1198  · intro c hc; have := hb.depth_val c hc; simp only [toRCirc] at hc; omega199  · intro c hc; simp only [toRCirc, List.mem_map, List.mem_range] at hc200    obtain ⟨i, _, rfl⟩ := hc; exact Nat.le_trans (decodeC_resources hb i).2.1 hd201  · intro c hc; exact Nat.le_trans (hb.size_val c hc) hs202  · intro c hc; simp only [toRCirc, List.mem_map, List.mem_range] at hc203    obtain ⟨i, _, rfl⟩ := hc; exact (decodeC_resources hb i).2.2204205/-- The phase-2 success count only depends on the readout function. -/206theorem succCountRO_congr {B N j : Nat} {F G : Readout} (h : ∀ P b, F P b = G P b) :207    succCountRO B N F j = succCountRO B N G j := by208  unfold succCountRO successB209  apply rsum_congr; intro P _210  rw [h]211212/-- CONDITIONAL BOUND FOR BINARY READOUTS: binary readout formulas with BBound213    (depth ≤ d, size ≤ s, r index bits, N+1 ≤ 2^r) fed RO_{pi_j} succeed with214    conditional probability ≤ 2/(q-1) + (q-1) ε, under the parity-correlation215    premise for depth d + 13 and size 12 U^10, U = (N+3)(B+2)((r+1)(s+1)+2). -/216theorem binary_readout_bound {B N j r d s : Nat} (hj : j < B) (R : Bool → BCirc)217    (hb : ∀ b, BBound (R b) (N + 1) B r d s) {ε : Rat}218    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →219      ParityCorrPremise (d + 2 + 11) (12 * Upar (N + 1) B ((r + 1) * (s + 1)) ^ 10) m ε) :220    succCountRO B (N + 1) (binReadoutOf B (N + 1) R) j / nonzeroCount B (N + 1) ≤221      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε := by222  have hN : ∀ b, N + 1 ≤ 2 ^ (R b).idx.length := fun b => by rw [(hb b).idx_len]; exact (hb b).width223  rw [← succCountRO_congr (fun P b => toRCirc_correct B (N + 1) R hN P b)]224  exact circuit_readout_bound hj _ (fun b => toRCirc_RBound (hb b)) hprem225226/-! ## Readouts computed by threshold networks -/227228/-- Output layout of a readout network: output 0 = valid, outputs 1..r = index bits,229    outputs r+1..r+B = value bits; compiled with the finite-input compiler on the230    B·N board bits. -/231def netBCirc (W B N r : Nat) (ls : List Layer) : BCirc :=232  ⟨netFormula W (B * N) ls 0, (List.range r).map (fun q => netFormula W (B * N) ls (1 + q)),233   (List.range B).map (fun p => netFormula W (B * N) ls (1 + r + p))⟩234235/-- boardBits vanishes beyond B·|P|, so zero-extension at B·N is invisible. -/236theorem pad_boardBits {B N : Nat} {P : List Nat} (hP : P.length = N) :237    pad (B * N) (boardBits B P) = boardBits B P := by238  funext j239  unfold pad240  by_cases hj : j < B * N241  · simp [hj]242  · simp only [hj, if_false]243    unfold boardBits244    rw [hP]; simp [hj]245246/-- On boards of N heaps the compiled formulas compute the network on the board bits. -/247theorem netBCirc_eval {W B N : Nat} (ls : List Layer) (hv : NetValid W ls) {P : List Nat}248    (hP : P.length = N) (o : Nat) :249    eval (boardBits B P) (netFormula W (B * N) ls o) = evalNet ls (boardBits B P) o := by250  unfold netFormula251  rw [eval_compileNet ls hv]252  have : (fun j => eval (boardBits B P) (clip (B * N) j)) = boardBits B P := by253    funext j; rw [eval_clip, pad_boardBits (B := B) hP]254  rw [this]255256/-- Semantics of a network readout on boards of N heaps. -/257theorem netReadout_eq {W B N r : Nat} (nets : Bool → List Layer) (hv : ∀ b, NetValid W (nets b))258    {P : List Nat} (hP : P.length = N) (b : Bool) :259    binReadoutOf B N (fun b => netBCirc W B N r (nets b)) P b =260      if evalNet (nets b) (boardBits B P) 0 then261        if toNatBE ((List.range r).map (fun q => evalNet (nets b) (boardBits B P) (1 + q))) < N then262          some (toNatBE ((List.range r).map (fun q => evalNet (nets b) (boardBits B P) (1 + q))),263            toNatBE ((List.range B).map (fun p => evalNet (nets b) (boardBits B P) (1 + r + p))))264        else none265      else none := by266  unfold binReadoutOf netBCirc267  simp only [List.map_map, Function.comp_def]268  rw [netBCirc_eval _ (hv b) hP]269  have e1 : (fun q => eval (boardBits B P) (netFormula W (B * N) (nets b) (1 + q))) =270      (fun q => evalNet (nets b) (boardBits B P) (1 + q)) := by271    funext q; exact netBCirc_eval _ (hv b) hP _272  have e2 : (fun p => eval (boardBits B P) (netFormula W (B * N) (nets b) (1 + r + p))) =273      (fun p => evalNet (nets b) (boardBits B P) (1 + r + p)) := by274    funext p; exact netBCirc_eval _ (hv b) hP _275  rw [e1, e2]276277/-- Network readouts satisfy BBound with depth 3L and size 2 (2W+3)^L (M+1)^(WL). -/278theorem netBCirc_BBound {W M B N r : Nat} (ls : List Layer) (hv : NetValid W ls)279    (hb : NetBounded M ls) (hr : N ≤ 2 ^ r) :280    BBound (netBCirc W B N r ls) N B r (3 * ls.length)281      (2 * ((2 * W + 3) ^ ls.length * (M + 1) ^ (W * ls.length))) := by282  have sp := fun o => netFormula_spec (B * N) ls hv hb o283  refine ⟨by simp [netBCirc], by simp [netBCirc], hr, (sp 0).2.1, ?_, ?_, (sp 0).2.2.1, ?_, ?_,284    (sp 0).2.2.2, ?_, ?_⟩ <;>285  · intro c hc286    simp only [netBCirc, List.mem_map, List.mem_range] at hc287    obtain ⟨q, _, rfl⟩ := hc288    first289      | exact (sp _).2.1290      | exact (sp _).2.2.1291      | exact (sp _).2.2.2292293/-- CONDITIONAL BOUND FOR NETWORK READOUTS.  Two valid L-layer threshold networks294    (one per observed bit) with fan-ins/widths ≤ M, compiled with the finite-input295    compiler on the B·(N+1) board bits and read through the binary decoder296    (r index bits, N+1 ≤ 2^r), succeed when fed RO_{pi_j} with conditional297    probability ≤ 2/(q-1) + (q-1) ε, under the parity-correlation premise for depth298    3L + 13 and size 12 U^10 with U = (N+3)(B+2)((r+1)(s+1)+2),299    s = 2 (2W+3)^L (M+1)^(WL). -/300theorem network_readout_bound {W M B N j r L : Nat} (hj : j < B) (nets : Bool → List Layer)301    (hlen : ∀ b, (nets b).length = L) (hv : ∀ b, NetValid W (nets b))302    (hb : ∀ b, NetBounded M (nets b)) (hr : N + 1 ≤ 2 ^ r) {ε : Rat}303    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →304      ParityCorrPremise (3 * L + 2 + 11)305        (12 * Upar (N + 1) B ((r + 1) * (2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) + 1)) ^ 10) m ε) :306    succCountRO B (N + 1) (binReadoutOf B (N + 1) (fun b => netBCirc W B (N + 1) r (nets b))) j /307        nonzeroCount B (N + 1) ≤308      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε := by309  apply binary_readout_bound hj _ _ hprem310  intro b311  have := netBCirc_BBound (B := B) (N := N + 1) (r := r) (nets b) (hv b) (hb b) hr312  rw [hlen] at this313  exact this314315316/-! ## Axiom audit -/317318#print axioms toNatBE_eq_iff319#print axioms decodeC_eval320#print axioms firstTrue_eqs321#print axioms toRCirc_correct322#print axioms getC_mem323#print axioms decodeC_resources324#print axioms toRCirc_RBound325#print axioms succCountRO_congr326#print axioms binary_readout_bound327#print axioms pad_boardBits328#print axioms netBCirc_eval329#print axioms netReadout_eq330#print axioms netBCirc_BBound331#print axioms network_readout_bound332end BinReadout333end NimAudit