PriorityEncoder

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 LocalRestore2import BinaryReadout34/- Phase 5, task 1: an explicit, resource-bounded priority encoder from selection5   readouts (RCirc: valid flag, N candidate flags, B value bits) to the paper's binary6   move format (BCirc: valid flag, r big-endian index bits, B big-endian value bits).7   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.89   Construction (no semantic primitive):10     first_i   = s_i AND (AND_{k<i} NOT s_k)                       (AttainCircuit.firstC)11     index bit q (q < r, weight 2^(r-1-q)) = OR of first_i over i < N with bit r-1-q of i12     valid     = R.valid AND (OR_{i<N} s_i)13     value     = R.val unchanged.14   Correctness holds for EVERY input assignment (several true flags, no true flag,15   invalid readouts, N = 0, N = 1 with zero index width, N not a power of two), under16   the index-width condition N ≤ 2^r.  (The recurrent controller's counter uses the17   stricter N < 2^r, because its counter must also hold the end value N.)18   Resources: depth + 3, every formula of size ≤ 4·U^3 with U = (N+2)(S+2), the same19   input support; total output size ≤ (1 + r + B)·4·U^3. -/2021namespace NimAudit22namespace PriorityEncoder2324open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit25  BinReadout2627/-- first_i over the flag list. -/28def firstF (sel : List Circ) (i : Nat) : Circ := firstC (getC sel) i2930/-- Big-endian index bit q: OR of first_i over the indices i < N whose bit r-1-q is 1. -/31def idxBit (sel : List Circ) (N r q : Nat) : Circ :=32  or (((List.range N).filter (fun i => i.testBit (r - 1 - q))).map (firstF sel))3334/-- THE PRIORITY ENCODER. -/35def encode (R : RCirc) (N r : Nat) : BCirc :=36  ⟨and [R.valid, or ((List.range N).map (getC R.sel))],37   (List.range r).map (idxBit R.sel N r),38   R.val⟩3940/-- Binary-format semantics on an arbitrary input vector (an index ≥ N is invalid);41    on boards this is exactly `BinReadout.binReadoutOf`. -/42def binSem (S : BCirc) (N : Nat) (z : Nat → Bool) : Option (Nat × Nat) :=43  if eval z S.valid then44    if toNatBE (S.idx.map (eval z)) < N then45      some (toNatBE (S.idx.map (eval z)), toNatBE (S.val.map (eval z)))46    else none47  else none4849theorem binReadoutOf_eq (B N : Nat) (R : Bool → BCirc) (P : List Nat) (b : Bool) :50    binReadoutOf B N R P b = binSem (R b) N (boardBits B P) := rfl5152theorem flags_eq (sel : List Circ) (N : Nat) (hlen : sel.length = N) (z : Nat → Bool) :53    (List.range N).map (fun i => eval z (getC sel i)) = sel.map (eval z) := by54  apply List.ext_getElem55  · simp [hlen]56  · intro n h1 h257    simp only [List.getElem_map, List.getElem_range, eval_getC]58    simp only [List.getD_eq_getElem?_getD, List.getElem?_map]59    rw [List.getElem?_eq_getElem (by simp at h2; omega)]60    rfl6162theorem firstF_eval (sel : List Circ) {N : Nat} (hlen : sel.length = N) (z : Nat → Bool) {i : Nat}63    (hi : i < N) : eval z (firstF sel i) = decide (firstTrue (sel.map (eval z)) = some i) := by64  unfold firstF65  rw [firstC_eval (N := N) z (getC sel) hi, flags_eq sel N hlen z]6667/-- PRIORITY-ENCODER CORRECTNESS, for every input assignment: the binary output decodes68    to exactly the selection readout (first true flag, value bits), and to `none` when69    the readout is invalid or no flag is true. -/70theorem encode_correct (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (hr : N ≤ 2 ^ r)71    (z : Nat → Bool) : binSem (encode R N r) N z = selReadout R z := by72  unfold binSem selReadout encode73  simp only74  by_cases hv : eval z R.valid = true75  · cases hft : firstTrue (R.sel.map (eval z)) with76    | none =>77      have hany : (R.sel.map (eval z)).any id = false := by78        have := firstTrue_isSome (R.sel.map (eval z)); rw [hft] at this; simpa using this.symm79      have hor : eval z (or ((List.range N).map (getC R.sel))) = false := by80        rw [eval_or, List.any_map]81        have e : ((List.range N).any (eval z ∘ getC R.sel)) = (R.sel.map (eval z)).any id := by82          rw [← flags_eq R.sel N hlen z, List.any_map]; rfl83        rw [e, hany]84      simp [hv, hor]85    | some i =>86      have hiN : i < N := by have := firstTrue_lt hft; simpa [hlen] using this87      have hflag : (R.sel.map (eval z)).getD i false = true := ((firstTrue_some_iff _ i).1 hft).2.188      have hor : eval z (or ((List.range N).map (getC R.sel))) = true := by89        rw [eval_or, List.any_map]90        apply List.any_eq_true.mpr91        exact ⟨i, List.mem_range.mpr hiN, by simp only [Function.comp_apply, eval_getC]; exact hflag⟩92      have hidx : toNatBE (((List.range r).map (idxBit R.sel N r)).map (eval z)) = i := by93        rw [List.map_map]94        apply toNatBE_of_bits (Nat.lt_of_lt_of_le hiN hr)95        intro q _96        simp only [Function.comp_apply]97        apply Bool.eq_iff_iff.mpr98        simp only [idxBit, eval_or, List.any_map, List.any_eq_true, List.mem_filter, List.mem_range,99          Function.comp_apply]100        constructor101        · rintro ⟨i', ⟨hi', hb⟩, he⟩102          rw [firstF_eval R.sel hlen z hi', hft, decide_eq_true_iff] at he103          cases he; exact hb104        · intro hb105          exact ⟨i, ⟨hiN, hb⟩, by rw [firstF_eval R.sel hlen z hiN, hft]; simp⟩106      simp only [eval_and, List.all_cons, List.all_nil, hv, hor, Bool.and_true, if_true, hidx, hiN]107  · simp [hv]108109/-! ## Resources -/110111/-- Resource bounds for binary readout formulas on an arbitrary input support M. -/112structure BinBound (S : BCirc) (N B r D Sz M : Nat) : Prop where113  idx_len : S.idx.length = r114  val_len : S.val.length = B115  width : N ≤ 2 ^ r116  all : ∀ c ∈ S.valid :: (S.idx ++ S.val), depth c ≤ D ∧ size c ≤ Sz ∧ maxInput c ≤ M117118/-- Total formula size of a binary readout (no sharing between output formulas). -/119def totalSize (S : BCirc) : Nat := size S.valid + (S.idx.map size).sum + (S.val.map size).sum120121theorem totalSize_le {S : BCirc} {N B r D Sz M : Nat} (h : BinBound S N B r D Sz M) :122    totalSize S ≤ (1 + r + B) * Sz := by123  unfold totalSize124  have h1 := (h.all S.valid (by simp)).2.1125  have h2 := sum_le_len_mul (cs := S.idx) (S := Sz) (fun c hc => (h.all c (by simp [hc])).2.1)126  have h3 := sum_le_len_mul (cs := S.val) (S := Sz) (fun c hc => (h.all c (by simp [hc])).2.1)127  rw [h.idx_len] at h2; rw [h.val_len] at h3128  rw [Nat.add_mul, Nat.add_mul, Nat.one_mul]129  omega130131/-- ENCODER RESOURCES: from source formulas of depth ≤ D, size ≤ S on inputs below M,132    every output formula has depth ≤ D + 3, size ≤ 4·((N+2)(S+2))^3 and inputs below M. -/133theorem encode_bound (R : RCirc) {N B r D S M : Nat} (hlen : R.sel.length = N) (hvl : R.val.length = B)134    (hr : N ≤ 2 ^ r)135    (hall : ∀ c ∈ R.valid :: (R.sel ++ R.val), depth c ≤ D ∧ size c ≤ S ∧ maxInput c ≤ M) :136    BinBound (encode R N r) N B r (D + 3) (4 * ((N + 2) * (S + 2)) ^ 3) M := by137  generalize hU : (N + 2) * (S + 2) = U138  have hNU : N + 2 ≤ U := by139    rw [← hU]; exact Nat.le_mul_of_pos_right (N + 2) (by omega)140  have hSU : S + 2 ≤ U := by141    rw [← hU]; exact Nat.le_mul_of_pos_left (S + 2) (by omega)142  have hU1 : 1 ≤ U := by omega143  have hsel : ∀ i < N, depth (getC R.sel i) ≤ D ∧ size (getC R.sel i) ≤ S ∧ maxInput (getC R.sel i) ≤ M :=144    fun i hi => hall _ (by simp [getC_mem (show i < R.sel.length by omega)])145  have hsel1 : ∀ i < N, size (getC R.sel i) ≤ 1 * U ^ 1 := fun i hi => by146    have := (hsel i hi).2.1; simp; omega147  have hF : ∀ i < N, depth (firstF R.sel i) ≤ D + 2 ∧ size (firstF R.sel i) ≤ 3 * U ^ 2 ∧148      maxInput (firstF R.sel i) ≤ M := by149    intro i hi150    refine ⟨dp_firstC (fun i' hi' => (hsel i' (by omega)).1),151      sz_firstC hU1 (by omega) (fun i' hi' => hsel1 i' (by omega)),152      mx_firstC (fun i' hi' => (hsel i' (by omega)).2.2)⟩153  refine ⟨by simp [encode], by simp [encode, hvl], hr, ?_⟩154  intro c hc155  simp only [encode, List.mem_cons, List.mem_append, List.mem_map, List.mem_range] at hc156  rcases hc with rfl | ⟨q, _, rfl⟩ | hcv157  · -- validity158    have hv := hall R.valid (by simp)159    refine ⟨?_, ?_, ?_⟩160    · apply depth_and_le; intro c hc161      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc162      rcases hc with rfl | rfl163      · omega164      · apply depth_or_le; intro c hc165        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc166        have := (hsel i (List.mem_range.mp hi)).1; omega167    · apply size_and_le hU1 (by simp; omega)168      intro c hc169      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc170      rcases hc with rfl | rfl171      · exact lift1 hU1 (show size R.valid ≤ 1 * U ^ 1 by simp; omega) (by omega) (by omega)172      · exact lift1 hU1 (size_or_le hU1 (by simp; omega) (fun c hc => by173          obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact hsel1 i (List.mem_range.mp hi)))174          (by omega) (by omega)175    · apply ControllerBits.maxInput_and_le; intro c hc176      simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] at hc177      rcases hc with rfl | rfl178      · exact hv.2.2179      · apply ControllerBits.maxInput_or_le; intro c hc180        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc181        exact (hsel i (List.mem_range.mp hi)).2.2182  · -- index bit q183    refine ⟨?_, ?_, ?_⟩184    · unfold idxBit; apply depth_or_le; intro c hc185      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc186      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).1187    · unfold idxBit188      apply size_or_le hU1 (by189        have := List.length_filter_le (fun i => i.testBit (r - 1 - q)) (List.range N)190        simp only [List.length_map, List.length_range] at this ⊢; omega)191      intro c hc192      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc193      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).2.1194    · unfold idxBit; apply ControllerBits.maxInput_or_le; intro c hc195      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc196      exact (hF i (List.mem_range.mp (List.mem_filter.mp hi).1)).2.2197  · -- value bit (unchanged)198    have h := hall c (by simp [hcv])199    refine ⟨by omega, ?_, h.2.2⟩200    exact lift1 hU1 (show size c ≤ 1 * U ^ 1 by simp; omega) (by omega) (by omega)201202/-- From the phase-4 selector bound. -/203theorem encode_bound_sel {R : RCirc} {N B D S M r : Nat} (h : SelBound R N B D S M) (hr : N ≤ 2 ^ r) :204    BinBound (encode R N r) N B r (D + 3) (4 * ((N + 2) * (S + 2)) ^ 3) M :=205  encode_bound R h.1 h.2.1 hr h.2.2206207/-- From the phase-3 readout bound (inputs = the B·N board bits). -/208theorem encode_bound_R {R : RCirc} {N B d s r : Nat} (h : RBound R N B d s) (hr : N ≤ 2 ^ r) :209    BinBound (encode R N r) N B r (d + 3) (4 * ((N + 2) * (s + 2)) ^ 3) (B * N) := by210  apply encode_bound R h.sel_len h.val_len hr211  intro c hc212  simp only [List.mem_cons, List.mem_append] at hc213  rcases hc with rfl | hc | hc214  · exact ⟨h.depth_valid, h.size_valid, h.max_valid⟩215  · exact ⟨h.depth_sel c hc, h.size_sel c hc, h.max_sel c hc⟩216  · exact ⟨h.depth_val c hc, h.size_val c hc, h.max_val c hc⟩217218/-- A board-input binary bound is a `BinReadout.BBound`. -/219theorem bbound_of_bin {S : BCirc} {N B r D Sz : Nat} (h : BinBound S N B r D Sz (B * N)) :220    BBound S N B r D Sz := by221  refine ⟨h.idx_len, h.val_len, h.width, (h.all _ (by simp)).1, fun c hc => (h.all c (by simp [hc])).1,222    fun c hc => (h.all c (by simp [hc])).1, (h.all _ (by simp)).2.1,223    fun c hc => (h.all c (by simp [hc])).2.1, fun c hc => (h.all c (by simp [hc])).2.1,224    (h.all _ (by simp)).2.2, fun c hc => (h.all c (by simp [hc])).2.2, fun c hc => (h.all c (by simp [hc])).2.2⟩225226/-- Every N has an adequate index width: r = log₂N + 1 gives N ≤ 2^r (r = 0 suffices227    for N ≤ 1). -/228theorem width_log (N : Nat) : N ≤ 2 ^ (N.log2 + 1) := Nat.le_of_lt Nat.lt_log2_self229230theorem width_small {N : Nat} (h : N ≤ 1) : N ≤ 2 ^ 0 := by simpa using h231232/-! ## Instances -/233234/-- (a) Attainability: the binary readout circuits of the fibre-guess selector. -/235def attainBin (B N r a0 a1 : Nat) : Bool → BCirc := fun b => encode (attR B N a0 a1 b) N r236237theorem attainBin_correct {B N r a0 a1 : Nat} (h0 : a0 ≠ 0) (h1 : a1 ≠ 0) (hl0 : a0 < 2 ^ B)238    (hl1 : a1 < 2 ^ B) (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) (b : Bool) :239    binReadoutOf B N (attainBin B N r a0 a1) P b = attainF a0 a1 P b := by240  rw [binReadoutOf_eq, attainBin, encode_correct _ N r (by simp [attR, attRC]) hr, ← readoutOf_eq,241    attR_correct h0 h1 hl0 hl1 hP hw]242243theorem attainBin_bound {B N r a0 a1 : Nat} (h0 : a0 ≠ 0) (h1 : a1 ≠ 0) (hl0 : a0 < 2 ^ B)244    (hl1 : a1 < 2 ^ B) (hr : N ≤ 2 ^ r) (b : Bool) :245    BBound (attainBin B N r a0 a1 b) N B r (9 + 3) (4 * ((N + 2) * (10 * Ua N B ^ 8 + 2)) ^ 3) := by246  apply bbound_of_bin247  apply encode_bound_R _ hr248  unfold attR249  cases b250  · exact attRC_RBound h0 hl0251  · exact attRC_RBound h1 hl1252253theorem succCountRO_boards {B N j : Nat} {F G : Readout}254    (h : ∀ P, P.length = N → Width B P → ∀ b, F P b = G P b) :255    succCountRO B N F j = succCountRO B N G j := by256  unfold succCountRO successB257  apply rsum_congr; intro P hP258  obtain ⟨hlen, hw⟩ := mem_boards hP259  rw [h P hlen hw]260261/-- EXACT ATTAINABILITY IN THE BINARY FORMAT: the explicit binary circuits for the least262    fibre representatives, fed the executed rollout outcome RO_{π_j}, succeed with263    conditional probability exactly 2/(2^B − 1). -/264theorem attainBin_exact {B N j r : Nat} (hB : 2 ≤ B) (hj : j < B) (hr : N + 1 ≤ 2 ^ r) :265    succCountRO B (N + 1)266        (binReadoutOf B (N + 1) (attainBin B (N + 1) r (fibreRep B (headVec j) false)267          (fibreRep B (headVec j) true))) j / nonzeroCount B (N + 1) =268      2 / (((2 ^ B : Nat) : Rat) - 1) := by269  have hw0 := headVec_ne_zero j270  have hwl := headVec_lt hj271  obtain ⟨n0, l0, _, _⟩ := fibreRep_spec hB hw0 hwl false272  obtain ⟨n1, l1, _, _⟩ := fibreRep_spec hB hw0 hwl true273  rw [succCountRO_boards (fun P hP hw b => attainBin_correct n0 n1 l0 l1 hr hP hw b)]274  exact attain_exact_head hB hj275276/-- (b) Local two-frame restoration in binary format. -/277def restBin (B N r : Nat) : BCirc := encode (LocalRestore.restC B N) N r278279theorem restBin_correct {B N r : Nat} (hr : N ≤ 2 ^ r) {Q Q' : List Nat} (hQ : Q.length = N)280    (hQ' : Q'.length = N) (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :281    ∃ i v, binSem (restBin B N r) N (LocalRestore.tf B N Q Q') = some (i, v) ∧282      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by283  obtain ⟨i, v, h1, h2, h3, h4⟩ := LocalRestore.restore_equiv hQ hQ' hw hw' h0 hm284  refine ⟨i, v, ?_, h2, h3, h4⟩285  rw [restBin, encode_correct _ N r LocalRestore.restC_bound.1 hr, h1]286287theorem restBin_bound {B N r : Nat} (hr : N ≤ 2 ^ r) :288    BinBound (restBin B N r) N B r (4 + 9 + 4 + 3)289      (4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1) + 2)) ^ 3)290      (2 * (B * N)) :=291  encode_bound_sel LocalRestore.restC_bound hr292293/-- (c) The structured rollout policy π_j in binary format. -/294def polBin (B N j r : Nat) : BCirc := encode (polSel B N j) N r295296theorem polBin_correct {B N j r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) :297    binSem (polBin B N j r) N (boardBits B P) = policyIdx j P ∧298      applyM P (binSem (polBin B N j r) N (boardBits B P)) = policyStep j P := by299  have e : binSem (polBin B N j r) N (boardBits B P) = selReadout (polSel B N j) (boardBits B P) :=300    encode_correct _ N r (polSel_bound (B := B) (N := N) j).1 hr _301  rw [e]302  exact polSel_correct hP hw303304theorem polBin_bound {B N j r : Nat} (hr : N ≤ 2 ^ r) :305    BinBound (polBin B N j r) N B r (5 + 9 + 3)306      (4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (4 * B + 9 + 2)) ^ 8 + 2)) ^ 3) (B * N) :=307  encode_bound_sel (polSel_bound j) hr308309/-- (d) The multi-head selector in binary format. -/310def mhBin (B N r : Nat) : BCirc := encode (mhSel B N) N r311312theorem mhBin_correct {B N r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)313    (o : Nat → Bool) :314    binSem (mhBin B N r) N (obsIn B N P o) = attainT (reconstruct B o) P := by315  rw [mhBin, encode_correct _ N r (mhSel_bound (B := B) (N := N)).1 hr, mhSel_correct hP hw]316317theorem mhBin_outcomes {B N r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P) :318    binSem (mhBin B N r) N (obsIn B N P (outcomes P)) = Controller.decisionMove P := by319  rw [mhBin, encode_correct _ N r (mhSel_bound (B := B) (N := N)).1 hr, mhSel_outcomes hP hw]320321theorem mhBin_bound {B N r : Nat} (hr : N ≤ 2 ^ r) :322    BinBound (mhBin B N r) N B r (4 + 9 + 3 + 3)323      (4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (9 + 1) + 2)) ^ 3)324      (B * N + B) :=325  encode_bound_sel mhSel_bound hr326327/-- The variable-target selector in binary format (σ on wires B·N …). -/328def varBin (B N r : Nat) : BCirc := encode (varSel B N) N r329330theorem varBin_correct {B N r : Nat} (hr : N ≤ 2 ^ r) {P : List Nat} (hP : P.length = N) (hw : Width B P)331    {σ : Nat} (hσ : σ < 2 ^ B) :332    binSem (varBin B N r) N (selIn B N P σ) = attainT σ P := by333  rw [varBin, encode_correct _ N r (varSel_bound (B := B) (N := N)).1 hr, varSel_correct hP hw hσ]334335/-! ## Edge cases (all instances of `encode_correct`) -/336337/-- Invalid source readout: no move. -/338theorem encode_invalid (R : RCirc) (N r : Nat) (z : Nat → Bool) (hv : eval z R.valid = false) :339    binSem (encode R N r) N z = none := by340  simp [binSem, encode, hv]341342/-- No true candidate flag: no move (even if the source valid flag is true). -/343theorem encode_noflag (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (z : Nat → Bool)344    (hno : ∀ i < N, eval z (getC R.sel i) = false) : binSem (encode R N r) N z = none := by345  have hor : eval z (or ((List.range N).map (getC R.sel))) = false := by346    rw [eval_or, List.any_map]; apply List.any_eq_false.mpr347    intro i hi; simpa using hno i (List.mem_range.mp hi)348  simp [binSem, encode, hor]349350/-- Several true flags: the encoded index is the least true one. -/351theorem encode_least (R : RCirc) (N r : Nat) (hlen : R.sel.length = N) (hr : N ≤ 2 ^ r) (z : Nat → Bool)352    (hv : eval z R.valid = true) {i : Nat} (hi : i < N) (hti : eval z (getC R.sel i) = true)353    (hlow : ∀ k < i, eval z (getC R.sel k) = false) :354    binSem (encode R N r) N z = some (i, toNatBE (R.val.map (eval z))) := by355  rw [encode_correct R N r hlen hr z]356  have hft : firstTrue (R.sel.map (eval z)) = some i := by357    rw [firstTrue_some_iff]358    refine ⟨by simp [hlen, hi], ?_, ?_⟩359    · rw [← eval_getC]; exact hti360    · intro k hk; rw [← eval_getC]; exact hlow k hk361  simp [selReadout, hv, hft]362363/-- N = 0: never a move, for any index width. -/364theorem encode_zero (R : RCirc) (r : Nat) (hlen : R.sel.length = 0) (z : Nat → Bool) :365    binSem (encode R 0 r) 0 z = none :=366  encode_noflag R 0 r hlen z (fun i hi => absurd hi (by omega))367368/-- N = 1 with zero index width (r = 0): the index list is empty and decodes to 0. -/369theorem encode_one (R : RCirc) (hlen : R.sel.length = 1) (z : Nat → Bool) :370    (encode R 1 0).idx = [] ∧ binSem (encode R 1 0) 1 z = selReadout R z :=371  ⟨rfl, encode_correct R 1 0 hlen (by decide) z⟩372373/-- BINARY SHARPNESS: the explicit binary circuits for the least fibre representatives374    succeed with exactly 2/(2^B − 1), satisfy BBound (depth 12, size375    4((N+3)(10·Ua(N+1) B^8 + 2))^3, r index bits), and under the parity-correlation376    premise every binary readout with the same bounds succeeds with at most377    2/(2^B − 1) + (2^B − 1)ε. -/378theorem attainBin_sharp {B N j r : Nat} (hB : 2 ≤ B) (hj : j < B) (hr : N + 1 ≤ 2 ^ r) {ε : Rat}379    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →380      ParityCorrPremise (9 + 3 + 2 + 11)381        (12 * Upar (N + 1) B ((r + 1) * (4 * ((N + 1 + 2) * (10 * Ua (N + 1) B ^ 8 + 2)) ^ 3 + 1)) ^ 10) m ε) :382    (∀ b, BBound (attainBin B (N + 1) r (fibreRep B (headVec j) false) (fibreRep B (headVec j) true) b)383      (N + 1) B r (9 + 3) (4 * ((N + 1 + 2) * (10 * Ua (N + 1) B ^ 8 + 2)) ^ 3)) ∧384    succCountRO B (N + 1)385        (binReadoutOf B (N + 1) (attainBin B (N + 1) r (fibreRep B (headVec j) false)386          (fibreRep B (headVec j) true))) j / nonzeroCount B (N + 1) = 2 / (((2 ^ B : Nat) : Rat) - 1) ∧387    (∀ R : Bool → BCirc, (∀ b, BBound (R b) (N + 1) B r (9 + 3) (4 * ((N + 1 + 2) * (10 * Ua (N + 1) B ^ 8 + 2)) ^ 3)) →388      succCountRO B (N + 1) (binReadoutOf B (N + 1) R) j / nonzeroCount B (N + 1) ≤389        2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε) := by390  have hw0 := headVec_ne_zero j391  have hwl := headVec_lt hj392  obtain ⟨n0, l0, _, _⟩ := fibreRep_spec hB hw0 hwl false393  obtain ⟨n1, l1, _, _⟩ := fibreRep_spec hB hw0 hwl true394  exact ⟨fun b => attainBin_bound n0 n1 l0 l1 hr b, attainBin_exact hB hj hr,395    fun R hR => binary_readout_bound hj R hR hprem⟩396397398/-! ## Axiom audit -/399400#print axioms binReadoutOf_eq401#print axioms flags_eq402#print axioms firstF_eval403#print axioms encode_correct404#print axioms totalSize_le405#print axioms encode_bound406#print axioms encode_bound_sel407#print axioms encode_bound_R408#print axioms bbound_of_bin409#print axioms width_log410#print axioms width_small411#print axioms attainBin_correct412#print axioms attainBin_bound413#print axioms succCountRO_boards414#print axioms attainBin_exact415#print axioms restBin_correct416#print axioms restBin_bound417#print axioms polBin_correct418#print axioms polBin_bound419#print axioms mhBin_correct420#print axioms mhBin_outcomes421#print axioms mhBin_bound422#print axioms varBin_correct423#print axioms encode_invalid424#print axioms encode_noflag425#print axioms encode_least426#print axioms encode_zero427#print axioms encode_one428#print axioms attainBin_sharp429end PriorityEncoder430end NimAudit