NimCorrBridge

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 BitBridge23/- Phase 3, target D (paper-specific part).  Written by Claude (10 October 2026).4   Lean 4.26.0, core/Std only.56   Readouts given by circuits.  For each observed bit b the readout is a family of7   formulas on the N·B input bits (heap-major, big-endian): a validity formula,8   N selection formulas (chosen index = first true one) and B value formulas9   (big-endian new value).  `readoutOf` turns this into a phase-2 `Readout`.1011   From these formulas we BUILD explicit formulas for12     first-true index selection, the indexed old-heap bits, the legality test13     (value < selected heap, big-endian comparator), the delta XOR, and the14     equality indicator H_{b,a} = 1[g_b(P) = a],15   prove them correct, and bound depth (≤ d + 11) and size (≤ 12 U^10 with16   U = (N+2)(B+2)(s+2)).  Then, ASSUMING the classical parity-correlation premise17   for formulas of that depth and size on every m with N ≤ m ≤ N·B, we derive the18   phase-2 hypothesis CorrHyp B N (readoutOf R) ε.1920   CONDITIONAL: the classical AC0 parity-correlation theorem (Hastad et al.) is not21   formalised; it is the explicit hypothesis `ParityCorrPremise`.  No AC0 predicate22   is defined by its correlation property. -/2324namespace NimAudit25namespace CorrBridge2627open Prob AC0 AC0.Circ Game Bridge Rollout2829attribute [local simp] Rat.add_zero Rat.zero_add Rat.zero_mul Rat.mul_zero Rat.one_mul30  Rat.mul_one3132/-! ## Readouts given by circuits -/3334structure RCirc where35  valid : Circ36  sel : List Circ37  val : List Circ3839/-- Input bits of a board: heap i, big-endian position p (bit B-1-p) at index B·i + p. -/40def boardBits (B : Nat) (P : List Nat) : Nat → Bool := fun j =>41  if j < B * P.length then (P.getD (j / B) 0).testBit (B - 1 - j % B) else false4243def firstTrue : List Bool → Option Nat44  | [] => none45  | true :: _ => some 046  | false :: l => (firstTrue l).map (· + 1)4748/-- The readout computed by the circuit families R false, R true. -/49def readoutOf (B : Nat) (R : Bool → RCirc) : Readout := fun P b =>50  if eval (boardBits B P) (R b).valid then51    match firstTrue ((R b).sel.map (eval (boardBits B P))) with52    | some i => some (i, toNatBE ((R b).val.map (eval (boardBits B P))))53    | none => none54  else none5556theorem firstTrue_some_iff : ∀ (l : List Bool) (i : Nat),57    firstTrue l = some i ↔ i < l.length ∧ l.getD i false = true ∧ ∀ i' < i, l.getD i' false = false58  | [], i => by simp [firstTrue]59  | true :: l, 0 => by simp [firstTrue]60  | true :: l, i + 1 => by61    simp only [firstTrue, Option.some.injEq, List.getD_cons_succ, List.length_cons]62    constructor63    · intro h; omega64    · rintro ⟨_, _, h⟩; have := h 0 (by omega); simp at this65  | false :: l, 0 => by66    simp only [firstTrue, List.getD_cons_zero]67    cases firstTrue l <;> simp68  | false :: l, i + 1 => by69    simp only [firstTrue, List.getD_cons_succ, List.length_cons]70    rw [show (Option.map (· + 1) (firstTrue l) = some (i + 1)) ↔ firstTrue l = some i by71      cases firstTrue l <;> simp]72    rw [firstTrue_some_iff l i]73    constructor74    · rintro ⟨h1, h2, h3⟩75      refine ⟨by omega, h2, ?_⟩76      intro i' hi'77      cases i' with78      | zero => rfl79      | succ i' => simpa using h3 i' (by omega)80    · rintro ⟨h1, h2, h3⟩81      refine ⟨by omega, h2, ?_⟩82      intro i' hi'83      simpa using h3 (i' + 1) (by omega)8485/-! ## Building blocks -/8687def getC (cs : List Circ) (i : Nat) : Circ := cs.getD i (const false)8889theorem eval_getC (z : Nat → Bool) (cs : List Circ) (i : Nat) :90    eval z (getC cs i) = (cs.map (eval z)).getD i false := by91  unfold getC92  simp only [List.getD_eq_getElem?_getD, List.getElem?_map]93  cases cs[i]? <;> simp9495def selC (R : RCirc) (i : Nat) : Circ :=96  and (getC R.sel i :: (List.range i).map (fun i' => not (getC R.sel i')))9798def heapC (B i p : Nat) : Circ := input (B * i + p)99def valC (R : RCirc) (p : Nat) : Circ := getC R.val p100def eqC (a b : Circ) : Circ := or [and [a, b], and [not a, not b]]101def xor2 (a b : Circ) : Circ := or [and [a, not b], and [not a, b]]102103def ltC (R : RCirc) (B i : Nat) : Circ :=104  or ((List.range B).map (fun p =>105    and ([not (valC R p), heapC B i p] ++ (List.range p).map (fun p' => eqC (valC R p') (heapC B i p')))))106107def legalC (R : RCirc) (N B : Nat) : Circ :=108  and [R.valid, or ((List.range N).map (fun i => and [selC R i, ltC R B i]))]109110def gbitC (R : RCirc) (N B p : Nat) : Circ :=111  and [legalC R N B, or ((List.range N).map (fun i => and [selC R i, xor2 (valC R p) (heapC B i p)]))]112113/-- The indicator formula for H_{b,a} = 1[g_b(P) = a]. -/114def HC (R : RCirc) (N B a : Nat) : Circ :=115  and ((List.range B).map (fun p =>116    if a.testBit (B - 1 - p) then gbitC R N B p else not (gbitC R N B p)))117118theorem eval_eqC (z : Nat → Bool) (a b : Circ) : eval z (eqC a b) = (eval z a == eval z b) := by119  unfold eqC120  simp only [eval_or, eval_and, eval_not, List.all_cons, List.all_nil, List.any_cons, List.any_nil]121  generalize eval z a = p; generalize eval z b = q122  cases p <;> cases q <;> rfl123124theorem eval_xor2 (z : Nat → Bool) (a b : Circ) : eval z (xor2 a b) = xor (eval z a) (eval z b) := by125  unfold xor2126  simp only [eval_or, eval_and, eval_not, List.all_cons, List.all_nil, List.any_cons, List.any_nil]127  generalize eval z a = p; generalize eval z b = q128  cases p <;> cases q <;> rfl129130/-! ## Semantics on encoded boards -/131132section Semantics133134variable {B N : Nat} {P : List Nat} {R : RCirc}135136theorem boardBits_heap (hP : P.length = N) {i p : Nat} (hi : i < N) (hp : p < B) :137    boardBits B P (B * i + p) = (P.getD i 0).testBit (B - 1 - p) := by138  unfold boardBits139  have hB : 0 < B := by omega140  have h1 : B * i + p < B * P.length := by141    rw [hP]142    have := Nat.mul_le_mul_left B (show i + 1 ≤ N by omega)143    rw [Nat.mul_succ] at this; omega144  have h2 : (B * i + p) / B = i := by145    rw [Nat.mul_comm, Nat.add_comm, Nat.add_mul_div_right _ _ hB, Nat.div_eq_of_lt hp]; omega146  have h3 : (B * i + p) % B = p := by147    rw [Nat.mul_comm, Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hp]148  simp [h1, h2, h3]149150theorem selC_eval (z : Nat → Bool) (hsel : R.sel.length = N) {i : Nat} (hi : i < N) :151    eval z (selC R i) = decide (firstTrue (R.sel.map (eval z)) = some i) := by152  unfold selC153  rw [Bool.eq_iff_iff, decide_eq_true_iff, firstTrue_some_iff]154  simp only [eval_and, List.all_cons, List.all_map, Bool.and_eq_true, List.all_eq_true,155    List.mem_range, Function.comp, eval_not, Bool.not_eq_true', eval_getC, List.length_map, hsel]156  constructor157  · rintro ⟨h1, h2⟩; exact ⟨hi, h1, h2⟩158  · rintro ⟨_, h1, h2⟩; exact ⟨h1, h2⟩159160theorem val_eval (z : Nat → Bool) (hval : R.val.length = B) {p : Nat} (hp : p < B) :161    eval z (valC R p) = (toNatBE (R.val.map (eval z))).testBit (B - 1 - p) := by162  unfold valC163  rw [eval_getC]164  have := testBit_toNatBE (R.val.map (eval z)) p (by simp [hval, hp])165  simp only [List.length_map, hval] at this166  exact this.symm167168/-- Big-endian comparison via the top differing bit. -/169theorem lt_iff_top {v h B : Nat} (hv : v < 2 ^ B) (hh : h < 2 ^ B) :170    v < h ↔ ∃ p < B, v.testBit (B - 1 - p) = false ∧ h.testBit (B - 1 - p) = true ∧171      ∀ p' < p, v.testBit (B - 1 - p') = h.testBit (B - 1 - p') := by172  have above : ∀ x k, x < 2 ^ B → B ≤ k → x.testBit k = false := fun x k hx hk =>173    Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by decide) hk))174  constructor175  · intro hlt176    have hne : v ^^^ h ≠ 0 := fun e => by have := xor_eq_zero_imp e; omega177    let k := (v ^^^ h).log2178    have hk : (v ^^^ h).testBit k = true := by179      cases hb : (v ^^^ h).testBit k with180      | true => rfl181      | false =>182        exfalso183        have : v ^^^ h < 2 ^ k := by184          apply Nat.lt_pow_two_of_testBit185          intro i hi186          by_cases hik : i = k187          · subst hik; exact hb188          · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self189              (Nat.pow_le_pow_right (by decide) (by omega)))190        exact absurd (Nat.log2_self_le hne) (Nat.not_le.mpr this)191    have habove : ∀ i, k < i → v.testBit i = h.testBit i := by192      intro i hi193      have : (v ^^^ h).testBit i = false := Nat.testBit_lt_two_pow194        (Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (by omega)))195      rw [Nat.testBit_xor] at this196      revert this; cases v.testBit i <;> cases h.testBit i <;> simp197    have hkB : k < B := by198      rcases Nat.lt_or_ge k B with h' | h'199      · exact h'200      · rw [Nat.testBit_xor, above v k hv h', above h k hh h'] at hk; cases hk201    rw [Nat.testBit_xor] at hk202    have hvk : v.testBit k = false := by203      cases hvb : v.testBit k204      · rfl205      · exfalso206        have hhk : h.testBit k = false := by rw [hvb] at hk; revert hk; cases h.testBit k <;> simp207        have := lt_of_top_testBit hhk hvb (fun i hi => (habove i hi).symm)208        omega209    have hhk : h.testBit k = true := by rw [hvk] at hk; simpa using hk210    refine ⟨B - 1 - k, by omega, ?_, ?_, ?_⟩211    · rw [show B - 1 - (B - 1 - k) = k by omega]; exact hvk212    · rw [show B - 1 - (B - 1 - k) = k by omega]; exact hhk213    · intro p' hp'; exact habove _ (by omega)214  · rintro ⟨p, hp, h1, h2, h3⟩215    apply lt_of_top_testBit h1 h2216    intro i hi217    rcases Nat.lt_or_ge i B with hiB | hiB218    · have := h3 (B - 1 - i) (by omega)219      rwa [show B - 1 - (B - 1 - i) = i by omega] at this220    · rw [above v i hv hiB, above h i hh hiB]221222theorem ltC_eval (hP : P.length = N) (hw : Width B P) (hval : R.val.length = B)223    {i : Nat} (hi : i < N) :224    eval (boardBits B P) (ltC R B i) =225      decide (toNatBE (R.val.map (eval (boardBits B P))) < P.getD i 0) := by226  have hvlt : toNatBE (R.val.map (eval (boardBits B P))) < 2 ^ B := by227    have := toNatBE_lt (R.val.map (eval (boardBits B P))); simpa [hval] using this228  have hhlt : P.getD i 0 < 2 ^ B := by229    apply hw; simp only [List.getD_eq_getElem?_getD]230    rw [List.getElem?_eq_getElem (by omega)]; simp231  rw [Bool.eq_iff_iff, decide_eq_true_iff, lt_iff_top hvlt hhlt]232  unfold ltC233  simp only [eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp, eval_and,234    List.all_append, List.all_cons, List.all_nil, Bool.and_eq_true, eval_not, Bool.not_eq_true',235    List.all_map, List.all_eq_true, eval_eqC, beq_iff_eq, Bool.and_true]236  constructor237  · rintro ⟨p, hp, ⟨h1, h2⟩, h3⟩238    unfold heapC at h2 h3239    rw [val_eval _ hval hp] at h1240    rw [eval_input, boardBits_heap hP hi hp] at h2241    refine ⟨p, hp, h1, h2, ?_⟩242    intro p' hp'243    have := h3 p' hp'244    rw [val_eval _ hval (by omega), eval_input, boardBits_heap hP hi (by omega)] at this245    exact this246  · rintro ⟨p, hp, h1, h2, h3⟩247    refine ⟨p, hp, ⟨?_, ?_⟩, ?_⟩248    · rw [val_eval _ hval hp]; exact h1249    · unfold heapC; rw [eval_input, boardBits_heap hP hi hp]; exact h2250    · intro p' hp'251      unfold heapC252      rw [val_eval _ hval (by omega), eval_input, boardBits_heap hP hi (by omega)]253      exact h3 p' hp'254255/-- The value g_b(P) of the circuit readout. -/256theorem gval_readoutOf (R' : Bool → RCirc) (b : Bool) (P : List Nat) :257    gval (readoutOf B R') b P =258      if eval (boardBits B P) (R' b).valid = true then259        match firstTrue ((R' b).sel.map (eval (boardBits B P))) with260        | some i => (match P[i]? with261            | some x => if toNatBE ((R' b).val.map (eval (boardBits B P))) < x then262                x ^^^ toNatBE ((R' b).val.map (eval (boardBits B P))) else 0263            | none => 0)264        | none => 0265      else 0 := by266  unfold gval readoutOf267  by_cases hv : eval (boardBits B P) (R' b).valid = true268  · simp only [hv, if_true]269    cases firstTrue ((R' b).sel.map (eval (boardBits B P))) <;> rfl270  · simp [hv]271272theorem legalC_eval (hP : P.length = N) (hw : Width B P) (hsel : R.sel.length = N)273    (hval : R.val.length = B) :274    eval (boardBits B P) (legalC R N B) =275      decide (eval (boardBits B P) R.valid = true ∧ ∃ i, i < N ∧276        firstTrue (R.sel.map (eval (boardBits B P))) = some i ∧277        toNatBE (R.val.map (eval (boardBits B P))) < P.getD i 0) := by278  unfold legalC279  rw [Bool.eq_iff_iff, decide_eq_true_iff]280  simp only [eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true, eval_or,281    List.any_map, List.any_eq_true, List.mem_range, Function.comp]282  constructor283  · rintro ⟨h1, i, hi, h2, h3⟩284    rw [selC_eval _ hsel hi, decide_eq_true_iff] at h2285    rw [ltC_eval hP hw hval hi, decide_eq_true_iff] at h3286    exact ⟨h1, i, hi, h2, h3⟩287  · rintro ⟨h1, i, hi, h2, h3⟩288    refine ⟨h1, i, hi, ?_, ?_⟩289    · rw [selC_eval _ hsel hi, decide_eq_true_iff]; exact h2290    · rw [ltC_eval hP hw hval hi, decide_eq_true_iff]; exact h3291292theorem gval_legal (R' : Bool → RCirc) (b : Bool) {i : Nat} (hP : P.length = N)293    (hv : eval (boardBits B P) (R' b).valid = true)294    (hf : firstTrue ((R' b).sel.map (eval (boardBits B P))) = some i) (hi : i < N)295    (hlt : toNatBE ((R' b).val.map (eval (boardBits B P))) < P.getD i 0) :296    gval (readoutOf B R') b P = P.getD i 0 ^^^ toNatBE ((R' b).val.map (eval (boardBits B P))) := by297  rw [gval_readoutOf]298  have hPi : P[i]? = some (P.getD i 0) := by299    simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp300  simp only [hv, if_true, hf, hPi, hlt]301302theorem gval_illegal (R' : Bool → RCirc) (b : Bool) (hP : P.length = N)303    (h : ¬ (eval (boardBits B P) (R' b).valid = true ∧ ∃ i, i < N ∧304      firstTrue ((R' b).sel.map (eval (boardBits B P))) = some i ∧305      toNatBE ((R' b).val.map (eval (boardBits B P))) < P.getD i 0)) :306    gval (readoutOf B R') b P = 0 := by307  rw [gval_readoutOf]308  by_cases hv : eval (boardBits B P) (R' b).valid = true309  · simp only [hv, if_true]310    cases hf : firstTrue ((R' b).sel.map (eval (boardBits B P))) with311    | none => rfl312    | some i =>313      simp only314      by_cases hi : i < N315      · have hPi : P[i]? = some (P.getD i 0) := by316          simp only [List.getD_eq_getElem?_getD]; rw [List.getElem?_eq_getElem (by omega)]; simp317        simp only [hPi]318        by_cases hlt : toNatBE ((R' b).val.map (eval (boardBits B P))) < P.getD i 0319        · exact absurd ⟨hv, i, hi, hf, hlt⟩ h320        · rw [if_neg hlt]321      · simp [List.getElem?_eq_none (show P.length ≤ i by omega)]322  · simp [hv]323324/-- Each g-bit formula computes the corresponding bit of g_b(P). -/325theorem gbitC_eval (R' : Bool → RCirc) (b : Bool) (hP : P.length = N) (hw : Width B P)326    (hsel : (R' b).sel.length = N) (hval : (R' b).val.length = B) {p : Nat} (hp : p < B) :327    eval (boardBits B P) (gbitC (R' b) N B p) = (gval (readoutOf B R') b P).testBit (B - 1 - p) := by328  have hL := legalC_eval (R := R' b) hP hw hsel hval329  unfold gbitC330  simp only [eval_and, List.all_cons, List.all_nil, Bool.and_true]331  rw [hL]332  by_cases hleg : eval (boardBits B P) (R' b).valid = true ∧ ∃ i, i < N ∧333      firstTrue ((R' b).sel.map (eval (boardBits B P))) = some i ∧334      toNatBE ((R' b).val.map (eval (boardBits B P))) < P.getD i 0335  · obtain ⟨hv, i, hi, hf, hlt⟩ := hleg336    rw [gval_legal R' b hP hv hf hi hlt, decide_eq_true ⟨hv, i, hi, hf, hlt⟩, Bool.true_and,337      Nat.testBit_xor]338    apply Bool.eq_iff_iff.mpr339    simp only [eval_or, List.any_map, List.any_eq_true, List.mem_range, Function.comp, eval_and,340      List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true]341    constructor342    · rintro ⟨i', hi', hs, hx⟩343      rw [selC_eval _ hsel hi', decide_eq_true_iff, hf] at hs344      cases hs345      rw [eval_xor2, val_eval _ hval hp, heapC, eval_input, boardBits_heap hP hi' hp] at hx346      rw [Bool.xor_comm]; exact hx347    · intro hx348      refine ⟨i, hi, ?_, ?_⟩349      · rw [selC_eval _ hsel hi, decide_eq_true_iff]; exact hf350      · rw [eval_xor2, val_eval _ hval hp, heapC, eval_input, boardBits_heap hP hi hp]351        rw [Bool.xor_comm]; exact hx352  · rw [gval_illegal R' b hP hleg, decide_eq_false hleg, Bool.false_and, Nat.zero_testBit]353354theorem gval_lt (R' : Bool → RCirc) (b : Bool) (hw : Width B P) (hval : (R' b).val.length = B) :355    gval (readoutOf B R') b P < 2 ^ B := by356  rw [gval_readoutOf]357  have hvlt : toNatBE ((R' b).val.map (eval (boardBits B P))) < 2 ^ B := by358    have := toNatBE_lt ((R' b).val.map (eval (boardBits B P))); simpa [hval] using this359  split360  · split361    · next i _ =>362      split363      · next x hx =>364        split365        · exact Nat.xor_lt_two_pow (hw x (List.mem_of_getElem? hx)) hvlt366        · exact Nat.two_pow_pos B367      · exact Nat.two_pow_pos B368    · exact Nat.two_pow_pos B369  · exact Nat.two_pow_pos B370371/-- INDICATOR CORRECTNESS: on boards of N heaps below 2^B and a < 2^B,372    the formula HC evaluates to 1[g_b(P) = a]. -/373theorem HC_eval (R' : Bool → RCirc) (b : Bool) (hP : P.length = N) (hw : Width B P)374    (hsel : (R' b).sel.length = N) (hval : (R' b).val.length = B) {a : Nat} (ha : a < 2 ^ B) :375    eval (boardBits B P) (HC (R' b) N B a) = decide (gval (readoutOf B R') b P = a) := by376  have hg := gval_lt R' b hw hval377  unfold HC378  rw [Bool.eq_iff_iff, decide_eq_true_iff]379  simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp]380  constructor381  · intro h382    apply Nat.eq_of_testBit_eq383    intro k384    rcases Nat.lt_or_ge k B with hk | hk385    · have := h (B - 1 - k) (by omega)386      rw [show B - 1 - (B - 1 - k) = k by omega] at this387      have hb := gbitC_eval R' b hP hw hsel hval (p := B - 1 - k) (by omega)388      rw [show B - 1 - (B - 1 - k) = k by omega] at hb389      revert this390      split391      · next hak => intro h1; rw [hb] at h1; rw [h1, hak]392      · next hak =>393        intro h1; simp only [eval_not, Bool.not_eq_true'] at h1394        rw [hb] at h1; rw [h1]; simpa using hak395    · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hg (Nat.pow_le_pow_right (by decide) hk)),396        Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le ha (Nat.pow_le_pow_right (by decide) hk))]397  · intro he p hp398    have hb := gbitC_eval R' b hP hw hsel hval hp399    rw [he] at hb400    split401    · next hak => rw [hb, hak]402    · next hak => simp only [eval_not, hb]; simpa using hak403404end Semantics405406/-! ## Encoded boards: boardBits agrees with the bit vector -/407408theorem getD_take_drop (x : List Bool) (k p B : Nat) (hp : p < B) :409    ((x.drop k).take B).getD p false = x.getD (k + p) false := by410  simp [List.getD_eq_getElem?_getD, List.getElem?_take, hp, List.getElem?_drop]411412theorem decodeBoard_getD (B : Nat) : ∀ (N : Nat) (x : List Bool) (i : Nat), i < N →413    (decodeBoard B N x).getD i 0 = toNatBE ((x.drop (B * i)).take B)414  | 0, _, i, hi => by omega415  | N + 1, x, 0, _ => by simp [decodeBoard]416  | N + 1, x, i + 1, hi => by417    simp only [decodeBoard, List.getD_cons_succ]418    rw [decodeBoard_getD B N (x.drop B) i (by omega), List.drop_drop, Nat.mul_succ, Nat.add_comm]419420theorem boardBits_decode {B N : Nat} {x : List Bool} (hx : x ∈ bitvecs (B * N)) :421    boardBits B (decodeBoard B N x) = vfun x := by422  funext j423  have hl := mem_bitvecs_length hx424  unfold boardBits vfun425  rw [length_decodeBoard]426  by_cases hj : j < B * N427  · simp only [hj, if_true]428    have hB : 0 < B := by429      rcases Nat.eq_zero_or_pos B with h | h430      · subst h; simp at hj431      · exact h432    have hi : j / B < N := by433      rw [Nat.div_lt_iff_lt_mul hB, Nat.mul_comm]; exact hj434    rw [decodeBoard_getD B N x (j / B) hi]435    have hm : j % B < B := Nat.mod_lt _ hB436    have hlen : ((x.drop (B * (j / B))).take B).length = B := by437      simp only [List.length_take, List.length_drop, hl]438      have := Nat.mul_le_mul_left B (show j / B + 1 ≤ N by omega)439      rw [Nat.mul_succ] at this440      omega441    have := testBit_toNatBE ((x.drop (B * (j / B))).take B) (j % B) (by rw [hlen]; exact hm)442    rw [hlen] at this443    rw [this, getD_take_drop x _ _ _ hm, Nat.div_add_mod]444  · simp only [hj, if_false]445    simp [List.getD_eq_getElem?_getD, List.getElem?_eq_none (show x.length ≤ j by omega)]446447/-! ## Depth and size bounds -/448449section Bounds450451theorem depth_and_le {cs : List Circ} {D : Nat} (h : ∀ c ∈ cs, depth c ≤ D) :452    depth (and cs) ≤ D + 1 := by453  simp only [depth_and]454  have : listMax (cs.map depth) ≤ D := by455    apply listMax_le; intro a ha456    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc457  omega458459theorem depth_or_le {cs : List Circ} {D : Nat} (h : ∀ c ∈ cs, depth c ≤ D) :460    depth (or cs) ≤ D + 1 := by461  simp only [depth_or]462  have : listMax (cs.map depth) ≤ D := by463    apply listMax_le; intro a ha464    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc465  omega466467theorem sum_le_len_mul {cs : List Circ} {S : Nat} (h : ∀ c ∈ cs, size c ≤ S) :468    (cs.map size).sum ≤ cs.length * S := by469  have := sum_map_le_mem (l := cs) (f := size) (g := fun _ => S) h470  rw [List.map_const', List.sum_replicate_nat] at this471  exact this472473theorem upow_pos {U k : Nat} (hU : 1 ≤ U) : 1 ≤ U ^ k := Nat.pow_pos hU474475theorem size_and_le {cs : List Circ} {a k U : Nat} (hU : 1 ≤ U) (hl : cs.length ≤ U)476    (h : ∀ c ∈ cs, size c ≤ a * U ^ k) : size (and cs) ≤ (a + 1) * U ^ (k + 1) := by477  simp only [size_and]478  have h1 := sum_le_len_mul h479  have h2 : cs.length * (a * U ^ k) ≤ U * (a * U ^ k) := Nat.mul_le_mul_right _ hl480  have h3 : U * (a * U ^ k) = a * U ^ (k + 1) := by rw [Nat.pow_succ]; grind481  have h4 := upow_pos (k := k + 1) hU482  rw [Nat.add_mul, Nat.one_mul]483  omega484485theorem size_or_le {cs : List Circ} {a k U : Nat} (hU : 1 ≤ U) (hl : cs.length ≤ U)486    (h : ∀ c ∈ cs, size c ≤ a * U ^ k) : size (or cs) ≤ (a + 1) * U ^ (k + 1) := by487  simp only [size_or]488  have h1 := sum_le_len_mul h489  have h2 : cs.length * (a * U ^ k) ≤ U * (a * U ^ k) := Nat.mul_le_mul_right _ hl490  have h3 : U * (a * U ^ k) = a * U ^ (k + 1) := by rw [Nat.pow_succ]; grind491  have h4 := upow_pos (k := k + 1) hU492  rw [Nat.add_mul, Nat.one_mul]493  omega494495theorem size_lift {c : Circ} {a a' k k' U : Nat} (hU : 1 ≤ U) (h : size c ≤ a * U ^ k)496    (ha : a ≤ a') (hk : k ≤ k') : size c ≤ a' * U ^ k' :=497  Nat.le_trans h (Nat.mul_le_mul ha (Nat.pow_le_pow_right hU hk))498499theorem size_not_le {c : Circ} {a k U : Nat} (hU : 1 ≤ U) (h : size c ≤ a * U ^ k) :500    size (not c) ≤ (a + 1) * U ^ k := by501  simp only [size_not]502  have := upow_pos (k := k) hU503  rw [Nat.add_mul, Nat.one_mul]; omega504505/-- Resource hypotheses on the readout formulas. -/506structure RBound (R : RCirc) (N B d s : Nat) : Prop where507  sel_len : R.sel.length = N508  val_len : R.val.length = B509  depth_valid : depth R.valid ≤ d510  depth_sel : ∀ c ∈ R.sel, depth c ≤ d511  depth_val : ∀ c ∈ R.val, depth c ≤ d512  size_valid : size R.valid ≤ s513  size_sel : ∀ c ∈ R.sel, size c ≤ s514  size_val : ∀ c ∈ R.val, size c ≤ s515  max_valid : maxInput R.valid ≤ B * N516  max_sel : ∀ c ∈ R.sel, maxInput c ≤ B * N517  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N518519/-- The polynomial size parameter U = (N+2)(B+2)(s+2). -/520def Upar (N B s : Nat) : Nat := (N + 2) * (B + 2) * (s + 2)521522variable {R : RCirc} {N B d s : Nat}523524theorem Upar_ge (N B s : Nat) : 1 ≤ Upar N B s ∧ N + 1 ≤ Upar N B s ∧ B + 2 ≤ Upar N B s ∧525    s ≤ Upar N B s := by526  unfold Upar527  have h1 : 1 ≤ (N + 2) * (B + 2) := Nat.mul_pos (by omega) (by omega)528  refine ⟨Nat.mul_pos h1 (by omega), ?_, ?_, ?_⟩529  · have := Nat.mul_le_mul (show N + 2 ≤ (N + 2) * (B + 2) from Nat.le_mul_of_pos_right _ (by omega))530      (show 1 ≤ s + 2 by omega)531    omega532  · have := Nat.mul_le_mul (show B + 2 ≤ (N + 2) * (B + 2) from Nat.le_mul_of_pos_left _ (by omega))533      (show 1 ≤ s + 2 by omega)534    omega535  · have := Nat.mul_le_mul h1 (show s + 2 ≤ s + 2 from Nat.le_refl _)536    omega537538theorem getC_size (hb : RBound R N B d s) (cs : List Circ) (hcs : ∀ c ∈ cs, size c ≤ s) (i : Nat) :539    size (getC cs i) ≤ 1 * Upar N B s ^ 1 := by540  have hU := (Upar_ge N B s).2.2.2541  unfold getC542  simp only [List.getD_eq_getElem?_getD]543  cases h : cs[i]? with544  | none => simp; exact (Upar_ge N B s).1545  | some c => simp; exact Nat.le_trans (hcs c (List.mem_of_getElem? h)) hU546547theorem getC_depth (cs : List Circ) (hcs : ∀ c ∈ cs, depth c ≤ d) (i : Nat) : depth (getC cs i) ≤ d := by548  unfold getC549  simp only [List.getD_eq_getElem?_getD]550  cases h : cs[i]? with551  | none => simp552  | some c => simp; exact hcs c (List.mem_of_getElem? h)553554theorem getC_max (cs : List Circ) (m : Nat) (hcs : ∀ c ∈ cs, maxInput c ≤ m) (i : Nat) :555    maxInput (getC cs i) ≤ m := by556  unfold getC557  simp only [List.getD_eq_getElem?_getD]558  cases h : cs[i]? with559  | none => simp560  | some c => simp; exact hcs c (List.mem_of_getElem? h)561562/-- DEPTH BOUND: HC has depth ≤ d + 11. -/563theorem HC_depth (hb : RBound R N B d s) (a : Nat) : depth (HC R N B a) ≤ d + 11 := by564  have hsel := getC_depth R.sel hb.depth_sel565  have hval := getC_depth R.val hb.depth_val566  have hselC : ∀ i, depth (selC R i) ≤ d + 2 := by567    intro i; unfold selC568    apply depth_and_le569    intro c hc570    simp only [List.mem_cons, List.mem_map, List.mem_range] at hc571    rcases hc with rfl | ⟨i', _, rfl⟩572    · have := hsel i; omega573    · simp; have := hsel i'; omega574  have heq : ∀ p' i, depth (eqC (valC R p') (heapC B i p')) ≤ d + 3 := by575    intro p' i; unfold eqC valC heapC576    apply depth_or_le; intro c hc577    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc578    rcases hc with rfl | rfl <;> apply depth_and_le <;> intro c hc <;>579      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc <;>580      rcases hc with rfl | rfl <;> (try simp) <;> have := hval p' <;> omega581  have hlt : ∀ i, depth (ltC R B i) ≤ d + 5 := by582    intro i; unfold ltC583    apply depth_or_le; intro c hc584    obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc585    have : depth (and ([not (valC R p), heapC B i p] ++586        (List.range p).map (fun p' => eqC (valC R p') (heapC B i p')))) ≤ d + 4 := by587      apply depth_and_le; intro c hc588      simp only [List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map] at hc589      rcases hc with (rfl | rfl) | ⟨p', _, rfl⟩590      · unfold valC; simp; have := hval p; omega591      · unfold heapC; simp592      · exact heq p' i593    omega594  have hlegal : depth (legalC R N B) ≤ d + 8 := by595    unfold legalC596    apply depth_and_le; intro c hc597    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc598    rcases hc with rfl | rfl599    · have := hb.depth_valid; omega600    · apply depth_or_le; intro c hc601      obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc602      apply depth_and_le; intro c hc603      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc604      rcases hc with rfl | rfl605      · have := hselC i; omega606      · exact hlt i607  have hgbit : ∀ p, depth (gbitC R N B p) ≤ d + 9 := by608    intro p; unfold gbitC609    apply depth_and_le; intro c hc610    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc611    rcases hc with rfl | rfl612    · exact hlegal613    · apply depth_or_le; intro c hc614      obtain ⟨i, _, rfl⟩ := List.mem_map.mp hc615      apply depth_and_le; intro c hc616      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc617      rcases hc with rfl | rfl618      · have := hselC i; omega619      · unfold xor2 valC heapC620        apply depth_or_le; intro c hc621        simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc622        have hv := hval p623        rcases hc with rfl | rfl <;> apply depth_and_le <;> intro c hc <;>624          simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc <;>625          rcases hc with rfl | rfl <;> (try simp) <;> omega626  unfold HC627  apply depth_and_le; intro c hc628  obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc629  split630  · have := hgbit p; omega631  · simp; have := hgbit p; omega632633/-- SIZE BOUND: HC has size ≤ 12 U^10 with U = (N+2)(B+2)(s+2). -/634theorem HC_size (hb : RBound R N B d s) (a : Nat) : size (HC R N B a) ≤ 12 * Upar N B s ^ 10 := by635  obtain ⟨hU1, hUN, hUB, hUs⟩ := Upar_ge N B s636  generalize hUdef : Upar N B s = U at *637  have base : ∀ c, c = R.valid ∨ (∃ i, c = getC R.sel i) ∨ (∃ p, c = getC R.val p) ∨638      (∃ j, c = input j) → size c ≤ 1 * U ^ 1 := by639    intro c hc640    rcases hc with rfl | ⟨i, rfl⟩ | ⟨p, rfl⟩ | ⟨j, rfl⟩641    · simp; exact Nat.le_trans hb.size_valid hUs642    · have := getC_size hb R.sel hb.size_sel i; rw [hUdef] at this; exact this643    · have := getC_size hb R.val hb.size_val p; rw [hUdef] at this; exact this644    · simp; exact hU1645  have hselC : ∀ i, i < N → size (selC R i) ≤ 3 * U ^ 2 := by646    intro i hi; unfold selC647    apply size_and_le hU1 (by simp; omega)648    intro c hc649    simp only [List.mem_cons, List.mem_map, List.mem_range] at hc650    rcases hc with rfl | ⟨i', _, rfl⟩651    · exact size_lift hU1 (base _ (Or.inr (Or.inl ⟨i, rfl⟩))) (by omega) (Nat.le_refl _)652    · exact size_not_le hU1 (base _ (Or.inr (Or.inl ⟨i', rfl⟩)))653  have hvalU : ∀ p, size (valC R p) ≤ 1 * U ^ 1 := fun p => base _ (Or.inr (Or.inr (Or.inl ⟨p, rfl⟩)))654  have hheapU : ∀ i p, size (heapC B i p) ≤ 1 * U ^ 1 := fun i p =>655    base _ (Or.inr (Or.inr (Or.inr ⟨_, rfl⟩)))656  have hpair : ∀ x y : Circ, size x ≤ 1 * U ^ 1 → size y ≤ 1 * U ^ 1 →657      size (or [and [x, not y], and [not x, y]]) ≤ 4 * U ^ 3 ∧658      size (or [and [x, y], and [not x, not y]]) ≤ 4 * U ^ 3 := by659    intro x y hx hy660    have hnx := size_not_le hU1 hx661    have hny := size_not_le hU1 hy662    have l2 : (2 : Nat) ≤ U := by omega663    have a1 : size (and [x, not y]) ≤ 3 * U ^ 2 := by664      apply size_and_le hU1 (by simp; omega); intro c hc665      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc666      rcases hc with rfl | rfl667      · exact size_lift hU1 hx (by omega) (Nat.le_refl _)668      · exact hny669    have a2 : size (and [not x, y]) ≤ 3 * U ^ 2 := by670      apply size_and_le hU1 (by simp; omega); intro c hc671      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc672      rcases hc with rfl | rfl673      · exact hnx674      · exact size_lift hU1 hy (by omega) (Nat.le_refl _)675    have a3 : size (and [x, y]) ≤ 3 * U ^ 2 := by676      apply size_and_le hU1 (by simp; omega); intro c hc677      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc678      rcases hc with rfl | rfl679      · exact size_lift hU1 hx (by omega) (Nat.le_refl _)680      · exact size_lift hU1 hy (by omega) (Nat.le_refl _)681    have a4 : size (and [not x, not y]) ≤ 3 * U ^ 2 := by682      apply size_and_le hU1 (by simp; omega); intro c hc683      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc684      rcases hc with rfl | rfl685      · exact hnx686      · exact hny687    constructor688    · apply size_or_le hU1 (by simp; omega); intro c hc689      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc690      rcases hc with rfl | rfl691      · exact a1692      · exact a2693    · apply size_or_le hU1 (by simp; omega); intro c hc694      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc695      rcases hc with rfl | rfl696      · exact a3697      · exact a4698  have hlt : ∀ i, size (ltC R B i) ≤ 6 * U ^ 5 := by699    intro i; unfold ltC700    apply size_or_le hU1 (by simp; omega); intro c hc701    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc702    have hp' := List.mem_range.mp hp703    apply size_and_le hU1 (by simp; omega); intro c hc704    simp only [List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map] at hc705    rcases hc with (rfl | rfl) | ⟨p', _, rfl⟩706    · exact size_lift hU1 (size_not_le hU1 (hvalU p)) (by omega) (by omega)707    · exact size_lift hU1 (hheapU i p) (by omega) (by omega)708    · exact (hpair _ _ (hvalU p') (hheapU i p')).2709  have hlegal : size (legalC R N B) ≤ 9 * U ^ 8 := by710    unfold legalC711    apply size_and_le hU1 (by simp; omega); intro c hc712    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc713    rcases hc with rfl | rfl714    · exact size_lift hU1 (base _ (Or.inl rfl)) (by omega) (by omega)715    · apply size_or_le hU1 (by simp; omega); intro c hc716      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc717      apply size_and_le hU1 (by simp; omega); intro c hc718      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc719      rcases hc with rfl | rfl720      · exact size_lift hU1 (hselC i (List.mem_range.mp hi)) (by omega) (by omega)721      · exact hlt i722  have hgbit : ∀ p, size (gbitC R N B p) ≤ 10 * U ^ 9 := by723    intro p; unfold gbitC724    apply size_and_le hU1 (by simp; omega); intro c hc725    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc726    rcases hc with rfl | rfl727    · exact hlegal728    · have : size (or ((List.range N).map (fun i => and [selC R i, xor2 (valC R p) (heapC B i p)]))) ≤729          6 * U ^ 5 := by730        apply size_or_le hU1 (by simp; omega); intro c hc731        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc732        apply size_and_le hU1 (by simp; omega); intro c hc733        simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc734        rcases hc with rfl | rfl735        · exact size_lift hU1 (hselC i (List.mem_range.mp hi)) (by omega) (by omega)736        · exact (hpair _ _ (hvalU p) (hheapU i p)).1737      exact size_lift hU1 this (by omega) (by omega)738  unfold HC739  apply size_and_le hU1 (by simp; omega); intro c hc740  obtain ⟨p, _, rfl⟩ := List.mem_map.mp hc741  split742  · exact size_lift hU1 (hgbit p) (by omega) (Nat.le_refl _)743  · exact size_not_le hU1 (hgbit p)744745/-- HC reads only the N·B board bits. -/746theorem HC_max (hb : RBound R N B d s) (a : Nat) : maxInput (HC R N B a) ≤ B * N := by747  have hheap : ∀ i p, i < N → p < B → maxInput (heapC B i p) ≤ B * N := by748    intro i p hi hp749    unfold heapC; simp750    have := Nat.mul_le_mul_left B (show i + 1 ≤ N by omega)751    rw [Nat.mul_succ] at this; omega752  have hsel := getC_max R.sel (B * N) hb.max_sel753  have hval := getC_max R.val (B * N) hb.max_val754  have and_max : ∀ cs : List Circ, (∀ c ∈ cs, maxInput c ≤ B * N) → maxInput (and cs) ≤ B * N := by755    intro cs h; simp only [maxInput_and]; apply listMax_le; intro a ha756    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc757  have or_max : ∀ cs : List Circ, (∀ c ∈ cs, maxInput c ≤ B * N) → maxInput (or cs) ≤ B * N := by758    intro cs h; simp only [maxInput_or]; apply listMax_le; intro a ha759    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc760  have hselC : ∀ i, maxInput (selC R i) ≤ B * N := by761    intro i; unfold selC; apply and_max; intro c hc762    simp only [List.mem_cons, List.mem_map, List.mem_range] at hc763    rcases hc with rfl | ⟨i', _, rfl⟩764    · exact hsel i765    · simp; exact hsel i'766  have hpair : ∀ x y : Circ, maxInput x ≤ B * N → maxInput y ≤ B * N →767      maxInput (or [and [x, not y], and [not x, y]]) ≤ B * N ∧768      maxInput (or [and [x, y], and [not x, not y]]) ≤ B * N := by769    intro x y hx hy770    constructor <;> apply or_max <;> intro c hc <;>771      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc <;>772      rcases hc with rfl | rfl <;> apply and_max <;> intro c hc <;>773      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc <;>774      rcases hc with rfl | rfl <;> (try simp only [maxInput_not]) <;> assumption775  have hlt : ∀ i, i < N → maxInput (ltC R B i) ≤ B * N := by776    intro i hi; unfold ltC; apply or_max; intro c hc777    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc778    have hp' := List.mem_range.mp hp779    apply and_max; intro c hc780    simp only [List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map] at hc781    rcases hc with (rfl | rfl) | ⟨p', hp'', rfl⟩782    · simp; exact hval p783    · exact hheap i p hi hp'784    · exact (hpair _ _ (hval p') (hheap i p' hi (by have := List.mem_range.mp hp''; omega))).2785  have hlegal : maxInput (legalC R N B) ≤ B * N := by786    unfold legalC; apply and_max; intro c hc787    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc788    rcases hc with rfl | rfl789    · exact hb.max_valid790    · apply or_max; intro c hc791      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc792      apply and_max; intro c hc793      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc794      rcases hc with rfl | rfl795      · exact hselC i796      · exact hlt i (List.mem_range.mp hi)797  have hgbit : ∀ p, p < B → maxInput (gbitC R N B p) ≤ B * N := by798    intro p hp; unfold gbitC; apply and_max; intro c hc799    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc800    rcases hc with rfl | rfl801    · exact hlegal802    · apply or_max; intro c hc803      obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc804      apply and_max; intro c hc805      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc806      rcases hc with rfl | rfl807      · exact hselC i808      · exact (hpair _ _ (hval p) (hheap i p (List.mem_range.mp hi) hp)).1809  unfold HC; apply and_max; intro c hc810  obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc811  have := hgbit p (List.mem_range.mp hp)812  split813  · exact this814  · simp; exact this815816end Bounds817818/-! ## The conditional bridge to CorrHyp -/819820/-- CONDITIONAL BRIDGE (paper Appendix G(i), circuit part).  Let the readout be821    given, for each observed bit b, by formulas R b with the resource bounds of822    `RBound` (depth ≤ d, size ≤ s, reading the N·B input bits).  ASSUME the823    classical parity-correlation premise for formulas of depth ≤ d + 11 and size824    ≤ 12 U^10 (U = (N+2)(B+2)(s+2)) on every m with N ≤ m ≤ B·N, with error ε.825    Then the phase-2 hypothesis CorrHyp B N (readoutOf B R) ε holds. -/826theorem corrHyp_of_premise {B N d s : Nat} (R : Bool → RCirc)827    (hb : ∀ b, RBound (R b) N B d s) {ε : Rat}828    (hprem : ∀ m, N ≤ m → m ≤ B * N → ParityCorrPremise (d + 11) (12 * Upar N B s ^ 10) m ε) :829    CorrHyp B N (readoutOf B R) ε := by830  intro b a u ha hu0 hu831  -- the mask for chi_u832  let mask := maskU B N u833  have hml : mask.length = B * N := length_maskU B N u834  have hones : N ≤ ones mask ∧ ones mask ≤ B * N := by835    have h1 := ones_maskU B N u836    have h2 := ones_toBitsBE_pos (by omega) hu837    have h3 : ones (toBitsBE B u) ≤ B := by838      have := ones_le_length (toBitsBE B u); rwa [length_toBitsBE] at this839    constructor840    · show N ≤ ones (maskU B N u)841      rw [h1]; have := Nat.mul_le_mul_left N h2; omega842    · show ones (maskU B N u) ≤ B * N843      rw [h1, Nat.mul_comm B N]; exact Nat.mul_le_mul_left N h3844  have hC := masked_correlation mask (HC (R b) N B a)845    (by rw [hml]; exact HC_max (hb b) a) (HC_depth (hb b) a) (HC_size (hb b) a)846    (hprem (ones mask) hones.1 hones.2)847  rw [hml] at hC848  -- identify the phase-2 correlation with the masked correlation849  have e : corr B N (readoutOf B R) b a u =850      rsum (bitvecs (B * N)) (fun x => ind (eval (vfun x) (HC (R b) N B a)) * sgn (pm mask x)) /851        (2 : Rat) ^ (B * N) := by852    unfold corr expect T853    rw [rsum_boards_bitvecs]854    have hT : ((2 ^ B : Nat) : Rat) ^ N = (2 : Rat) ^ (B * N) := by855      rw [← Rat.natCast_pow, ← Nat.pow_mul]; simp856    rw [hT]857    congr 1858    apply rsum_congr859    intro x hx860    have hw := decodeBoard_width hx861    have hl := length_decodeBoard B N x862    have hH : H (readoutOf B R) b a (decodeBoard B N x) = ind (eval (vfun x) (HC (R b) N B a)) := by863      unfold H ind864      rw [← boardBits_decode hx, HC_eval R b hl hw (hb b).sel_len (hb b).val_len ha]865      by_cases h : gval (readoutOf B R) b (decodeBoard B N x) = a <;> simp [h]866    have hchi : chi B u (nimSum (decodeBoard B N x)) = sgn (pm mask x) := by867      unfold chi sgn868      rw [chi_parity B N u hx]869    rw [hH, hchi]870  rw [e]871  exact hC872873/-- Combined with phase 2: under the same premise, the circuit readout fed the874    executed outcome of head pi_j succeeds with conditional probability at most875    2/(2^B-1) + (2^B-1) ε. -/876theorem circuit_readout_bound {B N j d s : Nat} (hj : j < B) (R : Bool → RCirc)877    (hb : ∀ b, RBound (R b) (N + 1) B d s) {ε : Rat}878    (hprem : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →879      ParityCorrPremise (d + 11) (12 * Upar (N + 1) B s ^ 10) m ε) :880    succCountRO B (N + 1) (readoutOf B R) j / nonzeroCount B (N + 1) ≤881      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε :=882  structured_head_bound hj _ (corrHyp_of_premise R hb hprem)883884#print axioms firstTrue_some_iff885#print axioms eval_getC886#print axioms eval_eqC887#print axioms eval_xor2888#print axioms boardBits_heap889#print axioms selC_eval890#print axioms val_eval891#print axioms lt_iff_top892#print axioms ltC_eval893#print axioms gval_readoutOf894#print axioms legalC_eval895#print axioms gval_legal896#print axioms gval_illegal897#print axioms gbitC_eval898#print axioms gval_lt899#print axioms HC_eval900#print axioms getD_take_drop901#print axioms decodeBoard_getD902#print axioms boardBits_decode903#print axioms depth_and_le904#print axioms depth_or_le905#print axioms sum_le_len_mul906#print axioms upow_pos907#print axioms size_and_le908#print axioms size_or_le909#print axioms size_lift910#print axioms size_not_le911#print axioms Upar_ge912#print axioms getC_size913#print axioms getC_depth914#print axioms getC_max915#print axioms HC_depth916#print axioms HC_size917#print axioms HC_max918#print axioms corrHyp_of_premise919#print axioms circuit_readout_bound920921end CorrBridge922end NimAudit