BitBridge

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 Circuit23/- Phase 3, target D (generic part).  Written by Claude (10 October 2026).4   Lean 4.26.0, core/Std only.56   * Bit vectors, big-endian heap encoding, and transfer of uniform sums from7     boards (N heaps < 2^B) to bit vectors of length B·N (heap-major).8   * <u, sigma(P)> equals the parity of the input bits selected by the mask9     consisting of N copies of u's bits; the mask has N·|u| ≥ N ones for u ≠ 0.10   * Restriction: fixing the coordinates outside a mask is a leaf substitution,11     so circuit size and depth are unchanged and the restricted circuit reads only12     the mask coordinates; averaging over the fixed coordinates turns a premise on13     full-parity correlation into a bound on masked-parity correlation.14   The classical AC0 parity-correlation theorem is NOT proved: it enters only as15   the explicit hypothesis `ParityCorrPremise`. -/1617namespace NimAudit18namespace Bridge1920open Prob AC0 AC0.Circ Game2122attribute [local simp] Rat.add_zero Rat.zero_add Rat.zero_mul Rat.mul_zero Rat.one_mul23  Rat.mul_one Rat.neg_mul Rat.mul_neg2425/-! ## Bit vectors -/2627def bitvecs : Nat → List (List Bool)28  | 0 => [[]]29  | n + 1 => (bitvecs n).map (false :: ·) ++ (bitvecs n).map (true :: ·)3031theorem mem_bitvecs_length {n : Nat} {x : List Bool} (h : x ∈ bitvecs n) : x.length = n := by32  induction n generalizing x with33  | zero => simp [bitvecs] at h; subst h; rfl34  | succ n ih =>35    simp only [bitvecs, List.mem_append, List.mem_map] at h36    rcases h with ⟨v, hv, rfl⟩ | ⟨v, hv, rfl⟩ <;> simp [ih hv]3738theorem rsum_bitvecs_succ (n : Nat) (f : List Bool → Rat) :39    rsum (bitvecs (n + 1)) f =40      rsum (bitvecs n) (fun v => f (false :: v)) + rsum (bitvecs n) (fun v => f (true :: v)) := by41  simp only [bitvecs, rsum_append, rsum_map]4243theorem rsum_bitvecs_add (m n : Nat) (f : List Bool → Rat) :44    rsum (bitvecs (m + n)) f =45      rsum (bitvecs m) (fun v => rsum (bitvecs n) (fun w => f (v ++ w))) := by46  induction m generalizing f with47  | zero => simp [bitvecs]48  | succ m ih =>49    rw [show m + 1 + n = (m + n) + 1 by omega, rsum_bitvecs_succ, rsum_bitvecs_succ, ih, ih]50    rfl5152theorem count_bitvecs (n : Nat) : rsum (bitvecs n) (fun _ => 1) = (2 : Rat) ^ n := by53  induction n with54  | zero => simp [bitvecs]55  | succ n ih => rw [rsum_bitvecs_succ, ih, Rat.pow_succ]; grind5657/-- Big-endian value of a bit list. -/58def toNatBE : List Bool → Nat59  | [] => 060  | b :: v => (if b then 2 ^ v.length else 0) + toNatBE v6162theorem toNatBE_lt (v : List Bool) : toNatBE v < 2 ^ v.length := by63  induction v with64  | nil => simp [toNatBE]65  | cons b v ih =>66    simp only [toNatBE, List.length_cons, Nat.pow_succ]67    split <;> omega6869theorem rsum_range_bitvecs (B : Nat) (g : Nat → Rat) :70    rsum (List.range (2 ^ B)) g = rsum (bitvecs B) (fun v => g (toNatBE v)) := by71  induction B generalizing g with72  | zero => simp [bitvecs, toNatBE]73  | succ B ih =>74    rw [show 2 ^ (B + 1) = 2 ^ B + 2 ^ B by rw [Nat.pow_succ]; omega, List.range_add,75      rsum_append, rsum_map, ih, ih, rsum_bitvecs_succ]76    congr 177    · apply rsum_congr; intro v _; simp [toNatBE]78    · apply rsum_congr; intro v hv; simp [toNatBE, mem_bitvecs_length hv]7980/-- (toNatBE v).testBit (|v| - 1 - p) = v_p for p < |v|. -/81theorem testBit_toNatBE (v : List Bool) (p : Nat) (hp : p < v.length) :82    (toNatBE v).testBit (v.length - 1 - p) = v.getD p false := by83  induction v generalizing p with84  | nil => simp at hp85  | cons b v ih =>86    simp only [toNatBE, List.length_cons]87    have hlt := toNatBE_lt v88    cases p with89    | zero =>90      simp only [Nat.add_sub_cancel, Nat.sub_zero, List.getD_cons_zero]91      cases b92      · simp; exact Nat.testBit_lt_two_pow hlt93      · simp only [if_true]; rw [Nat.testBit_two_pow_add_eq, Nat.testBit_lt_two_pow hlt]; rfl94    | succ p =>95      simp only [List.getD_cons_succ]96      have hp' : p < v.length := by simp at hp; omega97      have e : v.length + 1 - 1 - (p + 1) = v.length - 1 - p := by omega98      rw [e]99      cases b100      · simp; exact ih p hp'101      · simp only [if_true]102        rw [Nat.testBit_two_pow_add_gt (by omega)]103        exact ih p hp'104105/-! ## Boards as bit vectors -/106107/-- Decode a heap-major big-endian bit vector into N heaps. -/108def decodeBoard (B : Nat) : Nat → List Bool → List Nat109  | 0, _ => []110  | N + 1, x => toNatBE (x.take B) :: decodeBoard B N (x.drop B)111112theorem rsum_boards_bitvecs (B N : Nat) (f : List Nat → Rat) :113    rsum (boards (2 ^ B) N) f = rsum (bitvecs (B * N)) (fun x => f (decodeBoard B N x)) := by114  induction N generalizing f with115  | zero => simp [boards, bitvecs, decodeBoard]116  | succ N ih =>117    rw [rsum_boards_succ, rsum_range_bitvecs, show B * (N + 1) = B + B * N by118      rw [Nat.mul_succ, Nat.add_comm], rsum_bitvecs_add]119    apply rsum_congr; intro v hv120    rw [ih]121    apply rsum_congr; intro w _122    have hl := mem_bitvecs_length hv123    simp only [decodeBoard]124    rw [List.take_left' hl, List.drop_left' hl]125126theorem length_decodeBoard (B N : Nat) (x : List Bool) : (decodeBoard B N x).length = N := by127  induction N generalizing x with128  | zero => rfl129  | succ N ih => simp [decodeBoard, ih]130131theorem decodeBoard_width {B N : Nat} {x : List Bool} (hx : x ∈ bitvecs (B * N)) :132    Width B (decodeBoard B N x) := by133  induction N generalizing x with134  | zero => intro y hy; simp [decodeBoard] at hy135  | succ N ih =>136    intro y hy137    simp only [decodeBoard, List.mem_cons] at hy138    have hl := mem_bitvecs_length hx139    rcases hy with rfl | hy140    · have := toNatBE_lt (x.take B)141      have hB : B ≤ x.length := by rw [hl, Nat.mul_succ]; omega142      rw [List.length_take, Nat.min_eq_left hB] at this143      exact this144    · -- x.drop B ∈ bitvecs (B * N): rebuild via the length characterisation145      have hmem : x.drop B ∈ bitvecs (B * N) := by146        have key : ∀ n (z : List Bool), z.length = n → z ∈ bitvecs n := by147          intro n148          induction n with149          | zero => intro z hz; rw [List.length_eq_zero_iff] at hz; subst hz; simp [bitvecs]150          | succ n ihn =>151            intro z hz152            cases z with153            | nil => simp at hz154            | cons b z =>155              simp only [bitvecs, List.mem_append, List.mem_map]156              cases b157              · exact Or.inl ⟨z, ihn z (by simpa using hz), rfl⟩158              · exact Or.inr ⟨z, ihn z (by simpa using hz), rfl⟩159        apply key160        rw [List.length_drop, hl, Nat.mul_succ]; omega161      exact ih hmem y hy162163theorem mem_bitvecs_of_length {n : Nat} {z : List Bool} (hz : z.length = n) : z ∈ bitvecs n := by164  induction n generalizing z with165  | zero => rw [List.length_eq_zero_iff] at hz; subst hz; simp [bitvecs]166  | succ n ihn =>167    cases z with168    | nil => simp at hz169    | cons b z =>170      simp only [bitvecs, List.mem_append, List.mem_map]171      cases b172      · exact Or.inl ⟨z, ihn (by simpa using hz), rfl⟩173      · exact Or.inr ⟨z, ihn (by simpa using hz), rfl⟩174175/-! ## Masked parity and <u, sigma> -/176177/-- Big-endian B-bit expansion. -/178def toBitsBE : Nat → Nat → List Bool179  | 0, _ => []180  | B + 1, h => h.testBit B :: toBitsBE B h181182theorem length_toBitsBE (B h : Nat) : (toBitsBE B h).length = B := by183  induction B with184  | zero => rfl185  | succ B ih => simp [toBitsBE, ih]186187/-- Parity of the coordinates of x selected by the mask. -/188def pm : List Bool → List Bool → Bool189  | [], _ => false190  | _ :: _, [] => false191  | m :: ms, b :: bs => xor (m && b) (pm ms bs)192193theorem pm_append {ms1 ms2 v w : List Bool} (h : ms1.length = v.length) :194    pm (ms1 ++ ms2) (v ++ w) = xor (pm ms1 v) (pm ms2 w) := by195  induction ms1 generalizing v with196  | nil => cases v with197    | nil => simp [pm]198    | cons _ _ => simp at h199  | cons m ms ih =>200    cases v with201    | nil => simp at h202    | cons b v =>203      simp only [List.cons_append, pm]204      rw [ih (by simpa using h)]205      cases (m && b) <;> cases pm ms v <;> cases pm ms2 w <;> rfl206207/-- Mask for the character chi_u on N heaps: N copies of u's B bits. -/208def maskU (B : Nat) : Nat → Nat → List Bool209  | 0, _ => []210  | N + 1, u => toBitsBE B u ++ maskU B N u211212theorem length_maskU (B N u : Nat) : (maskU B N u).length = B * N := by213  induction N with214  | zero => rfl215  | succ N ih => simp [maskU, length_toBitsBE, ih, Nat.mul_succ, Nat.add_comm]216217theorem dotB_zero_right (B u : Nat) : dotB B u 0 = false := by218  induction B with219  | zero => rfl220  | succ B ih => simp [dotB, ih]221222theorem length_bitvecs (n : Nat) : (bitvecs n).length = 2 ^ n := by223  induction n with224  | zero => rfl225  | succ n ih => simp [bitvecs, ih, Nat.pow_succ]; omega226227theorem dotB_congr_right {B v v' : Nat} (u : Nat) (h : ∀ k < B, v.testBit k = v'.testBit k) :228    dotB B u v = dotB B u v' := by229  induction B with230  | zero => rfl231  | succ B ih =>232    simp only [dotB]233    rw [ih (fun k hk => h k (by omega)), h B (by omega)]234235/-- <u, value of a big-endian block> = masked parity of the block. -/236theorem dot_toNatBE (u : Nat) : ∀ (v : List Bool),237    dotB v.length u (toNatBE v) = pm (toBitsBE v.length u) v238  | [] => rfl239  | b :: v => by240    simp only [List.length_cons, dotB, toBitsBE, pm, toNatBE]241    have hlt := toNatBE_lt v242    have hcong : dotB v.length u ((if b then 2 ^ v.length else 0) + toNatBE v) =243        dotB v.length u (toNatBE v) := by244      apply dotB_congr_right245      intro k hk246      cases b247      · simp248      · simp only [if_true]; exact Nat.testBit_two_pow_add_gt hk _249    have htop : ((if b then 2 ^ v.length else 0) + toNatBE v).testBit v.length = b := by250      cases b251      · simp; exact Nat.testBit_lt_two_pow hlt252      · simp only [if_true]; rw [Nat.testBit_two_pow_add_eq, Nat.testBit_lt_two_pow hlt]; rfl253    rw [hcong, htop, dot_toNatBE u v]254    cases (u.testBit v.length && b) <;> cases pm (toBitsBE v.length u) v <;> rfl255256/-- PARITY IDENTITY: on encoded boards, <u, sigma(P)> is the masked parity of the257    input bits. -/258theorem chi_parity (B N u : Nat) {x : List Bool} (hx : x ∈ bitvecs (B * N)) :259    dotB B u (nimSum (decodeBoard B N x)) = pm (maskU B N u) x := by260  induction N generalizing x with261  | zero => simp [decodeBoard, nimSum, maskU, pm, dotB_zero_right]262  | succ N ih =>263    have hl := mem_bitvecs_length hx264    have hdrop : x.drop B ∈ bitvecs (B * N) := mem_bitvecs_of_length (by265      rw [List.length_drop, hl, Nat.mul_succ]; omega)266    have htake : (x.take B).length = B := by rw [List.length_take]; rw [hl, Nat.mul_succ]; omega267    simp only [decodeBoard, nimSum, maskU]268    rw [dotB_xor_right, ih hdrop]269    conv => rhs; rw [← List.take_append_drop B x]270    rw [pm_append (by rw [length_toBitsBE, htake])]271    have := dot_toNatBE u (x.take B)272    rw [htake] at this273    rw [this]274275/-- Number of ones in a bit list. -/276def ones (l : List Bool) : Nat := (l.filter id).length277278theorem ones_append (l m : List Bool) : ones (l ++ m) = ones l + ones m := by279  simp [ones, List.filter_append]280281theorem true_mem_toBitsBE {B u i : Nat} (hi : i < B) (hb : u.testBit i = true) :282    true ∈ toBitsBE B u := by283  induction B with284  | zero => omega285  | succ B ih =>286    simp only [toBitsBE, List.mem_cons]287    by_cases h : i = B288    · subst h; left; exact hb.symm289    · right; exact ih (by omega)290291theorem ones_pos_of_mem {l : List Bool} (h : true ∈ l) : 1 ≤ ones l := by292  unfold ones293  exact List.length_pos_of_mem (a := true) (by simp [List.mem_filter, h])294295theorem ones_toBitsBE_pos {B u : Nat} (hu0 : u ≠ 0) (hu : u < 2 ^ B) : 1 ≤ ones (toBitsBE B u) := by296  obtain ⟨i, hi⟩ := Nat.exists_testBit_of_ne_zero hu0297  have hiB : i < B := by298    rcases Nat.lt_or_ge i B with h | h299    · exact h300    · exfalso301      rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hu (Nat.pow_le_pow_right (by decide) h))] at hi302      cases hi303  exact ones_pos_of_mem (true_mem_toBitsBE hiB hi)304305theorem ones_le_length (l : List Bool) : ones l ≤ l.length := List.length_filter_le _ _306307theorem ones_maskU (B N u : Nat) : ones (maskU B N u) = N * ones (toBitsBE B u) := by308  induction N with309  | zero => simp [maskU, ones]310  | succ N ih => simp [maskU, ones_append, ih, Nat.succ_mul, Nat.add_comm]311312/-! ## Restriction to the mask coordinates -/313314/-- Number of zeros. -/315def zeros (l : List Bool) : Nat := (l.filter (fun b => !b)).length316317theorem ones_add_zeros (l : List Bool) : ones l + zeros l = l.length := by318  induction l with319  | nil => rfl320  | cons b l ih => cases b <;> simp [ones, zeros, List.filter_cons] at * <;> omega321322/-- Interleave y (mask coordinates) and ρ (other coordinates) according to the mask. -/323def merge : List Bool → List Bool → List Bool → List Bool324  | [], _, _ => []325  | true :: ms, ys, rs => ys.headD false :: merge ms ys.tail rs326  | false :: ms, ys, rs => rs.headD false :: merge ms ys rs.tail327328/-- SPLITTING THE UNIFORM SUM over the mask / non-mask coordinates. -/329theorem rsum_bitvecs_merge : ∀ (mask : List Bool) (f : List Bool → Rat),330    rsum (bitvecs mask.length) f =331      rsum (bitvecs (zeros mask)) (fun ρ => rsum (bitvecs (ones mask)) (fun y => f (merge mask y ρ)))332  | [], f => by simp [bitvecs, merge, zeros, ones]333  | true :: ms, f => by334    have hz : zeros (true :: ms) = zeros ms := by simp [zeros]335    have ho : ones (true :: ms) = ones ms + 1 := by simp [ones]336    rw [hz, ho, List.length_cons, rsum_bitvecs_succ, rsum_bitvecs_merge ms, rsum_bitvecs_merge ms,337      ← rsum_add]338    apply rsum_congr; intro ρ _339    rw [rsum_bitvecs_succ]340    simp [merge]341  | false :: ms, f => by342    have hz : zeros (false :: ms) = zeros ms + 1 := by simp [zeros]343    have ho : ones (false :: ms) = ones ms := by simp [ones]344    rw [hz, ho, List.length_cons, rsum_bitvecs_succ, rsum_bitvecs_succ,345      rsum_bitvecs_merge ms, rsum_bitvecs_merge ms]346    simp [merge]347348/-- Parity of all bits. -/349def par : List Bool → Bool350  | [] => false351  | b :: bs => xor b (par bs)352353theorem pm_merge : ∀ (mask y ρ : List Bool), y.length = ones mask →354    pm mask (merge mask y ρ) = par y355  | [], y, _, hy => by356    simp [ones] at hy; subst hy; rfl357  | true :: ms, y, ρ, hy => by358    cases y with359    | nil => simp [ones] at hy360    | cons b y =>361      simp only [merge, List.headD_cons, List.tail_cons, pm, Bool.true_and, par]362      rw [pm_merge ms y ρ (by simpa [ones] using hy)]363  | false :: ms, y, ρ, hy => by364    simp only [merge, pm, Bool.false_and, Bool.false_xor]365    exact pm_merge ms y ρ.tail (by simpa [ones] using hy)366367theorem length_merge : ∀ (mask y ρ : List Bool), (merge mask y ρ).length = mask.length368  | [], _, _ => rfl369  | true :: ms, y, ρ => by simp [merge, length_merge ms]370  | false :: ms, y, ρ => by simp [merge, length_merge ms]371372/-- Rank of position j among the ones (resp. zeros) of the mask. -/373def rankT (mask : List Bool) (j : Nat) : Nat := ones (mask.take j)374def rankF (mask : List Bool) (j : Nat) : Nat := zeros (mask.take j)375376theorem merge_getD : ∀ (mask y ρ : List Bool) (j : Nat), j < mask.length →377    (merge mask y ρ).getD j false =378      if mask.getD j false then y.getD (rankT mask j) false else ρ.getD (rankF mask j) false379  | [], _, _, j, hj => by simp at hj380  | true :: ms, y, ρ, 0, _ => by381    cases y <;> simp [merge, rankT, ones]382  | true :: ms, y, ρ, j + 1, hj => by383    simp only [merge, List.getD_cons_succ, List.getD_cons_succ]384    rw [merge_getD ms y.tail ρ j (by simpa using hj)]385    simp only [rankT, rankF, List.take_succ_cons, ones, zeros, List.filter_cons, id,386      if_true, Bool.not_true, Bool.false_eq_true, if_false, List.length_cons]387    cases y <;> cases ms.getD j false <;> simp388  | false :: ms, y, ρ, 0, _ => by389    cases ρ <;> simp [merge, rankF, zeros]390  | false :: ms, y, ρ, j + 1, hj => by391    simp only [merge, List.getD_cons_succ]392    rw [merge_getD ms y ρ.tail j (by simpa using hj)]393    simp only [rankT, rankF, List.take_succ_cons, ones, zeros, List.filter_cons, id,394      Bool.false_eq_true, if_false, Bool.not_false, if_true, List.length_cons]395    cases ρ <;> cases ms.getD j false <;> simp396397theorem rankT_lt : ∀ (mask : List Bool) (j : Nat), mask.getD j false = true →398    rankT mask j < ones mask399  | [], j, h => by simp at h400  | true :: ms, 0, _ => by simp [rankT, ones]401  | false :: ms, 0, h => by simp at h402  | b :: ms, j + 1, h => by403    have := rankT_lt ms j (by simpa using h)404    simp only [rankT, ones, List.take_succ_cons, List.filter_cons] at this ⊢405    cases b <;> simp <;> omega406407/-- Bit vector as an input assignment. -/408def vfun (x : List Bool) : Nat → Bool := fun j => x.getD j false409410/-- The circuit with non-mask coordinates fixed to ρ and mask coordinates renamed411    to 0, 1, ..., ones mask - 1. -/412def restrictC (mask ρ : List Bool) (C : Circ) : Circ :=413  subst (fun j => if mask.getD j false then input (rankT mask j)414    else const (ρ.getD (rankF mask j) false)) C415416theorem restrict_leaf (mask ρ : List Bool) (j : Nat) :417    IsLeaf (if mask.getD j false then input (rankT mask j)418      else const (ρ.getD (rankF mask j) false)) := by419  split <;> simp [IsLeaf]420421/-- RESTRICTION PRESERVES SIZE AND DEPTH, and the result reads only the mask422    coordinates. -/423theorem restrictC_resources (mask ρ : List Bool) (C : Circ) :424    size (restrictC mask ρ C) = size C ∧ depth (restrictC mask ρ C) = depth C ∧425    maxInput (restrictC mask ρ C) ≤ ones mask := by426  refine ⟨size_subst_leaf _ (restrict_leaf mask ρ) C, depth_subst_leaf _ (restrict_leaf mask ρ) C, ?_⟩427  apply maxInput_subst_le428  intro j429  by_cases h : mask.getD j false = true430  · simp only [h, if_true, maxInput_input]; have := rankT_lt mask j h; omega431  · rw [if_neg h]; simp432433theorem eval_restrictC {mask y ρ : List Bool} {C : Circ} (hC : maxInput C ≤ mask.length) :434    eval (vfun y) (restrictC mask ρ C) = eval (vfun (merge mask y ρ)) C := by435  unfold restrictC436  rw [eval_subst]437  apply eval_congr_below438  intro j hj439  have hjm : j < mask.length := Nat.lt_of_lt_of_le hj hC440  unfold vfun441  rw [merge_getD mask y ρ j hjm]442  split <;> simp443444/-! ## The conditional bridge -/445446def ind (b : Bool) : Rat := if b then 1 else 0447def sgn (b : Bool) : Rat := if b then -1 else 1448449/-- THE CLASSICAL PARITY-CORRELATION PREMISE (explicit hypothesis, not proved):450    every formula of depth ≤ d and size ≤ s reading only m inputs has correlation451    at most ε with parity of those m bits under the uniform distribution. -/452def ParityCorrPremise (d s m : Nat) (ε : Rat) : Prop :=453  ∀ C : Circ, depth C ≤ d → size C ≤ s → maxInput C ≤ m →454    -ε ≤ rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) / (2 : Rat) ^ m ∧455    rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) / (2 : Rat) ^ m ≤ ε456457theorem two_pow_pos' (n : Nat) : (0 : Rat) < (2 : Rat) ^ n := by458  have : ((2 ^ n : Nat) : Rat) = (2 : Rat) ^ n := by simp459  rw [← this]; exact Rat.natCast_pos.mpr (Nat.two_pow_pos n)460461/-- RESTRICTION/AVERAGING BRIDGE: under the premise at m = ones mask, the462    correlation of any circuit (depth ≤ d, size ≤ s, reading only the |mask|463    coordinates) with the MASKED parity is at most ε. -/464theorem masked_correlation (mask : List Bool) (C : Circ) {d s : Nat} {ε : Rat}465    (hC : maxInput C ≤ mask.length) (hd : depth C ≤ d) (hs : size C ≤ s)466    (hprem : ParityCorrPremise d s (ones mask) ε) :467    -ε ≤ rsum (bitvecs mask.length) (fun x => ind (eval (vfun x) C) * sgn (pm mask x)) /468        (2 : Rat) ^ mask.length ∧469    rsum (bitvecs mask.length) (fun x => ind (eval (vfun x) C) * sgn (pm mask x)) /470        (2 : Rat) ^ mask.length ≤ ε := by471  rw [rsum_bitvecs_merge]472  have inner : ∀ ρ ∈ bitvecs (zeros mask),473      rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun (merge mask y ρ)) C) *474        sgn (pm mask (merge mask y ρ))) =475      rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) := by476    intro ρ _477    apply rsum_congr; intro y hy478    rw [eval_restrictC hC, pm_merge mask y ρ (mem_bitvecs_length hy)]479  rw [rsum_congr inner]480  have hres := fun ρ => restrictC_resources mask ρ C481  have hT := two_pow_pos' (ones mask)482  have hb : ∀ ρ ∈ bitvecs (zeros mask),483      -(ε * (2 : Rat) ^ ones mask) ≤484        rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) ∧485      rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) ≤486        ε * (2 : Rat) ^ ones mask := by487    intro ρ _488    obtain ⟨k1, k2⟩ := hprem (restrictC mask ρ C) (by rw [(hres ρ).2.1]; exact hd)489      (by rw [(hres ρ).1]; exact hs) (hres ρ).2.2490    generalize rsum (bitvecs (ones mask))491      (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) = X at k1 k2 ⊢492    have hT' : (2 : Rat) ^ ones mask ≠ 0 := Rat.ne_of_gt hT493    have e : X / (2 : Rat) ^ ones mask * (2 : Rat) ^ ones mask = X := by grind494    have m1 := Rat.mul_le_mul_of_nonneg_right k1 (Rat.le_of_lt hT)495    have m2 := Rat.mul_le_mul_of_nonneg_right k2 (Rat.le_of_lt hT)496    rw [e] at m1 m2497    constructor <;> grind498  obtain ⟨b1, b2⟩ := rsum_bound hb499  rw [length_bitvecs] at b1 b2500  have hsplit : (2 : Rat) ^ mask.length = (2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask := by501    have h := ones_add_zeros mask502    have e : ∀ n : Nat, (2 : Rat) ^ n = ((2 ^ n : Nat) : Rat) := by intro n; simp503    rw [e, e, e, ← Rat.natCast_mul, ← Nat.pow_add, ← h, Nat.add_comm]504  have hN := two_pow_pos' mask.length505  have hN' : (2 : Rat) ^ mask.length ≠ 0 := Rat.ne_of_gt hN506  generalize rsum (bitvecs (zeros mask)) (fun ρ => rsum (bitvecs (ones mask))507    (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y))) = S at b1 b2 ⊢508  have c1 : (((2 ^ zeros mask : Nat) : Rat)) = (2 : Rat) ^ zeros mask := by simp509  rw [c1] at b1 b2510  rw [hsplit] at hN' ⊢511  have hZ := two_pow_pos' (zeros mask)512  constructor513  · apply Rat.le_of_mul_le_mul_right _ (Rat.mul_pos hZ hT)514    have e : S / ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) *515        ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) = S := by grind516    rw [e]; grind517  · apply Rat.le_of_mul_le_mul_right _ (Rat.mul_pos hZ hT)518    have e : S / ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) *519        ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) = S := by grind520    rw [e]; grind521522#print axioms mem_bitvecs_length523#print axioms rsum_bitvecs_succ524#print axioms rsum_bitvecs_add525#print axioms count_bitvecs526#print axioms toNatBE_lt527#print axioms rsum_range_bitvecs528#print axioms testBit_toNatBE529#print axioms rsum_boards_bitvecs530#print axioms length_decodeBoard531#print axioms decodeBoard_width532#print axioms mem_bitvecs_of_length533#print axioms length_toBitsBE534#print axioms pm_append535#print axioms length_maskU536#print axioms dotB_zero_right537#print axioms length_bitvecs538#print axioms dotB_congr_right539#print axioms dot_toNatBE540#print axioms chi_parity541#print axioms ones_append542#print axioms true_mem_toBitsBE543#print axioms ones_pos_of_mem544#print axioms ones_toBitsBE_pos545#print axioms ones_le_length546#print axioms ones_maskU547#print axioms ones_add_zeros548#print axioms rsum_bitvecs_merge549#print axioms pm_merge550#print axioms length_merge551#print axioms merge_getD552#print axioms rankT_lt553#print axioms restrict_leaf554#print axioms restrictC_resources555#print axioms eval_restrictC556#print axioms two_pow_pos'557#print axioms masked_correlation558559end Bridge560end NimAudit