Foundation

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 4, CLASSICAL FOUNDATION (separate, quantitative track).  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   Target.  `Bridge.ParityCorrPremise d s m ε` (every depth-d, size-s formula on m7   inputs has correlation at most ε with parity) remains an explicit HYPOTHESIS of8   every application.  This file proves the finite, probabilistic ENDGAME of the9   random-restriction route and isolates exactly what is left:1011   (1) decision trees of depth < m have correlation exactly 0 with parity of m bits12       (`dtree_corr_zero`, via a flip-pairing argument);13   (2) for a fixed star set (mask), the correlation of a formula is at most the14       fraction of fixings ρ for which the restricted formula is NOT certified to be15       a decision tree of depth < #stars (`mask_bound`);16   (3) FINITE PROBABILITY MODEL of p-random restrictions: mask weight17       p^#stars (1-p)^#fixed, ρ uniform; total weight 1 (`maskW_sum`);18   (4) RESTRICTION BOUND: |corr| ≤ Pr_{p-random ρ}[bad] for every p ∈ [0,1] and every19       certificate assignment (`restriction_bound`), hence20       `SwitchingBound d s m p ε → ParityCorrPremise d s m ε` (`premise_of_switching`).2122   REMAINING CLASSICAL CONTENT (not proved): `SwitchingBound`, i.e. a bound on the23   probability that a p-random restriction fails to collapse a depth-d, size-s formula24   to a decision tree of depth below the number of surviving variables.  This is what25   Håstad's switching lemma (iterated d−1 times, with a Chernoff bound on the number of26   stars) supplies.  No external proof is imported or claimed. -/2728namespace NimAudit29namespace Foundation3031open Prob AC0 AC0.Circ Bridge3233/-! ## Decision trees and their zero correlation with parity -/3435inductive DTree where36  | leaf (b : Bool)37  | node (i : Nat) (t0 t1 : DTree)3839namespace DTree4041def eval (x : Nat → Bool) : DTree → Bool42  | leaf b => b43  | node i t0 t1 => if x i then eval x t1 else eval x t04445def depth : DTree → Nat46  | leaf _ => 047  | node _ t0 t1 => max (depth t0) (depth t1) + 14849/-- Root-to-leaf paths (query, answer) with the leaf label. -/50def leaves : DTree → List (List (Nat × Bool) × Bool)51  | leaf b => [([], b)]52  | node i t0 t1 => (leaves t0).map (fun l => ((i, false) :: l.1, l.2)) ++53      (leaves t1).map (fun l => ((i, true) :: l.1, l.2))5455end DTree5657def sat (x : Nat → Bool) (π : List (Nat × Bool)) : Bool := π.all (fun c => x c.1 == c.2)5859theorem rsum_zero' {α : Type} (l : List α) (f : α → Rat) (h : ∀ a ∈ l, f a = 0) : rsum l f = 0 := by60  rw [rsum_congr h, rsum_zero]6162theorem ind_eval_leaves (x : Nat → Bool) : ∀ T : DTree,63    ind (T.eval x) = rsum T.leaves (fun l => ind (sat x l.1) * ind l.2)64  | .leaf b => by simp [DTree.eval, DTree.leaves, sat, ind, Rat.add_zero]65  | .node i t0 t1 => by66    simp only [DTree.eval, DTree.leaves, rsum_append, rsum_map]67    cases hx : x i68    · simp only [Bool.false_eq_true, if_false]69      rw [ind_eval_leaves x t0]70      have h1 : rsum t1.leaves (fun l => ind (sat x ((i, true) :: l.1)) * ind l.2) = 0 :=71        rsum_zero' _ _ (fun l _ => by simp [sat, hx, ind])72      rw [h1]73      have h2 : ∀ l ∈ t0.leaves, ind (sat x ((i, false) :: l.1)) * ind l.2 = ind (sat x l.1) * ind l.2 := by74        intro l _; simp [sat, hx]75      rw [rsum_congr h2]; grind76    · simp only [if_true]77      rw [ind_eval_leaves x t1]78      have h1 : rsum t0.leaves (fun l => ind (sat x ((i, false) :: l.1)) * ind l.2) = 0 :=79        rsum_zero' _ _ (fun l _ => by simp [sat, hx, ind])80      rw [h1]81      have h2 : ∀ l ∈ t1.leaves, ind (sat x ((i, true) :: l.1)) * ind l.2 = ind (sat x l.1) * ind l.2 := by82        intro l _; simp [sat, hx]83      rw [rsum_congr h2]; grind8485theorem leaves_length : ∀ (T : DTree), ∀ l ∈ T.leaves, l.1.length ≤ T.depth86  | .leaf b => by intro l hl; simp [DTree.leaves] at hl; subst hl; simp87  | .node i t0 t1 => by88    intro l hl89    simp only [DTree.leaves, List.mem_append, List.mem_map] at hl90    rcases hl with ⟨l', hl', rfl⟩ | ⟨l', hl', rfl⟩91    · have := leaves_length t0 l' hl'; simp [DTree.depth]; omega92    · have := leaves_length t1 l' hl'; simp [DTree.depth]; omega9394/-- Flip coordinate j. -/95def flipAt : Nat → List Bool → List Bool96  | _, [] => []97  | 0, b :: bs => (!b) :: bs98  | j + 1, b :: bs => b :: flipAt j bs99100theorem rsum_flip : ∀ (m j : Nat) (h : List Bool → Rat), j < m →101    rsum (bitvecs m) (fun y => h (flipAt j y)) = rsum (bitvecs m) h102  | 0, _, _, hj => absurd hj (Nat.not_lt_zero _)103  | m + 1, 0, h, _ => by104    rw [rsum_bitvecs_succ, rsum_bitvecs_succ]105    simp only [flipAt, Bool.not_false, Bool.not_true]106    grind107  | m + 1, j + 1, h, hj => by108    rw [rsum_bitvecs_succ, rsum_bitvecs_succ]109    simp only [flipAt]110    rw [rsum_flip m j (fun v => h (false :: v)) (by omega), rsum_flip m j (fun v => h (true :: v)) (by omega)]111112theorem par_flipAt : ∀ (j : Nat) (y : List Bool), j < y.length → par (flipAt j y) = !par y113  | _, [], h => by simp at h114  | 0, b :: bs, _ => by simp [flipAt, par]115  | j + 1, b :: bs, h => by116    simp only [flipAt, par]117    rw [par_flipAt j bs (by simpa using h)]118    cases b <;> cases par bs <;> rfl119120theorem vfun_flipAt : ∀ (j : Nat) (y : List Bool) (i : Nat), i ≠ j → vfun (flipAt j y) i = vfun y i121  | j, [], _, _ => by cases j <;> rfl122  | 0, b :: bs, i, hij => by123    cases i with124    | zero => exact absurd rfl hij125    | succ i => simp [flipAt, vfun]126  | j + 1, b :: bs, i, hij => by127    cases i with128    | zero => simp [flipAt, vfun]129    | succ i =>130      have := vfun_flipAt j bs i (by omega)131      simpa [flipAt, vfun] using this132133theorem sgn_not (b : Bool) : sgn (!b) = -sgn b := by cases b <;> decide134135/-- PAIRING: a weight invariant under flipping a coordinate j < m has zero correlation136    with parity of m bits. -/137theorem pairing (m j : Nat) (hj : j < m) (g : List Bool → Rat) (hg : ∀ y, g (flipAt j y) = g y) :138    rsum (bitvecs m) (fun y => g y * sgn (par y)) = 0 := by139  have h1 := rsum_flip m j (fun y => g y * sgn (par y)) hj140  have h2 : rsum (bitvecs m) (fun y => g (flipAt j y) * sgn (par (flipAt j y))) =141      (-1) * rsum (bitvecs m) (fun y => g y * sgn (par y)) := by142    rw [← rsum_mul_left]143    apply rsum_congr; intro y hy144    rw [hg, par_flipAt j y (by rw [mem_bitvecs_length hy]; exact hj), sgn_not]145    grind146  rw [h2] at h1147  grind148149theorem exists_not_mem : ∀ (m : Nat) (l : List Nat), l.length < m → ∃ j < m, j ∉ l150  | 0, _, h => absurd h (Nat.not_lt_zero _)151  | m + 1, l, h => by152    by_cases hm : m ∈ l153    · have hpos := List.length_pos_of_mem hm154      have hlen : (l.erase m).length < m := by rw [List.length_erase_of_mem hm]; omega155      obtain ⟨j, hj, hnot⟩ := exists_not_mem m (l.erase m) hlen156      refine ⟨j, by omega, fun hjl => hnot ?_⟩157      exact (List.mem_erase_of_ne (by omega)).mpr hjl158    · exact ⟨m, by omega, hm⟩159160theorem sat_congr {x x' : Nat → Bool} : ∀ (π : List (Nat × Bool)), (∀ c ∈ π, x c.1 = x' c.1) → sat x π = sat x' π161  | [], _ => rfl162  | c :: π, h => by163    simp only [sat, List.all_cons]164    rw [h c (by simp)]165    have := sat_congr π (fun c' hc' => h c' (by simp [hc']))166    simp only [sat] at this167    rw [this]168169/-- DECISION TREES ARE UNCORRELATED WITH PARITY: depth < m ⇒ correlation exactly 0. -/170theorem dtree_corr_zero (T : DTree) (m : Nat) (hT : T.depth < m) :171    rsum (bitvecs m) (fun y => ind (T.eval (vfun y)) * sgn (par y)) = 0 := by172  have e : ∀ y ∈ bitvecs m, ind (T.eval (vfun y)) * sgn (par y) =173      rsum T.leaves (fun l => (ind (sat (vfun y) l.1) * ind l.2) * sgn (par y)) := by174    intro y _175    rw [ind_eval_leaves]176    induction T.leaves with177    | nil => simp178    | cons a l ih => simp only [rsum_cons]; rw [← ih]; grind179  rw [rsum_congr e, rsum_comm]180  apply rsum_zero'181  intro l hl182  obtain ⟨j, hj, hnot⟩ := exists_not_mem m (l.1.map Prod.fst) (by183    rw [List.length_map]; exact Nat.lt_of_le_of_lt (leaves_length T l hl) hT)184  apply pairing m j hj (fun y => ind (sat (vfun y) l.1) * ind l.2)185  intro y186  rw [sat_congr l.1 (fun c hc => vfun_flipAt j y c.1 (by187    intro h; apply hnot; rw [← h]; exact List.mem_map_of_mem hc))]188189/-! ## Restrictions: the per-mask bound -/190191theorem par_merge : ∀ (mask y ρ : List Bool), y.length = ones mask → ρ.length = zeros mask →192    par (merge mask y ρ) = xor (par y) (par ρ)193  | [], y, ρ, hy, hρ => by194    simp [ones] at hy; simp [zeros] at hρ; subst hy; subst hρ; rfl195  | true :: ms, y, ρ, hy, hρ => by196    cases y with197    | nil => simp [ones] at hy198    | cons b y =>199      simp only [merge, List.headD_cons, List.tail_cons, par]200      rw [par_merge ms y ρ (by simpa [ones] using hy) (by simpa [zeros] using hρ)]201      cases b <;> cases par y <;> cases par ρ <;> rfl202  | false :: ms, y, ρ, hy, hρ => by203    cases ρ with204    | nil => simp [zeros] at hρ205    | cons r ρ =>206      simp only [merge, List.headD_cons, List.tail_cons, par]207      rw [par_merge ms y ρ (by simpa [ones] using hy) (by simpa [zeros] using hρ)]208      cases r <;> cases par y <;> cases par ρ <;> rfl209210theorem sgn_xor (a b : Bool) : sgn (xor a b) = sgn a * sgn b := by cases a <;> cases b <;> simp [sgn] <;> grind211212/-- A certified shallow decision tree for the restricted formula. -/213def agrees (k : Nat) (T : DTree) (C : Circ) : Bool :=214  decide (T.depth < k) && (bitvecs k).all (fun y => T.eval (vfun y) == eval (vfun y) C)215216/-- The bad event for a certificate assignment τ: no certified tree of depth < #stars. -/217def badR (C : Circ) (τ : List Bool → List Bool → Option DTree) (mask ρ : List Bool) : Bool :=218  match τ mask ρ with219  | some T => !(agrees (ones mask) T (restrictC mask ρ C))220  | none => true221222theorem inner_good {C : Circ} {k : Nat} {T : DTree} (h : agrees k T C = true) :223    rsum (bitvecs k) (fun y => ind (eval (vfun y) C) * sgn (par y)) = 0 := by224  simp only [agrees, Bool.and_eq_true, decide_eq_true_iff, List.all_eq_true, beq_iff_eq] at h225  rw [← dtree_corr_zero T k h.1]226  apply rsum_congr; intro y hy; rw [h.2 y hy]227228theorem ind_bounds (b : Bool) (s : Bool) : -1 ≤ ind b * sgn s ∧ ind b * sgn s ≤ 1 := by229  cases b <;> cases s <;> simp [ind, sgn] <;> decide230231/-- PER-MASK BOUND (unnormalised): |Σ_x ind(C x)·(−1)^{par x}| ≤ #bad · 2^#stars. -/232theorem mask_bound (mask : List Bool) (C : Circ) (hC : maxInput C ≤ mask.length)233    (τ : List Bool → List Bool → Option DTree) :234    -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) * (2 : Rat) ^ ones mask) ≤235      rsum (bitvecs mask.length) (fun x => ind (eval (vfun x) C) * sgn (par x)) ∧236    rsum (bitvecs mask.length) (fun x => ind (eval (vfun x) C) * sgn (par x)) ≤237      rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) * (2 : Rat) ^ ones mask := by238  rw [rsum_bitvecs_merge]239  have hT := two_pow_pos' (ones mask)240  have hin : ∀ ρ ∈ bitvecs (zeros mask),241      rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun (merge mask y ρ)) C) * sgn (par (merge mask y ρ))) =242      sgn (par ρ) * rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) := by243    intro ρ hρ244    rw [← rsum_mul_left]245    apply rsum_congr; intro y hy246    rw [eval_restrictC hC, par_merge mask y ρ (mem_bitvecs_length hy) (mem_bitvecs_length hρ), sgn_xor]247    grind248  rw [rsum_congr hin]249  have hb : ∀ ρ ∈ bitvecs (zeros mask),250      -(ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask) ≤251        sgn (par ρ) * rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) ∧252      sgn (par ρ) * rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) ≤253        ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask := by254    intro ρ _255    cases hbad : badR C τ mask ρ256    · -- good: a certified tree exists257      have hgood : ∃ T, agrees (ones mask) T (restrictC mask ρ C) = true := by258        unfold badR at hbad259        cases hτ : τ mask ρ with260        | none => rw [hτ] at hbad; cases hbad261        | some T => rw [hτ] at hbad; exact ⟨T, by simpa using hbad⟩262      obtain ⟨T, hT'⟩ := hgood263      rw [inner_good hT']264      refine ⟨?_, ?_⟩ <;> simp [ind] <;> first | decide | rfl265    · obtain ⟨b1, b2⟩ := rsum_bound (l := bitvecs (ones mask))266        (f := fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) (e := 1)267        (fun y _ => ind_bounds _ _)268      rw [length_bitvecs] at b1 b2269      have c1 : (((2 ^ ones mask : Nat) : Rat)) = (2 : Rat) ^ ones mask := by simp270      rw [c1] at b1 b2271      generalize rsum (bitvecs (ones mask)) (fun y => ind (eval (vfun y) (restrictC mask ρ C)) * sgn (par y)) = X272        at b1 b2 ⊢273      generalize (2 : Rat) ^ ones mask = W at b1 b2 ⊢274      simp only [ind, if_true]275      cases par ρ276      · simp only [sgn, Bool.false_eq_true, if_false]; constructor <;> grind277      · simp only [sgn, if_true]; constructor <;> grind278  have hl : rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask) =279      rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) * (2 : Rat) ^ ones mask := by280    rw [show (fun ρ => ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask) =281      (fun ρ => (2 : Rat) ^ ones mask * ind (badR C τ mask ρ)) from by funext ρ; grind, rsum_mul_left]282    grind283  have hl' : rsum (bitvecs (zeros mask)) (fun ρ => -(ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask)) =284      -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) * (2 : Rat) ^ ones mask) := by285    rw [show (fun ρ => -(ind (badR C τ mask ρ) * (2 : Rat) ^ ones mask)) =286      (fun ρ => (-(2 : Rat) ^ ones mask) * ind (badR C τ mask ρ)) from by funext ρ; grind, rsum_mul_left]287    grind288  constructor289  · rw [← hl']; exact rsum_le (fun ρ hρ => (hb ρ hρ).1)290  · rw [← hl]; exact rsum_le (fun ρ hρ => (hb ρ hρ).2)291292/-! ## The finite probability model of p-random restrictions -/293294/-- Weight of a star set: p^#stars (1 − p)^#fixed. -/295def maskW (p : Rat) (mask : List Bool) : Rat := p ^ ones mask * (1 - p) ^ zeros mask296297theorem maskW_sum (p : Rat) : ∀ m, rsum (bitvecs m) (maskW p) = 1298  | 0 => by simp [bitvecs, maskW, ones, zeros, rsum, Rat.add_zero]299  | m + 1 => by300    rw [rsum_bitvecs_succ]301    have h0 : ∀ v, maskW p (false :: v) = (1 - p) * maskW p v := by302      intro v; simp only [maskW, ones, zeros, List.filter_cons, Bool.not_false, if_true, Bool.false_eq_true,303        if_false, List.length_cons, Rat.pow_succ]; grind304    have h1 : ∀ v, maskW p (true :: v) = p * maskW p v := by305      intro v; simp only [maskW, ones, zeros, List.filter_cons, Bool.not_true, if_true, Bool.false_eq_true,306        if_false, List.length_cons, Rat.pow_succ, id]; grind307    simp only [h0, h1, rsum_mul_left, maskW_sum p m]308    grind309310theorem pow_nonneg' {a : Rat} (ha : 0 ≤ a) : ∀ n : Nat, 0 ≤ a ^ n311  | 0 => by simp; decide312  | n + 1 => by rw [Rat.pow_succ]; exact Rat.mul_nonneg (pow_nonneg' ha n) ha313314theorem maskW_nonneg {p : Rat} (h0 : 0 ≤ p) (h1 : p ≤ 1) (mask : List Bool) : 0 ≤ maskW p mask :=315  Rat.mul_nonneg (pow_nonneg' h0 _) (pow_nonneg' (by grind) _)316317/-- Probability of an event E(mask, ρ) under the p-random restriction on m variables. -/318def restrProb (p : Rat) (m : Nat) (E : List Bool → List Bool → Bool) : Rat :=319  rsum (bitvecs m) (fun mask => maskW p mask *320    (rsum (bitvecs (zeros mask)) (fun ρ => ind (E mask ρ)) / (2 : Rat) ^ zeros mask))321322/-- Normalised correlation with parity of m bits. -/323def corr (m : Nat) (C : Circ) : Rat :=324  rsum (bitvecs m) (fun x => ind (eval (vfun x) C) * sgn (par x)) / (2 : Rat) ^ m325326theorem two_pow_split (mask : List Bool) :327    (2 : Rat) ^ mask.length = (2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask := by328  have h := ones_add_zeros mask329  have e : ∀ n : Nat, (2 : Rat) ^ n = ((2 ^ n : Nat) : Rat) := by intro n; simp330  rw [e, e, e, ← Rat.natCast_mul, ← Nat.pow_add, ← h, Nat.add_comm]331332/-- Normalised per-mask bound. -/333theorem mask_bound_norm (mask : List Bool) (C : Circ) (hC : maxInput C ≤ mask.length)334    (τ : List Bool → List Bool → Option DTree) :335    -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask) ≤336      corr mask.length C ∧337    corr mask.length C ≤ rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask := by338  obtain ⟨b1, b2⟩ := mask_bound mask C hC τ339  unfold corr340  rw [two_pow_split]341  have hT := two_pow_pos' (ones mask)342  have hZ := two_pow_pos' (zeros mask)343  generalize rsum (bitvecs mask.length) (fun x => ind (eval (vfun x) C) * sgn (par x)) = S at b1 b2 ⊢344  generalize rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) = K at b1 b2 ⊢345  have hT' : (2 : Rat) ^ ones mask ≠ 0 := Rat.ne_of_gt hT346  have hZ' : (2 : Rat) ^ zeros mask ≠ 0 := Rat.ne_of_gt hZ347  constructor348  · apply Rat.le_of_mul_le_mul_right _ (Rat.mul_pos hZ hT)349    have e1 : S / ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) *350        ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) = S := by grind351    have e2 : -(K / (2 : Rat) ^ zeros mask) * ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) =352        -(K * (2 : Rat) ^ ones mask) := by grind353    rw [e1, e2]; exact b1354  · apply Rat.le_of_mul_le_mul_right _ (Rat.mul_pos hZ hT)355    have e1 : S / ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) *356        ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) = S := by grind357    have e2 : K / (2 : Rat) ^ zeros mask * ((2 : Rat) ^ zeros mask * (2 : Rat) ^ ones mask) =358        K * (2 : Rat) ^ ones mask := by grind359    rw [e1, e2]; exact b2360361/-- RESTRICTION BOUND: for every p ∈ [0,1] and every certificate assignment τ, the362    correlation of C with parity of m bits is at most the probability, under the363    p-random restriction, that τ fails to certify a decision tree of depth below the364    number of surviving variables. -/365theorem restriction_bound {p : Rat} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (m : Nat) (C : Circ) (hC : maxInput C ≤ m)366    (τ : List Bool → List Bool → Option DTree) :367    -restrProb p m (badR C τ) ≤ corr m C ∧ corr m C ≤ restrProb p m (badR C τ) := by368  have hsum := maskW_sum p m369  have hc : corr m C = rsum (bitvecs m) (fun mask => maskW p mask * corr m C) := by370    rw [show (fun mask => maskW p mask * corr m C) = (fun mask => corr m C * maskW p mask) from by371      funext mask; grind, rsum_mul_left, hsum]; grind372  have hb : ∀ mask ∈ bitvecs m,373      maskW p mask * -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask) ≤374        maskW p mask * corr m C ∧375      maskW p mask * corr m C ≤376        maskW p mask * (rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask) := by377    intro mask hmask378    have hlen := mem_bitvecs_length hmask379    obtain ⟨k1, k2⟩ := mask_bound_norm mask C (by rw [hlen]; exact hC) τ380    rw [hlen] at k1 k2381    have hw := maskW_nonneg hp0 hp1 mask382    exact ⟨Rat.mul_le_mul_of_nonneg_left k1 hw, Rat.mul_le_mul_of_nonneg_left k2 hw⟩383  have hneg : rsum (bitvecs m) (fun mask => maskW p mask *384      -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask)) =385      -restrProb p m (badR C τ) := by386    unfold restrProb387    rw [show (fun mask => maskW p mask *388        -(rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask)) =389      (fun mask => (-1) * (maskW p mask *390        (rsum (bitvecs (zeros mask)) (fun ρ => ind (badR C τ mask ρ)) / (2 : Rat) ^ zeros mask))) from by391      funext mask; grind, rsum_mul_left]392    grind393  constructor394  · rw [hc, ← hneg]; exact rsum_le (fun mask h => (hb mask h).1)395  · rw [hc]; exact rsum_le (fun mask h => (hb mask h).2)396397/-! ## The remaining classical statement and the proved reduction -/398399/-- SWITCHING BOUND (the remaining classical content, NOT proved): for every formula of400    depth ≤ d and size ≤ s on m inputs there is a certificate assignment whose failure401    probability under the p-random restriction is at most ε. -/402def SwitchingBound (d s m : Nat) (p ε : Rat) : Prop :=403  ∀ C : Circ, depth C ≤ d → size C ≤ s → maxInput C ≤ m →404    ∃ τ : List Bool → List Bool → Option DTree, restrProb p m (badR C τ) ≤ ε405406/-- PROVED REDUCTION: a switching bound yields the parity-correlation premise. -/407theorem premise_of_switching {d s m : Nat} {p ε : Rat} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)408    (h : SwitchingBound d s m p ε) : ParityCorrPremise d s m ε := by409  intro C hd hs hm410  obtain ⟨τ, hτ⟩ := h C hd hs hm411  obtain ⟨b1, b2⟩ := restriction_bound hp0 hp1 m C hm τ412  unfold corr at b1 b2413  constructor414  · exact Rat.le_trans (by grind) b1415  · exact Rat.le_trans b2 hτ416417/-- Sanity check of the model: with p = 1 (no fixing) the bad event is "C itself has418    no certified tree of depth < m"; a decision-tree-certified formula has correlation 0. -/419theorem corr_zero_of_tree {m : Nat} {C : Circ} {T : DTree} (h : agrees m T C = true) : corr m C = 0 := by420  unfold corr; rw [inner_good h]; grind421422423/-! ## Axiom audit -/424425#print axioms rsum_zero'426#print axioms ind_eval_leaves427#print axioms leaves_length428#print axioms rsum_flip429#print axioms par_flipAt430#print axioms vfun_flipAt431#print axioms sgn_not432#print axioms pairing433#print axioms exists_not_mem434#print axioms sat_congr435#print axioms dtree_corr_zero436#print axioms par_merge437#print axioms sgn_xor438#print axioms inner_good439#print axioms ind_bounds440#print axioms mask_bound441#print axioms maskW_sum442#print axioms pow_nonneg'443#print axioms maskW_nonneg444#print axioms two_pow_split445#print axioms mask_bound_norm446#print axioms restriction_bound447#print axioms premise_of_switching448#print axioms corr_zero_of_tree449end Foundation450end NimAudit