AttainCircuit

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 NimCorrBridge2import NimAttain34/- Phase 3, targets A + D: an explicit circuit realisation of the attainability5   readout, and the resulting CONDITIONAL sharpness.  Written by Claude6   (10 October 2026).  Lean 4.26.0, core/Std only.78   For a nonzero guess t < 2^B with top bit k = log2 t:9     cancel test   x XOR t < x  ⟺  bit k of x        (one input literal)10     nonzero test  x ≠ 0        ⟺  OR of the B bits of x11     decrement     bit k' of x-1 = bit k' of x XOR (all lower bits of x are 0)12   The selection formulas choose the first cancelling heap if one exists, else the13   first nonzero heap; the value formulas output x XOR t or x - 1 accordingly.14   We prove that `readoutOf` of these formulas equals `attainF` on every board, and15   bound depth and size.  With the phase-3 exactness theorem and the conditional16   bridge this gives: UNDER THE PARITY-CORRELATION PREMISE, the class of readouts17   with these resource bounds has optimal conditional success in18   [2/(q-1), 2/(q-1) + (q-1) ε]. -/1920namespace NimAudit21namespace AttainCircuit2223open Prob AC0 AC0.Circ Game Bridge Rollout Attain CorrBridge2425attribute [local simp] Rat.add_zero Rat.zero_add2627/-! ## Arithmetic facts -/2829/-- x XOR t < x iff x has t's top bit (t ≠ 0). -/30theorem cancel_iff_bit {x t : Nat} (ht : t ≠ 0) : x ^^^ t < x ↔ x.testBit t.log2 = true := by31  have htk : t.testBit t.log2 = true := by32    cases hb : t.testBit t.log2 with33    | true => rfl34    | false =>35      exfalso36      have hlt : t < 2 ^ t.log2 := by37        apply Nat.lt_pow_two_of_testBit38        intro i hi39        by_cases hik : i = t.log240        · subst hik; exact hb41        · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self42            (Nat.pow_le_pow_right (by decide) (by omega)))43      exact absurd (Nat.log2_self_le ht) (Nat.not_le.mpr hlt)44  have habove : ∀ i, t.log2 < i → t.testBit i = false := fun i hi =>45    Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self46      (Nat.pow_le_pow_right (by decide) (by omega)))47  constructor48  · intro hlt49    cases hx : x.testBit t.log2 with50    | true => rfl51    | false =>52      exfalso53      have : x < x ^^^ t := by54        apply lt_of_top_testBit (k := t.log2) hx55        · rw [Nat.testBit_xor, hx, htk]; rfl56        · intro i hi; rw [Nat.testBit_xor, habove i hi, Bool.xor_false]57      omega58  · intro hx59    apply lt_of_top_testBit (k := t.log2)60    · rw [Nat.testBit_xor, hx, htk]; rfl61    · exact hx62    · intro i hi; rw [Nat.testBit_xor, habove i hi, Bool.xor_false]6364/-- Bits of x - 1 (x > 0). -/65theorem testBit_pred (x : Nat) (hx : 0 < x) (k : Nat) :66    (x - 1).testBit k = xor (x.testBit k) (decide (∀ j < k, x.testBit j = false)) := by67  induction x using Nat.strongRecOn generalizing k with68  | ind x ih =>69    rcases Nat.mod_two_eq_zero_or_one x with hev | hod70    · have hy : 0 < x / 2 := by omega71      cases k with72      | zero =>73        simp only [Nat.testBit_zero]74        have : (x - 1) % 2 = 1 := by omega75        simp [hev, this]76      | succ k =>77        rw [← Nat.testBit_div_two (x - 1) k, ← Nat.testBit_div_two x k,78          show (x - 1) / 2 = x / 2 - 1 by omega, ih (x / 2) (by omega) hy k]79        congr 180        apply Bool.eq_iff_iff.mpr81        simp only [decide_eq_true_iff]82        constructor83        · intro h j hj84          cases j with85          | zero => simp [Nat.testBit_zero, hev]86          | succ j => rw [← Nat.testBit_div_two]; exact h j (by omega)87        · intro h j hj88          rw [Nat.testBit_div_two]; exact h (j + 1) (by omega)89    · cases k with90      | zero =>91        simp only [Nat.testBit_zero]92        have : (x - 1) % 2 = 0 := by omega93        simp [hod, this]94      | succ k =>95        rw [← Nat.testBit_div_two (x - 1) k, ← Nat.testBit_div_two x k,96          show (x - 1) / 2 = x / 2 by omega]97        have : ¬ ∀ j < k + 1, x.testBit j = false := by98          intro h; have := h 0 (by omega); simp [Nat.testBit_zero, hod] at this99        simp [this]100101theorem pos_iff_bit {x B : Nat} (hx : x < 2 ^ B) :102    0 < x ↔ ∃ p < B, x.testBit (B - 1 - p) = true := by103  constructor104  · intro h105    obtain ⟨i, hi⟩ := Nat.exists_testBit_of_ne_zero (Nat.pos_iff_ne_zero.mp h)106    have hiB : i < B := by107      rcases Nat.lt_or_ge i B with h' | h'108      · exact h'109      · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by decide) h'))] at hi110        cases hi111    exact ⟨B - 1 - i, by omega, by rwa [show B - 1 - (B - 1 - i) = i by omega]⟩112  · rintro ⟨p, _, hp⟩113    rcases Nat.eq_zero_or_pos x with h | h114    · subst h; simp at hp115    · exact h116117/-! ## Readout indices via firstTrue -/118119theorem cancelIdx_firstTrue (t : Nat) : ∀ P : List Nat,120    cancelIdx t P = (firstTrue (P.map (fun x => decide (x ^^^ t < x)))).map121      (fun i => (i, P.getD i 0 ^^^ t))122  | [] => rfl123  | x :: P => by124    simp only [cancelIdx, List.map_cons]125    by_cases hx : x ^^^ t < x126    · simp [hx, firstTrue]127    · simp only [hx, if_false, decide_false, firstTrue]128      rw [cancelIdx_firstTrue t P]129      cases firstTrue (P.map (fun x => decide (x ^^^ t < x))) <;> simp130131theorem decIdx_firstTrue : ∀ P : List Nat,132    decIdx P = (firstTrue (P.map (fun x => decide (0 < x)))).map (fun i => (i, P.getD i 0 - 1))133  | [] => rfl134  | x :: P => by135    simp only [decIdx, List.map_cons]136    by_cases hx : 0 < x137    · simp [hx, firstTrue]138    · simp only [hx, if_false, decide_false, firstTrue]139      rw [decIdx_firstTrue P]140      cases firstTrue (P.map (fun x => decide (0 < x))) <;> simp141142theorem range_map_getD {α : Type} (f : Nat → α) : ∀ P : List Nat,143    (List.range P.length).map (fun i => f (P.getD i 0)) = P.map f144  | [] => rfl145  | x :: P => by146    rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.map_map]147    simp only [List.getD_cons_zero, List.map_cons]148    congr 1149    rw [← range_map_getD f P]150    apply List.map_congr_left151    intro i _152    simp153154theorem firstTrue_or (N : Nat) (c n : Nat → Bool) :155    firstTrue ((List.range N).map (fun i => c i || (!((List.range N).any c) && n i))) =156      if (List.range N).any c then firstTrue ((List.range N).map c)157      else firstTrue ((List.range N).map n) := by158  by_cases h : (List.range N).any c = true159  · simp only [h, Bool.not_true, Bool.false_and, Bool.or_false, if_true]160  · simp only [h, Bool.not_false, Bool.true_and, Bool.false_eq_true, if_false]161    congr 1162    apply List.map_congr_left163    intro i hi164    have : c i = false := by165      cases hc : c i166      · rfl167      · exact absurd (List.any_eq_true.mpr ⟨i, hi, hc⟩) h168    simp [this]169170theorem firstTrue_lt {l : List Bool} {i : Nat} (h : firstTrue l = some i) : i < l.length :=171  ((firstTrue_some_iff l i).1 h).1172173/-! ## The circuits -/174175def cancelC (B k i : Nat) : Circ := input (B * i + (B - 1 - k))176def nzC (B i : Nat) : Circ := or ((List.range B).map (fun p => input (B * i + p)))177def anyC (B N k : Nat) : Circ := or ((List.range N).map (cancelC B k))178def selA (B N k i : Nat) : Circ := or [cancelC B k i, and [not (anyC B N k), nzC B i]]179180/-- "i is the first index (below i) with cs true". -/181def firstC (cs : Nat → Circ) (i : Nat) : Circ :=182  and (cs i :: (List.range i).map (fun i' => not (cs i')))183184def xbitC (B t i p : Nat) : Circ :=185  if t.testBit (B - 1 - p) then not (input (B * i + p)) else input (B * i + p)186187/-- All bits of heap i strictly below big-endian position p are zero. -/188def lowZeroC (B i p : Nat) : Circ :=189  and ((List.range (B - 1 - p)).map (fun r => not (input (B * i + (p + 1 + r)))))190191def decbitC (B i p : Nat) : Circ := xor2 (input (B * i + p)) (lowZeroC B i p)192193def valA (B N t k p : Nat) : Circ :=194  or [and [anyC B N k, or ((List.range N).map (fun i => and [firstC (cancelC B k) i, xbitC B t i p]))],195      and [not (anyC B N k), or ((List.range N).map (fun i => and [firstC (nzC B) i, decbitC B i p]))]]196197def validA (B N : Nat) : Circ := or ((List.range N).map (nzC B))198199/-- The attainability readout for a single guess t (as in `attainF`). -/200def attainT (t : Nat) (P : List Nat) : Option (Nat × Nat) :=201  match cancelIdx t P with202  | some m => some m203  | none => decIdx P204205theorem attainF_eq (a0 a1 : Nat) (P : List Nat) (b : Bool) :206    attainF a0 a1 P b = attainT (if b then a1 else a0) P := rfl207208/-- The readout circuits for guess t. -/209def attRC (B N t : Nat) : RCirc :=210  ⟨validA B N, (List.range N).map (selA B N t.log2), (List.range B).map (valA B N t t.log2)⟩211212/-- The two-guess circuit readout. -/213def attR (B N a0 a1 : Nat) : Bool → RCirc := fun b => attRC B N (if b then a1 else a0)214215/-! ## Semantics -/216217section Sem218219variable {B N : Nat} {P : List Nat}220221theorem firstC_eval (z : Nat → Bool) (cs : Nat → Circ) {i : Nat} (hi : i < N) :222    eval z (firstC cs i) = decide (firstTrue ((List.range N).map (fun i => eval z (cs i))) = some i) := by223  unfold firstC224  rw [Bool.eq_iff_iff, decide_eq_true_iff, firstTrue_some_iff]225  simp only [eval_and, List.all_cons, List.all_map, Bool.and_eq_true, List.all_eq_true,226    List.mem_range, Function.comp, eval_not, Bool.not_eq_true', List.length_map, List.length_range]227  simp only [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hi]228  constructor229  · rintro ⟨h1, h2⟩230    refine ⟨hi, by simpa using h1, ?_⟩231    intro i' hi'232    rw [List.getElem?_range (by omega)]; simpa using h2 i' hi'233  · rintro ⟨_, h1, h2⟩234    refine ⟨by simpa using h1, ?_⟩235    intro i' hi'236    have := h2 i' hi'237    rw [List.getElem?_range (by omega)] at this; simpa using this238239theorem cancel_eval (hP : P.length = N) {t : Nat} (ht : t < 2 ^ B) (ht0 : t ≠ 0) {i : Nat} (hi : i < N) :240    eval (boardBits B P) (cancelC B t.log2 i) = decide (P.getD i 0 ^^^ t < P.getD i 0) := by241  have hk : t.log2 < B := by242    rcases Nat.lt_or_ge t.log2 B with h | h243    · exact h244    · exfalso245      exact absurd (Nat.lt_of_lt_of_le ht (Nat.pow_le_pow_right (by decide) h))246        (Nat.not_lt.mpr (Nat.log2_self_le ht0))247  unfold cancelC248  rw [eval_input, boardBits_heap hP hi (by omega), show B - 1 - (B - 1 - t.log2) = t.log2 by omega]249  apply Bool.eq_iff_iff.mpr250  rw [decide_eq_true_iff, cancel_iff_bit ht0]251252theorem nz_eval (hP : P.length = N) (hw : Width B P) {i : Nat} (hi : i < N) :253    eval (boardBits B P) (nzC B i) = decide (0 < P.getD i 0) := by254  have hx : P.getD i 0 < 2 ^ B := by255    apply hw; simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp256  unfold nzC257  apply Bool.eq_iff_iff.mpr258  rw [decide_eq_true_iff, pos_iff_bit hx]259  simp only [eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp, eval_input]260  constructor261  · rintro ⟨p, hp, h⟩; rw [boardBits_heap hP hi hp] at h; exact ⟨p, hp, h⟩262  · rintro ⟨p, hp, h⟩; exact ⟨p, hp, by rw [boardBits_heap hP hi hp]; exact h⟩263264theorem toNatBE_of_bits {h : Nat} (hh : h < 2 ^ B) (f : Nat → Bool)265    (hf : ∀ p < B, f p = h.testBit (B - 1 - p)) : toNatBE ((List.range B).map f) = h := by266  apply Nat.eq_of_testBit_eq267  intro k268  have hlen : ((List.range B).map f).length = B := by simp269  rcases Nat.lt_or_ge k B with hk | hk270  · have := testBit_toNatBE ((List.range B).map f) (B - 1 - k) (by rw [hlen]; omega)271    rw [hlen, show B - 1 - (B - 1 - k) = k by omega] at this272    rw [this]273    simp only [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range (show B - 1 - k < B by omega),274      Option.map_some, Option.getD_some]275    rw [hf _ (by omega), show B - 1 - (B - 1 - k) = k by omega]276  · have h1 := toNatBE_lt ((List.range B).map f)277    rw [hlen] at h1278    rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le h1 (Nat.pow_le_pow_right (by decide) hk)),279      Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hh (Nat.pow_le_pow_right (by decide) hk))]280281/-- CIRCUIT REALISATION IS EXACT: the circuit readout equals the attainability282    readout `attainF` on every board of N heaps below 2^B (nonzero guesses). -/283theorem attR_correct {a0 a1 : Nat} (h0 : a0 ≠ 0) (h1 : a1 ≠ 0) (hl0 : a0 < 2 ^ B) (hl1 : a1 < 2 ^ B)284    (hP : P.length = N) (hw : Width B P) (b : Bool) :285    readoutOf B (attR B N a0 a1) P b = attainF a0 a1 P b := by286  generalize ht : (if b then a1 else a0) = t287  have ht0 : t ≠ 0 := by rw [← ht]; cases b <;> simp [h0, h1]288  have htl : t < 2 ^ B := by rw [← ht]; cases b <;> simp [hl0, hl1]289  have hRb : attR B N a0 a1 b = attRC B N t := by unfold attR; rw [ht]290  rw [attainF_eq, ht]291  unfold readoutOf attainT292  rw [hRb]293  generalize hz : boardBits B P = z294  -- evaluated tests as lists over heaps295  have hcan : (List.range N).map (fun i => eval z (cancelC B t.log2 i)) =296      P.map (fun x => decide (x ^^^ t < x)) := by297    have hrm := range_map_getD (fun x => decide (x ^^^ t < x)) P298    rw [← hrm, hP]299    apply List.map_congr_left; intro i hi300    rw [← hz, cancel_eval hP htl ht0 (List.mem_range.mp hi)]301  have hnz : (List.range N).map (fun i => eval z (nzC B i)) = P.map (fun x => decide (0 < x)) := by302    have hrm := range_map_getD (fun x => decide (0 < x)) P303    rw [← hrm, hP]304    apply List.map_congr_left; intro i hi305    rw [← hz, nz_eval hP hw (List.mem_range.mp hi)]306  have hany : eval z (anyC B N t.log2) = (List.range N).any (fun i => eval z (cancelC B t.log2 i)) := by307    unfold anyC; rw [eval_or, List.any_map]; rfl308  have hsel : ((attRC B N t).sel.map (eval z)) =309      (List.range N).map (fun i => eval z (cancelC B t.log2 i) ||310        (!((List.range N).any (fun i => eval z (cancelC B t.log2 i))) && eval z (nzC B i))) := by311    unfold attRC312    rw [List.map_map]313    apply List.map_congr_left; intro i _314    simp only [Function.comp, selA, eval_or, eval_and, eval_not, List.any_cons, List.any_nil,315      List.all_cons, List.all_nil, Bool.or_false, Bool.and_true, hany]316  have hvalid : eval z (attRC B N t).valid = (List.range N).any (fun i => eval z (nzC B i)) := by317    unfold attRC validA; rw [eval_or, List.any_map]; rfl318  rw [hsel, firstTrue_or, hvalid]319  rw [cancelIdx_firstTrue, decIdx_firstTrue]320  have hanyP : (List.range N).any (fun i => eval z (cancelC B t.log2 i)) =321      (P.map (fun x => decide (x ^^^ t < x))).any id := by322    rw [← hcan]; simp [List.any_map, Function.comp]323  by_cases hA : (List.range N).any (fun i => eval z (cancelC B t.log2 i)) = true324  · -- a cancelling heap exists325    simp only [hA, if_true]326    rw [hcan]327    obtain ⟨i, hi⟩ : ∃ i, firstTrue (P.map (fun x => decide (x ^^^ t < x))) = some i := by328      rw [hanyP] at hA329      cases hf : firstTrue (P.map (fun x => decide (x ^^^ t < x))) with330      | some i => exact ⟨i, rfl⟩331      | none =>332        exfalso333        obtain ⟨y, hy, hyb⟩ := List.any_eq_true.mp hA334        have key : ∀ l : List Bool, firstTrue l = none → ∀ y ∈ l, y = false := by335          intro l; induction l with336          | nil => simp337          | cons c l ihl =>338            cases c339            · intro h y hy340              simp only [firstTrue] at h341              rcases List.mem_cons.mp hy with rfl | hy342              · rfl343              · exact ihl (by cases hfl : firstTrue l <;> simp_all) y hy344            · intro h; simp [firstTrue] at h345        have := key _ hf y hy; simp at hyb; rw [this] at hyb; cases hyb346    have hiN : i < N := by have := firstTrue_lt hi; rw [List.length_map, hP] at this; exact this347    obtain ⟨_, hbit, _⟩ := (firstTrue_some_iff _ i).1 hi348    have hPi : P.getD i 0 ^^^ t < P.getD i 0 := by349      simp only [List.getD_eq_getElem?_getD, List.getElem?_map] at hbit350      rw [List.getElem?_eq_getElem (by omega)] at hbit351      simp only [Option.map_some, Option.getD_some, decide_eq_true_eq] at hbit352      simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simpa using hbit353    have hvalidT : (List.range N).any (fun i => eval z (nzC B i)) = true := by354      apply List.any_eq_true.mpr355      refine ⟨i, List.mem_range.mpr hiN, ?_⟩356      rw [← hz, nz_eval hP hw hiN, decide_eq_true_iff]; omega357    simp only [hvalidT, if_true, hi, Option.map_some]358    congr 2359    -- the value bits give P_i XOR t360    unfold attRC361    simp only [List.map_map]362    apply toNatBE_of_bits (Nat.xor_lt_two_pow (hw _ (by363      simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp)) htl)364    intro p hp365    simp only [Function.comp, valA, eval_or, eval_and, eval_not, List.any_cons, List.any_nil,366      List.all_cons, List.all_nil, Bool.and_true, Bool.or_false, hany, hA, Bool.not_true,367      Bool.false_and, Bool.true_and]368    apply Bool.eq_iff_iff.mpr369    simp only [List.any_map, List.any_eq_true, List.mem_range, Function.comp, eval_and,370      List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true]371    rw [Nat.testBit_xor]372    have hfc : ∀ i', i' < N → (eval z (firstC (cancelC B t.log2) i') = true ↔ i' = i) := by373      intro i' hi'374      rw [← hz, firstC_eval _ _ hi', hz, hcan, decide_eq_true_iff, hi]375      constructor376      · intro h; cases h; rfl377      · intro h; rw [h]378    have hxb : ∀ i', i' < N → eval z (xbitC B t i' p) =379        xor ((P.getD i' 0).testBit (B - 1 - p)) (t.testBit (B - 1 - p)) := by380      intro i' hi'381      unfold xbitC382      rw [← hz]383      split384      · next htb =>385        rw [eval_not, eval_input, boardBits_heap hP hi' hp, htb]386        cases (P.getD i' 0).testBit (B - 1 - p) <;> rfl387      · next htb =>388        rw [eval_input, boardBits_heap hP hi' hp]389        have : t.testBit (B - 1 - p) = false := by simpa using htb390        rw [this, Bool.xor_false]391    constructor392    · rintro ⟨i', hi', hf', hx⟩393      rw [(hfc i' hi').1 hf'] at hx394      rw [hxb i hiN] at hx; exact hx395    · intro hx396      exact ⟨i, hiN, (hfc i hiN).2 rfl, by rw [hxb i hiN]; exact hx⟩397  · -- no cancelling heap398    simp only [hA, Bool.false_eq_true, if_false]399    rw [hnz]400    have hcnone : firstTrue (P.map (fun x => decide (x ^^^ t < x))) = none := by401      cases hf : firstTrue (P.map (fun x => decide (x ^^^ t < x))) with402      | none => rfl403      | some i =>404        exfalso; apply hA405        rw [hanyP]406        obtain ⟨hl, hb, _⟩ := (firstTrue_some_iff _ i).1 hf407        apply List.any_eq_true.mpr408        refine ⟨true, ?_, rfl⟩409        simp only [List.getD_eq_getElem?_getD] at hb410        rw [List.getElem?_eq_getElem hl] at hb411        simp at hb412        exact List.mem_iff_getElem.mpr ⟨i, hl, by simpa using hb⟩413    simp only [hcnone, Option.map_none]414    by_cases hV : (List.range N).any (fun i => eval z (nzC B i)) = true415    · simp only [hV, if_true]416      obtain ⟨i, hi⟩ : ∃ i, firstTrue (P.map (fun x => decide (0 < x))) = some i := by417        rw [← hnz]418        cases hf : firstTrue ((List.range N).map (fun i => eval z (nzC B i))) with419        | some i => exact ⟨i, rfl⟩420        | none =>421          exfalso422          obtain ⟨j, hj, hjb⟩ := List.any_eq_true.mp hV423          have key : ∀ l : List Bool, firstTrue l = none → ∀ y ∈ l, y = false := by424            intro l; induction l with425            | nil => simp426            | cons c l ihl =>427              cases c428              · intro h y hy429                simp only [firstTrue] at h430                rcases List.mem_cons.mp hy with rfl | hy431                · rfl432                · exact ihl (by cases hfl : firstTrue l <;> simp_all) y hy433              · intro h; simp [firstTrue] at h434          have := key _ hf (eval z (nzC B j)) (List.mem_map.mpr ⟨j, hj, rfl⟩)435          rw [this] at hjb; cases hjb436      have hiN : i < N := by have := firstTrue_lt hi; rw [List.length_map, hP] at this; exact this437      obtain ⟨_, hbit, _⟩ := (firstTrue_some_iff _ i).1 hi438      have hpos : 0 < P.getD i 0 := by439        simp only [List.getD_eq_getElem?_getD, List.getElem?_map] at hbit440        rw [List.getElem?_eq_getElem (by omega)] at hbit441        simp only [Option.map_some, Option.getD_some, decide_eq_true_eq] at hbit442        simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simpa using hbit443      simp only [hi, Option.map_some]444      congr 2445      unfold attRC446      simp only [List.map_map]447      have hxlt : P.getD i 0 < 2 ^ B := hw _ (by448        simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp)449      apply toNatBE_of_bits (Nat.lt_of_le_of_lt (Nat.sub_le _ _) hxlt)450      intro p hp451      simp only [Function.comp, valA, eval_or, eval_and, eval_not, List.any_cons, List.any_nil,452        List.all_cons, List.all_nil, Bool.and_true, Bool.or_false, hany, hA, Bool.not_false,453        Bool.false_and, Bool.true_and, Bool.false_or]454      apply Bool.eq_iff_iff.mpr455      simp only [List.any_map, List.any_eq_true, List.mem_range, Function.comp, eval_and,456        List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true]457      rw [testBit_pred _ hpos]458      have hfn : ∀ i', i' < N → (eval z (firstC (nzC B) i') = true ↔ i' = i) := by459        intro i' hi'460        rw [← hz, firstC_eval _ _ hi', hz, hnz, decide_eq_true_iff, hi]461        constructor462        · intro h; cases h; rfl463        · intro h; rw [h]464      have hdb : ∀ i', i' < N → eval z (decbitC B i' p) =465          xor ((P.getD i' 0).testBit (B - 1 - p))466            (decide (∀ j < B - 1 - p, (P.getD i' 0).testBit j = false)) := by467        intro i' hi'468        unfold decbitC469        rw [eval_xor2, ← hz, eval_input, boardBits_heap hP hi' hp]470        congr 1471        unfold lowZeroC472        apply Bool.eq_iff_iff.mpr473        simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp,474          eval_not, eval_input, Bool.not_eq_true', decide_eq_true_iff]475        constructor476        · intro h j hj477          have := h (B - 1 - p - 1 - j) (by omega)478          rw [boardBits_heap hP hi' (by omega)] at this479          rwa [show B - 1 - (p + 1 + (B - 1 - p - 1 - j)) = j by omega] at this480        · intro h r hr481          rw [boardBits_heap hP hi' (by omega)]482          exact h _ (by omega)483      constructor484      · rintro ⟨i', hi', hf', hx⟩485        rw [(hfn i' hi').1 hf'] at hx486        rw [hdb i hiN] at hx; exact hx487      · intro hx488        exact ⟨i, hiN, (hfn i hiN).2 rfl, by rw [hdb i hiN]; exact hx⟩489    · simp only [hV, Bool.false_eq_true, if_false]490      have hnone : firstTrue (P.map (fun x => decide (0 < x))) = none := by491        cases hf : firstTrue (P.map (fun x => decide (0 < x))) with492        | none => rfl493        | some i =>494          exfalso; apply hV495          obtain ⟨hl, hb, _⟩ := (firstTrue_some_iff _ i).1 hf496          have hiN : i < N := by rw [List.length_map, hP] at hl; exact hl497          apply List.any_eq_true.mpr498          refine ⟨i, List.mem_range.mpr hiN, ?_⟩499          rw [← hz, nz_eval hP hw hiN, decide_eq_true_iff]500          simp only [List.getD_eq_getElem?_getD, List.getElem?_map] at hb501          rw [List.getElem?_eq_getElem (by omega)] at hb502          simp only [Option.map_some, Option.getD_some, decide_eq_true_eq] at hb503          simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simpa using hb504      simp [hnone]505506end Sem507508/-- The success counts of the circuit readout and of `attainF` coincide. -/509theorem succCount_attR {B N w a0 a1 : Nat} (h0 : a0 ≠ 0) (h1 : a1 ≠ 0) (hl0 : a0 < 2 ^ B)510    (hl1 : a1 < 2 ^ B) :511    succCount B N (readoutOf B (attR B N a0 a1)) w = succCount B N (attainF a0 a1) w := by512  unfold succCount513  apply rsum_congr514  intro P hP515  obtain ⟨hlen, hw⟩ := mem_boards hP516  have : ∀ b, readoutOf B (attR B N a0 a1) P b = attainF a0 a1 P b :=517    fun b => attR_correct h0 h1 hl0 hl1 hlen hw b518  unfold successB519  rw [this]520521/-! ## Resource bounds of the attainability circuits -/522523/-- Size parameter for the attainability circuits. -/524def Ua (N B : Nat) : Nat := (N + 2) * (B + 2)525526theorem Ua_ge (N B : Nat) : 1 ≤ Ua N B ∧ N + 2 ≤ Ua N B ∧ B + 2 ≤ Ua N B := by527  unfold Ua528  refine ⟨Nat.mul_pos (by omega) (by omega), ?_, ?_⟩529  · have := Nat.le_mul_of_pos_right (N + 2) (show 0 < B + 2 by omega); omega530  · have := Nat.le_mul_of_pos_left (B + 2) (show 0 < N + 2 by omega); omega531532section ABounds533534variable {B N t : Nat}535536theorem mem_pair {x a b : Circ} (h : x ∈ [a, b]) : x = a ∨ x = b := by537  simpa using h538539theorem attRC_depth_size (t p i : Nat) :540    depth (selA B N t.log2 i) ≤ 9 ∧ depth (valA B N t t.log2 p) ≤ 9 ∧ depth (validA B N) ≤ 9 ∧541    size (selA B N t.log2 i) ≤ 10 * Ua N B ^ 8 ∧ size (valA B N t t.log2 p) ≤ 10 * Ua N B ^ 8 ∧542    size (validA B N) ≤ 10 * Ua N B ^ 8 := by543  obtain ⟨hU, hUN, hUB⟩ := Ua_ge N B544  generalize Ua N B = U at *545  have sin : ∀ j, size (input j) ≤ 1 * U ^ 1 := fun j => by simp; omega546  -- basic blocks547  have hcan : ∀ i, size (cancelC B t.log2 i) ≤ 1 * U ^ 1 ∧ depth (cancelC B t.log2 i) ≤ 0 :=548    fun i => ⟨sin _, by simp [cancelC]⟩549  have hnz : ∀ i, size (nzC B i) ≤ 2 * U ^ 2 ∧ depth (nzC B i) ≤ 1 := by550    intro i; unfold nzC551    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩552    · intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; exact sin _553    · intro c hc; obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc; simp554  have hany : size (anyC B N t.log2) ≤ 2 * U ^ 2 ∧ depth (anyC B N t.log2) ≤ 1 := by555    unfold anyC556    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩557    · intro c hc; obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (hcan i).1558    · intro c hc; obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc; exact (hcan i).2559  have hnany : size (not (anyC B N t.log2)) ≤ 3 * U ^ 2 ∧ depth (not (anyC B N t.log2)) ≤ 2 :=560    ⟨size_not_le hU hany.1, by simp; have := hany.2; omega⟩561  -- selA562  have hsel : size (selA B N t.log2 i) ≤ 5 * U ^ 4 ∧ depth (selA B N t.log2 i) ≤ 4 := by563    unfold selA564    have hand : size (and [not (anyC B N t.log2), nzC B i]) ≤ 4 * U ^ 3 ∧565        depth (and [not (anyC B N t.log2), nzC B i]) ≤ 3 := by566      refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩567      · intro c hc; rcases mem_pair hc with rfl | rfl568        · exact hnany.1569        · exact size_lift hU (hnz i).1 (by omega) (Nat.le_refl _)570      · intro c hc; rcases mem_pair hc with rfl | rfl571        · exact hnany.2572        · have := (hnz i).2; omega573    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩574    · intro c hc; rcases mem_pair hc with rfl | rfl575      · exact size_lift hU (hcan i).1 (by omega) (by omega)576      · exact hand.1577    · intro c hc; rcases mem_pair hc with rfl | rfl578      · have := (hcan i).2; omega579      · exact hand.2580  -- firstC blocks581  have hfc : ∀ i', i' ≤ N → size (firstC (cancelC B t.log2) i') ≤ 3 * U ^ 2 ∧582      depth (firstC (cancelC B t.log2) i') ≤ 2 := by583    intro i' hi'; unfold firstC584    refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩585    · intro c hc586      simp only [List.mem_cons, List.mem_map] at hc587      rcases hc with rfl | ⟨i'', _, rfl⟩588      · exact size_lift hU (hcan i').1 (by omega) (Nat.le_refl _)589      · exact size_not_le hU (hcan i'').1590    · intro c hc591      simp only [List.mem_cons, List.mem_map] at hc592      rcases hc with rfl | ⟨i'', _, rfl⟩593      · have := (hcan i').2; omega594      · simp [cancelC]595  have hfn : ∀ i', i' ≤ N → size (firstC (nzC B) i') ≤ 4 * U ^ 3 ∧ depth (firstC (nzC B) i') ≤ 3 := by596    intro i' hi'; unfold firstC597    refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩598    · intro c hc599      simp only [List.mem_cons, List.mem_map] at hc600      rcases hc with rfl | ⟨i'', _, rfl⟩601      · exact size_lift hU (hnz i').1 (by omega) (Nat.le_refl _)602      · exact size_not_le hU (hnz i'').1603    · intro c hc604      simp only [List.mem_cons, List.mem_map] at hc605      rcases hc with rfl | ⟨i'', _, rfl⟩606      · have := (hnz i').2; omega607      · simp; have := (hnz i'').2; omega608  have hxb : ∀ i', size (xbitC B t i' p) ≤ 2 * U ^ 1 ∧ depth (xbitC B t i' p) ≤ 1 := by609    intro i'; unfold xbitC; split610    · exact ⟨size_not_le hU (sin _), by simp⟩611    · exact ⟨size_lift hU (sin _) (by omega) (Nat.le_refl _), by simp⟩612  have hlz : ∀ i', size (lowZeroC B i' p) ≤ 3 * U ^ 2 ∧ depth (lowZeroC B i' p) ≤ 2 := by613    intro i'; unfold lowZeroC614    refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩615    · intro c hc; obtain ⟨r, _, rfl⟩ := List.mem_map.mp hc; exact size_not_le hU (sin _)616    · intro c hc; obtain ⟨r, _, rfl⟩ := List.mem_map.mp hc; simp617  have hdb : ∀ i', size (decbitC B i' p) ≤ 6 * U ^ 4 ∧ depth (decbitC B i' p) ≤ 5 := by618    intro i'; unfold decbitC xor2619    have a1 : size (and [input (B * i' + p), not (lowZeroC B i' p)]) ≤ 5 * U ^ 3 ∧620        depth (and [input (B * i' + p), not (lowZeroC B i' p)]) ≤ 4 := by621      refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩622      · intro c hc; rcases mem_pair hc with rfl | rfl623        · exact size_lift hU (sin _) (by omega) (by omega)624        · exact size_not_le hU (hlz i').1625      · intro c hc; rcases mem_pair hc with rfl | rfl626        · simp627        · simp; have := (hlz i').2; omega628    have a2 : size (and [not (input (B * i' + p)), lowZeroC B i' p]) ≤ 4 * U ^ 3 ∧629        depth (and [not (input (B * i' + p)), lowZeroC B i' p]) ≤ 3 := by630      refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩631      · intro c hc; rcases mem_pair hc with rfl | rfl632        · exact size_lift hU (size_not_le hU (sin _)) (by omega) (by omega)633        · exact (hlz i').1634      · intro c hc; rcases mem_pair hc with rfl | rfl635        · simp636        · have := (hlz i').2; omega637    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩638    · intro c hc; rcases mem_pair hc with rfl | rfl639      · exact a1.1640      · exact size_lift hU a2.1 (by omega) (Nat.le_refl _)641    · intro c hc; rcases mem_pair hc with rfl | rfl642      · exact a1.2643      · have := a2.2; omega644  -- valA645  have hval : size (valA B N t t.log2 p) ≤ 10 * U ^ 8 ∧ depth (valA B N t t.log2 p) ≤ 9 := by646    unfold valA647    have o1 : size (or ((List.range N).map (fun i => and [firstC (cancelC B t.log2) i, xbitC B t i p])))648        ≤ 5 * U ^ 4 ∧649        depth (or ((List.range N).map (fun i => and [firstC (cancelC B t.log2) i, xbitC B t i p]))) ≤ 4 := by650      refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩651      · intro c hc; obtain ⟨i', hi', rfl⟩ := List.mem_map.mp hc652        have hi'' := List.mem_range.mp hi'653        apply size_and_le hU (by simp; omega)654        intro c hc; rcases mem_pair hc with rfl | rfl655        · exact (hfc i' (by omega)).1656        · exact size_lift hU (hxb i').1 (by omega) (by omega)657      · intro c hc; obtain ⟨i', hi', rfl⟩ := List.mem_map.mp hc658        have hi'' := List.mem_range.mp hi'659        apply depth_and_le660        intro c hc; rcases mem_pair hc with rfl | rfl661        · exact (hfc i' (by omega)).2662        · have := (hxb i').2; omega663    have o2 : size (or ((List.range N).map (fun i => and [firstC (nzC B) i, decbitC B i p]))) ≤ 8 * U ^ 6 ∧664        depth (or ((List.range N).map (fun i => and [firstC (nzC B) i, decbitC B i p]))) ≤ 7 := by665      refine ⟨size_lift hU (size_or_le hU (by simp; omega) (a := 7) (k := 5) ?_) (by omega) (Nat.le_refl _),666        depth_or_le ?_⟩667      · intro c hc; obtain ⟨i', hi', rfl⟩ := List.mem_map.mp hc668        have hi'' := List.mem_range.mp hi'669        apply size_and_le hU (by simp; omega)670        intro c hc; rcases mem_pair hc with rfl | rfl671        · exact size_lift hU (hfn i' (by omega)).1 (by omega) (by omega)672        · exact (hdb i').1673      · intro c hc; obtain ⟨i', hi', rfl⟩ := List.mem_map.mp hc674        have hi'' := List.mem_range.mp hi'675        apply depth_and_le676        intro c hc; rcases mem_pair hc with rfl | rfl677        · have := (hfn i' (by omega)).2; omega678        · have := (hdb i').2; omega679    have b1 : size (and [anyC B N t.log2, or ((List.range N).map680        (fun i => and [firstC (cancelC B t.log2) i, xbitC B t i p]))]) ≤ 9 * U ^ 7 ∧681        depth (and [anyC B N t.log2, or ((List.range N).map682        (fun i => and [firstC (cancelC B t.log2) i, xbitC B t i p]))]) ≤ 8 := by683      refine ⟨size_lift hU (size_and_le hU (by simp; omega) (a := 5) (k := 4) ?_) (by omega) (by omega),684        depth_and_le ?_⟩685      · intro c hc; rcases mem_pair hc with rfl | rfl686        · exact size_lift hU hany.1 (by omega) (by omega)687        · exact o1.1688      · intro c hc; rcases mem_pair hc with rfl | rfl689        · have := hany.2; omega690        · have := o1.2; omega691    have b2 : size (and [not (anyC B N t.log2), or ((List.range N).map692        (fun i => and [firstC (nzC B) i, decbitC B i p]))]) ≤ 9 * U ^ 7 ∧693        depth (and [not (anyC B N t.log2), or ((List.range N).map694        (fun i => and [firstC (nzC B) i, decbitC B i p]))]) ≤ 8 := by695      refine ⟨size_and_le hU (by simp; omega) ?_, depth_and_le ?_⟩696      · intro c hc; rcases mem_pair hc with rfl | rfl697        · exact size_lift hU hnany.1 (by omega) (by omega)698        · exact o2.1699      · intro c hc; rcases mem_pair hc with rfl | rfl700        · have := hnany.2; omega701        · exact o2.2702    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩703    · intro c hc; rcases mem_pair hc with rfl | rfl704      · exact b1.1705      · exact b2.1706    · intro c hc; rcases mem_pair hc with rfl | rfl707      · exact b1.2708      · exact b2.2709  have hvalid : size (validA B N) ≤ 3 * U ^ 3 ∧ depth (validA B N) ≤ 2 := by710    unfold validA711    refine ⟨size_or_le hU (by simp; omega) ?_, depth_or_le ?_⟩712    · intro c hc; obtain ⟨i', _, rfl⟩ := List.mem_map.mp hc; exact (hnz i').1713    · intro c hc; obtain ⟨i', _, rfl⟩ := List.mem_map.mp hc; exact (hnz i').2714  refine ⟨by have := hsel.2; omega, hval.2, by have := hvalid.2; omega,715    size_lift hU hsel.1 (by omega) (by omega), hval.1, size_lift hU hvalid.1 (by omega) (by omega)⟩716717theorem and_max' {cs : List Circ} {m : Nat} (h : ∀ c ∈ cs, maxInput c ≤ m) : maxInput (and cs) ≤ m := by718  simp only [maxInput_and]; apply listMax_le; intro a ha719  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc720721theorem or_max' {cs : List Circ} {m : Nat} (h : ∀ c ∈ cs, maxInput c ≤ m) : maxInput (or cs) ≤ m := by722  simp only [maxInput_or]; apply listMax_le; intro a ha723  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc724725theorem in_max {i p : Nat} (hi : i < N) (hp : p < B) : maxInput (input (B * i + p)) ≤ B * N := by726  simp only [maxInput_input]727  have := Nat.mul_le_mul_left B (show i + 1 ≤ N by omega)728  rw [Nat.mul_succ] at this; omega729730theorem attRC_max {k : Nat} (hk : k < B) (t : Nat) :731    (∀ i, i < N → maxInput (selA B N k i) ≤ B * N) ∧732    (∀ p, p < B → maxInput (valA B N t k p) ≤ B * N) ∧ maxInput (validA B N) ≤ B * N := by733  have hcan : ∀ i, i < N → maxInput (cancelC B k i) ≤ B * N := fun i hi => in_max hi (by omega)734  have hnz : ∀ i, i < N → maxInput (nzC B i) ≤ B * N := by735    intro i hi; unfold nzC; apply or_max'; intro c hc736    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc; exact in_max hi (List.mem_range.mp hp)737  have hany : maxInput (anyC B N k) ≤ B * N := by738    unfold anyC; apply or_max'; intro c hc739    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact hcan i (List.mem_range.mp hi)740  refine ⟨?_, ?_, ?_⟩741  · intro i hi; unfold selA; apply or_max'; intro c hc; rcases mem_pair hc with rfl | rfl742    · exact hcan i hi743    · apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl744      · simp only [maxInput_not]; exact hany745      · exact hnz i hi746  · intro p hp; unfold valA; apply or_max'; intro c hc; rcases mem_pair hc with rfl | rfl747    · apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl748      · exact hany749      · apply or_max'; intro c hc750        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc751        have hi' := List.mem_range.mp hi752        apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl753        · unfold firstC; apply and_max'; intro c hc754          simp only [List.mem_cons, List.mem_map, List.mem_range] at hc755          rcases hc with rfl | ⟨i', hi'', rfl⟩756          · exact hcan i hi'757          · simp only [maxInput_not]; exact hcan i' (by omega)758        · unfold xbitC; split759          · simp only [maxInput_not]; exact in_max hi' hp760          · exact in_max hi' hp761    · apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl762      · simp only [maxInput_not]; exact hany763      · apply or_max'; intro c hc764        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc765        have hi' := List.mem_range.mp hi766        apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl767        · unfold firstC; apply and_max'; intro c hc768          simp only [List.mem_cons, List.mem_map, List.mem_range] at hc769          rcases hc with rfl | ⟨i', hi'', rfl⟩770          · exact hnz i hi'771          · simp only [maxInput_not]; exact hnz i' (by omega)772        · unfold decbitC xor2; apply or_max'; intro c hc; rcases mem_pair hc with rfl | rfl773          · apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl774            · exact in_max hi' hp775            · simp only [maxInput_not]; unfold lowZeroC; apply and_max'; intro c hc776              obtain ⟨r, hr, rfl⟩ := List.mem_map.mp hc777              simp only [maxInput_not]; exact in_max hi' (by have := List.mem_range.mp hr; omega)778          · apply and_max'; intro c hc; rcases mem_pair hc with rfl | rfl779            · simp only [maxInput_not]; exact in_max hi' hp780            · unfold lowZeroC; apply and_max'; intro c hc781              obtain ⟨r, hr, rfl⟩ := List.mem_map.mp hc782              simp only [maxInput_not]; exact in_max hi' (by have := List.mem_range.mp hr; omega)783  · unfold validA; apply or_max'; intro c hc784    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc; exact hnz i (List.mem_range.mp hi)785786theorem log2_lt {t : Nat} (ht0 : t ≠ 0) (ht : t < 2 ^ B) : t.log2 < B := by787  rcases Nat.lt_or_ge t.log2 B with h | h788  · exact h789  · exact absurd (Nat.lt_of_lt_of_le ht (Nat.pow_le_pow_right (by decide) h))790      (Nat.not_lt.mpr (Nat.log2_self_le ht0))791792/-- The attainability circuits satisfy the resource bounds: depth ≤ 9,793    size ≤ 10 ((N+2)(B+2))^8, reading only the N·B board bits. -/794theorem attRC_RBound {t : Nat} (ht0 : t ≠ 0) (ht : t < 2 ^ B) :795    RBound (attRC B N t) N B 9 (10 * Ua N B ^ 8) := by796  have hm := attRC_max (N := N) (log2_lt ht0 ht) t797  refine ⟨by simp [attRC], by simp [attRC], (attRC_depth_size (N := N) (B := B) t 0 0).2.2.1, ?_, ?_,798    (attRC_depth_size (N := N) (B := B) t 0 0).2.2.2.2.2, ?_, ?_, hm.2.2, ?_, ?_⟩799  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc800    obtain ⟨i, _, rfl⟩ := hc; exact (attRC_depth_size t 0 i).1801  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc802    obtain ⟨p, _, rfl⟩ := hc; exact (attRC_depth_size t p 0).2.1803  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc804    obtain ⟨i, _, rfl⟩ := hc; exact (attRC_depth_size t 0 i).2.2.2.1805  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc806    obtain ⟨p, _, rfl⟩ := hc; exact (attRC_depth_size t p 0).2.2.2.2.1807  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc808    obtain ⟨i, hi, rfl⟩ := hc; exact hm.1 i hi809  · intro c hc; simp only [attRC, List.mem_map, List.mem_range] at hc810    obtain ⟨p, hp, rfl⟩ := hc; exact hm.2.1 p hp811812end ABounds813814theorem RBound_mono {R : RCirc} {N B d s d' s' : Nat} (h : RBound R N B d s) (hd : d ≤ d')815    (hs : s ≤ s') : RBound R N B d' s' :=816  ⟨h.sel_len, h.val_len, Nat.le_trans h.depth_valid hd, fun c hc => Nat.le_trans (h.depth_sel c hc) hd,817    fun c hc => Nat.le_trans (h.depth_val c hc) hd, Nat.le_trans h.size_valid hs,818    fun c hc => Nat.le_trans (h.size_sel c hc) hs, fun c hc => Nat.le_trans (h.size_val c hc) hs,819    h.max_valid, h.max_sel, h.max_val⟩820821/-- The premise forces ε ≥ 0 (use the constant-false formula). -/822theorem premise_nonneg {d s m : Nat} {ε : Rat} (hs : 1 ≤ s) (h : ParityCorrPremise d s m ε) :823    0 ≤ ε := by824  obtain ⟨k1, _⟩ := h (const false) (by simp) (by simp; omega) (by simp)825  have : rsum (bitvecs m) (fun y => ind (eval (vfun y) (const false)) * sgn (par y)) = 0 := by826    rw [rsum_congr (g := fun _ => (0 : Rat)) (by intro y _; simp [ind])]827    exact rsum_zero _828  rw [this] at k1829  have h0 : (0 : Rat) / (2 : Rat) ^ m = 0 := by grind830  rw [h0] at k1831  grind832833/-- CONDITIONAL SHARPNESS (targets A + C + D combined).  Fix B ≥ 2, a structured834    head j < B, N ≥ 1 (written N + 1), and resource bounds d ≥ 9,835    s ≥ 10 ((N+3)(B+2))^8.  ASSUME the classical parity-correlation premise with836    error ε for formulas of depth ≤ d + 11 and size ≤ 12 U^10 (U = (N+3)(B+2)(s+2))837    on every m with N + 1 ≤ m ≤ B (N + 1).  Then:838    (1) the explicit attainability circuits lie in the class (RBound d s);839    (2) fed RO_{pi_j}, they succeed with conditional probability exactly 2/(q-1);840    (3) they satisfy CorrHyp with error ε;841    (4) every readout in the class succeeds with conditional probability842        ≤ 2/(q-1) + (q-1) ε.843    So the optimum over the class lies in [2/(q-1), 2/(q-1) + (q-1) ε]. -/844theorem conditional_sharpness {B N j d s : Nat} (hB : 2 ≤ B) (hj : j < B) (hd : 9 ≤ d)845    (hs : 10 * Ua (N + 1) B ^ 8 ≤ s) {ε : Rat}846    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →847      ParityCorrPremise (d + 11) (12 * Upar (N + 1) B s ^ 10) m ε) :848    (∀ b, RBound (attR B (N + 1) (fibreRep B (headVec j) false) (fibreRep B (headVec j) true) b)849      (N + 1) B d s) ∧850    succCountRO B (N + 1) (readoutOf B (attR B (N + 1) (fibreRep B (headVec j) false)851        (fibreRep B (headVec j) true))) j / nonzeroCount B (N + 1) =852      2 / (((2 ^ B : Nat) : Rat) - 1) ∧853    CorrHyp B (N + 1) (readoutOf B (attR B (N + 1) (fibreRep B (headVec j) false)854        (fibreRep B (headVec j) true))) ε ∧855    (∀ R : Bool → RCirc, (∀ b, RBound (R b) (N + 1) B d s) →856      succCountRO B (N + 1) (readoutOf B R) j / nonzeroCount B (N + 1) ≤857        2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε) := by858  have hw0 := headVec_ne_zero j859  have hwl := headVec_lt hj860  obtain ⟨n0, l0, _, _⟩ := fibreRep_spec hB hw0 hwl false861  obtain ⟨n1, l1, _, _⟩ := fibreRep_spec hB hw0 hwl true862  have hRB : ∀ b, RBound (attR B (N + 1) (fibreRep B (headVec j) false)863      (fibreRep B (headVec j) true) b) (N + 1) B d s := by864    intro b865    apply RBound_mono _ hd hs866    unfold attR867    cases b868    · exact attRC_RBound n0 l0869    · exact attRC_RBound n1 l1870  refine ⟨hRB, ?_, corrHyp_of_premise _ hRB hprem, fun R hR => circuit_readout_bound hj R hR hprem⟩871  rw [succCountRO_eq hj, succCount_attR n0 n1 l0 l1]872  exact attain_exact hB hw0 hwl873874/-- ASYMPTOTIC FORM (absolute-error convention).  Fix B ≥ 2, j < B, d ≥ 9 and size875    bounds s N ≥ 10 ((N+3)(B+2))^8.  If the premise holds for every N with error876    ε N and ε is negligible, then there is δ with δ N ≥ 0, δ negligible, such that877    for every N the explicit circuits succeed with exactly 2/(q-1) and every878    readout in the class succeeds with at most 2/(q-1) + δ N. -/879theorem asymptotic_sharpness {B j d : Nat} (hB : 2 ≤ B) (hj : j < B) (hd : 9 ≤ d)880    (s : Nat → Nat) (hs : ∀ N, 10 * Ua (N + 1) B ^ 8 ≤ s N) (ε : Nat → Rat) (hε : Negligible ε)881    (hprem : ∀ N m, N + 1 ≤ m → m ≤ B * (N + 1) →882      ParityCorrPremise (d + 11) (12 * Upar (N + 1) B (s N) ^ 10) m (ε N)) :883    ∃ δ : Nat → Rat, Negligible δ ∧ (∀ N, 0 ≤ δ N) ∧ ∀ N,884      succCountRO B (N + 1) (readoutOf B (attR B (N + 1) (fibreRep B (headVec j) false)885          (fibreRep B (headVec j) true))) j / nonzeroCount B (N + 1) =886        2 / (((2 ^ B : Nat) : Rat) - 1) ∧887      ∀ R : Bool → RCirc, (∀ b, RBound (R b) (N + 1) B d (s N)) →888        succCountRO B (N + 1) (readoutOf B R) j / nonzeroCount B (N + 1) ≤889          2 / (((2 ^ B : Nat) : Rat) - 1) + δ N := by890  refine ⟨fun N => ((2 ^ B - 1 : Nat) : Rat) * ε N, negligible_const_mul _ hε, ?_, ?_⟩891  · intro N892    have hpos : 1 ≤ 12 * Upar (N + 1) B (s N) ^ 10 := by893      have := (Upar_ge (N + 1) B (s N)).1894      have := Nat.pow_pos (n := 10) this895      omega896    have h0 := premise_nonneg hpos (hprem N (N + 1) (Nat.le_refl _)897      (by have := Nat.mul_le_mul_right (N + 1) (show 1 ≤ B by omega); omega))898    exact Rat.mul_nonneg Rat.natCast_nonneg h0899  · intro N900    obtain ⟨_, hex, _, hup⟩ := conditional_sharpness (N := N) hB hj hd (hs N) (hprem N)901    refine ⟨hex, fun R hR => ?_⟩902    rw [natCast_pred]903    exact hup R hR904905#print axioms cancel_iff_bit906#print axioms testBit_pred907#print axioms pos_iff_bit908#print axioms cancelIdx_firstTrue909#print axioms decIdx_firstTrue910#print axioms range_map_getD911#print axioms firstTrue_or912#print axioms firstTrue_lt913#print axioms attainF_eq914#print axioms firstC_eval915#print axioms cancel_eval916#print axioms nz_eval917#print axioms toNatBE_of_bits918#print axioms attR_correct919#print axioms succCount_attR920#print axioms Ua_ge921#print axioms mem_pair922#print axioms attRC_depth_size923#print axioms and_max'924#print axioms or_max'925#print axioms in_max926#print axioms attRC_max927#print axioms log2_lt928#print axioms attRC_RBound929#print axioms RBound_mono930#print axioms premise_nonneg931#print axioms conditional_sharpness932#print axioms asymptotic_sharpness933934end AttainCircuit935end NimAudit