Classical

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 Bypass23/- Phase 6, Priority 3a: the classical external boundary and its paper-specific4   consequences.  Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   EXTERNAL INPUT (a theorem PARAMETER, never an axiom), as authorised by Søren Riis:7   Håstad, "On the correlation of parity and small-depth circuits", SIAM J. Comput.8   43(5):1699–1708 (2014), Corollary 3.2 (DOI 10.1137/120897432): a depth-d circuit of9   size S agrees with parity on n inputs on a fraction (1 + c)/2 of inputs with10   |c| ≤ 2^{−Ω(n/(log S)^{d−1})} (exponent n/(log S)^{d−1}, not (n/log S)^{d−1}).  For11   fixed d and S polynomial in n this is negligible in n.  We take the negligible FAMILY12   form, quantified over ALL bounded-depth polynomial-size circuits, in the CLASSICAL13   convention, as the single external input `HastadNegl`.1415   CONVENTION ADAPTERS PROVED HERE.16   * Circuit conventions: classical depth counts AND/OR levels only (aoDepth), classical17     size counts AND/OR gates only (aoGates), negations sit on inputs (negLeaf).  Our18     formulas count NOT in depth and every node in size, so aoDepth ≤ depth and19     aoGates ≤ size; nnf pushes negations to the inputs preserving the function, aoDepth,20     aoGates and inputs.  The hypothesis is stated for FORMULAS (trees), which are special21     circuits: a formula with g AND/OR gates is a circuit with g gates, so the classical22     DAG theorem implies it (phase 4 SharedCircuit relates formulas and DAGs in our23     convention).  Trivial depths/sizes need no special case: the statement is monotone.24   * Correlation conventions: Håstad's signed correlation scorr = 2·Pr[C = PAR] − 1 versus25     our indicator correlation E[1_C · (−1)^PAR]; for m ≥ 1 inputs the latter equals26     −scorr/2 (indicator_signed), so |scorr| ≤ δ gives the indicator premise with δ/2.27     For m = 0 the parity is constant and the conventions do not agree (not used).28   CONSEQUENCES PROVED HERE.29   * HastadNegl ⇒ ParityNotAC0 (the worst-case premise of the single-frame barrier and of30     the bypass barriers).31   * The asymptotic Theorem thm:search-gap(i): for fixed B ≥ 2 and any binary readout32     family of fixed depth and polynomial size, success ≤ 2/(2^B − 1) + η_N with η33     negligible, including the uniformity over restriction supports N+1 ≤ m ≤ B(N+1). -/3435namespace NimAudit36namespace ClassicalBoundary3738open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit39  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame40  Family Barrier ParityCircuit4142/-! ## Classical circuit conventions -/4344/-- AND/OR depth: NOT nodes and leaves contribute nothing. -/45def aoDepth : Circ → Nat46  | .input _ => 047  | .const _ => 048  | .not c => aoDepth c49  | .and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => aoDepth c)) + 150  | .or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => aoDepth c)) + 15152/-- Number of AND/OR gates. -/53def aoGates : Circ → Nat54  | .input _ => 055  | .const _ => 056  | .not c => aoGates c57  | .and cs => (cs.attach.map (fun ⟨c, _⟩ => aoGates c)).sum + 158  | .or cs => (cs.attach.map (fun ⟨c, _⟩ => aoGates c)).sum + 15960/-- Negation normal form: NOT is applied only to inputs and constants. -/61def negLeaf : Circ → Bool62  | .input _ => true63  | .const _ => true64  | .not (.input _) => true65  | .not (.const _) => true66  | .not _ => false67  | .and cs => cs.attach.all (fun ⟨c, _⟩ => negLeaf c)68  | .or cs => cs.attach.all (fun ⟨c, _⟩ => negLeaf c)6970/-- Push negations to the leaves; p = true means "negate". -/71def nnf (p : Bool) : Circ → Circ72  | .input i => if p then .not (.input i) else .input i73  | .const b => .const (xor p b)74  | .not c => nnf (!p) c75  | .and cs => if p then .or (cs.attach.map (fun ⟨c, _⟩ => nnf p c)) else .and (cs.attach.map (fun ⟨c, _⟩ => nnf p c))76  | .or cs => if p then .and (cs.attach.map (fun ⟨c, _⟩ => nnf p c)) else .or (cs.attach.map (fun ⟨c, _⟩ => nnf p c))7778@[simp] theorem aoDepth_and (cs : List Circ) : aoDepth (.and cs) = listMax (cs.map aoDepth) + 1 := by simp [aoDepth]79@[simp] theorem aoDepth_or (cs : List Circ) : aoDepth (.or cs) = listMax (cs.map aoDepth) + 1 := by simp [aoDepth]80@[simp] theorem aoGates_and (cs : List Circ) : aoGates (.and cs) = (cs.map aoGates).sum + 1 := by simp [aoGates]81@[simp] theorem aoGates_or (cs : List Circ) : aoGates (.or cs) = (cs.map aoGates).sum + 1 := by simp [aoGates]82@[simp] theorem negLeaf_and (cs : List Circ) : negLeaf (.and cs) = cs.all negLeaf := by simp [negLeaf]83@[simp] theorem negLeaf_or (cs : List Circ) : negLeaf (.or cs) = cs.all negLeaf := by simp [negLeaf]84@[simp] theorem nnf_and (p : Bool) (cs : List Circ) :85    nnf p (.and cs) = if p then .or (cs.map (nnf p)) else .and (cs.map (nnf p)) := by simp [nnf]86@[simp] theorem nnf_or (p : Bool) (cs : List Circ) :87    nnf p (.or cs) = if p then .and (cs.map (nnf p)) else .or (cs.map (nnf p)) := by simp [nnf]8889theorem any_not_eq (l : List Circ) (f : Circ → Bool) : l.any (fun c => !f c) = !(l.all f) := by90  induction l with91  | nil => rfl92  | cons a l ih => simp [List.any_cons, List.all_cons, ih]9394theorem all_not_eq (l : List Circ) (f : Circ → Bool) : l.all (fun c => !f c) = !(l.any f) := by95  induction l with96  | nil => rfl97  | cons a l ih => simp [List.any_cons, List.all_cons, ih]9899/-- nnf computes the (possibly negated) function. -/100theorem eval_nnf (x : Nat → Bool) : ∀ (p : Bool) (c : Circ), eval x (nnf p c) = xor p (eval x c)101  | p, .input i => by cases p <;> simp [nnf]102  | p, .const b => by cases p <;> simp [nnf]103  | p, .not c => by simp only [nnf, eval_not, eval_nnf x (!p) c]; cases p <;> simp104  | p, .and cs => by105    rw [nnf_and]106    cases p107    · simp only [Bool.false_eq_true, if_false, eval_and, List.all_map, Bool.false_xor]108      exact all_congr_mem (fun c _ => by simp [eval_nnf x false c])109    · simp only [if_true, eval_or, eval_and, List.any_map, Bool.true_xor]110      rw [← any_not_eq]111      exact any_congr_mem (fun c _ => by simp [eval_nnf x true c])112  | p, .or cs => by113    rw [nnf_or]114    cases p115    · simp only [Bool.false_eq_true, if_false, eval_or, List.any_map, Bool.false_xor]116      exact any_congr_mem (fun c _ => by simp [eval_nnf x false c])117    · simp only [if_true, eval_and, eval_or, List.all_map, Bool.true_xor]118      rw [← all_not_eq]119      exact all_congr_mem (fun c _ => by simp [eval_nnf x true c])120121theorem negLeaf_nnf : ∀ (p : Bool) (c : Circ), negLeaf (nnf p c) = true122  | p, .input i => by cases p <;> simp [nnf, negLeaf]123  | p, .const b => by simp [nnf, negLeaf]124  | p, .not c => by simp only [nnf]; exact negLeaf_nnf (!p) c125  | p, .and cs => by126    rw [nnf_and]127    have h : ∀ c ∈ cs, negLeaf (nnf p c) = true := fun c _ => negLeaf_nnf p c128    cases p <;> simp [List.all_eq_true] <;> exact h129  | p, .or cs => by130    rw [nnf_or]131    have h : ∀ c ∈ cs, negLeaf (nnf p c) = true := fun c _ => negLeaf_nnf p c132    cases p <;> simp [List.all_eq_true] <;> exact h133134theorem listMax_map_congr {l : List Circ} {f g : Circ → Nat} (h : ∀ c ∈ l, f c = g c) :135    listMax (l.map f) = listMax (l.map g) := by rw [List.map_congr_left h]136137theorem sum_map_congr' {l : List Circ} {f g : Circ → Nat} (h : ∀ c ∈ l, f c = g c) :138    (l.map f).sum = (l.map g).sum := by rw [List.map_congr_left h]139140theorem aoDepth_nnf : ∀ (p : Bool) (c : Circ), aoDepth (nnf p c) = aoDepth c141  | p, .input i => by cases p <;> simp [nnf, aoDepth]142  | p, .const b => by simp [nnf, aoDepth]143  | p, .not c => by simp only [nnf, aoDepth]; exact aoDepth_nnf (!p) c144  | p, .and cs => by145    rw [nnf_and]146    have h := listMax_map_congr (l := cs) (f := fun c => aoDepth (nnf p c)) (g := aoDepth) (fun c _ => aoDepth_nnf p c)147    cases p <;> simp [List.map_map, Function.comp_def, h]148  | p, .or cs => by149    rw [nnf_or]150    have h := listMax_map_congr (l := cs) (f := fun c => aoDepth (nnf p c)) (g := aoDepth) (fun c _ => aoDepth_nnf p c)151    cases p <;> simp [List.map_map, Function.comp_def, h]152153theorem aoGates_nnf : ∀ (p : Bool) (c : Circ), aoGates (nnf p c) = aoGates c154  | p, .input i => by cases p <;> simp [nnf, aoGates]155  | p, .const b => by simp [nnf, aoGates]156  | p, .not c => by simp only [nnf, aoGates]; exact aoGates_nnf (!p) c157  | p, .and cs => by158    rw [nnf_and]159    have h := sum_map_congr' (l := cs) (f := fun c => aoGates (nnf p c)) (g := aoGates) (fun c _ => aoGates_nnf p c)160    cases p <;> simp [List.map_map, Function.comp_def, h]161  | p, .or cs => by162    rw [nnf_or]163    have h := sum_map_congr' (l := cs) (f := fun c => aoGates (nnf p c)) (g := aoGates) (fun c _ => aoGates_nnf p c)164    cases p <;> simp [List.map_map, Function.comp_def, h]165166theorem maxInput_nnf : ∀ (p : Bool) (c : Circ), maxInput (nnf p c) = maxInput c167  | p, .input i => by cases p <;> simp [nnf]168  | p, .const b => by simp [nnf]169  | p, .not c => by simp only [nnf, maxInput_not]; exact maxInput_nnf (!p) c170  | p, .and cs => by171    rw [nnf_and]172    have h := listMax_map_congr (l := cs) (f := fun c => maxInput (nnf p c)) (g := maxInput) (fun c _ => maxInput_nnf p c)173    cases p <;> simp [List.map_map, Function.comp_def, h]174  | p, .or cs => by175    rw [nnf_or]176    have h := listMax_map_congr (l := cs) (f := fun c => maxInput (nnf p c)) (g := maxInput) (fun c _ => maxInput_nnf p c)177    cases p <;> simp [List.map_map, Function.comp_def, h]178179theorem aoDepth_le : ∀ c : Circ, aoDepth c ≤ depth c180  | .input i => by simp [aoDepth]181  | .const b => by simp [aoDepth]182  | .not c => by simp only [aoDepth, depth_not]; have := aoDepth_le c; omega183  | .and cs => by184    simp only [aoDepth_and, depth_and]185    have : listMax (cs.map aoDepth) ≤ listMax (cs.map depth) := by186      apply listMax_le; intro a ha187      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha188      exact Nat.le_trans (aoDepth_le c) (le_listMax (List.mem_map_of_mem hc))189    omega190  | .or cs => by191    simp only [aoDepth_or, depth_or]192    have : listMax (cs.map aoDepth) ≤ listMax (cs.map depth) := by193      apply listMax_le; intro a ha194      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha195      exact Nat.le_trans (aoDepth_le c) (le_listMax (List.mem_map_of_mem hc))196    omega197198theorem aoGates_le : ∀ c : Circ, aoGates c ≤ size c199  | .input i => by simp [aoGates]200  | .const b => by simp [aoGates]201  | .not c => by simp only [aoGates, size_not]; have := aoGates_le c; omega202  | .and cs => by203    simp only [aoGates_and, size_and]204    have := sum_map_le_mem (l := cs) (f := aoGates) (g := size) (fun c _ => aoGates_le c)205    omega206  | .or cs => by207    simp only [aoGates_or, size_or]208    have := sum_map_le_mem (l := cs) (f := aoGates) (g := size) (fun c _ => aoGates_le c)209    omega210211/-- Lemma lem:unit-ac0 in the paper's convention: one fixed-scale gate is a DEPTH-2 DNF212    when negations on inputs are not counted (our NOT-counting depth bound was 3). -/213theorem dnf_aoDepth (W : Nat) (g : Gate) : aoDepth (dnf W g) ≤ 2 := by214  unfold dnf215  rw [aoDepth_or]216  have : listMax ((((boards (g.fanin + 1) W).filter (fun t => decide (g.thr ≤ selSum g t))).map (termC g)).map aoDepth) ≤ 1 := by217    apply listMax_le; intro a ha218    obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha219    obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc220    unfold termC; rw [aoDepth_and]221    have : listMax ((t.filterMap (fun j => if j < g.fanin then some (litC g j) else none)).map aoDepth) ≤ 0 := by222      apply listMax_le; intro b hb223      obtain ⟨c', hc', rfl⟩ := List.mem_map.mp hb224      obtain ⟨j, _, hj⟩ := List.mem_filterMap.mp hc'225      split at hj226      · cases hj; unfold litC; split <;> simp [aoDepth]227      · cases hj228    omega229  omega230231/-! ## Correlation conventions -/232233/-- Agreement count of a formula with parity on m bits. -/234def agree (m : Nat) (C : Circ) : Rat := rsum (bitvecs m) (fun y => if eval (vfun y) C = par y then 1 else 0)235236/-- Håstad's signed correlation c, defined by Pr[C = PAR] = (1 + c)/2. -/237def scorr (m : Nat) (C : Circ) : Rat := 2 * agree m C / (2 : Rat) ^ m - 1238239theorem sgn_not' (b : Bool) : sgn (!b) = -sgn b := by cases b <;> decide240241theorem sgn_par_sum {m : Nat} (hm : 1 ≤ m) : rsum (bitvecs m) (fun y => sgn (par y)) = 0 := by242  obtain ⟨n, rfl⟩ : ∃ n, m = n + 1 := ⟨m - 1, by omega⟩243  rw [rsum_bitvecs_succ]244  have e : rsum (bitvecs n) (fun v => sgn (par (true :: v))) = rsum (bitvecs n) (fun v => (-1) * sgn (par v)) := by245    apply rsum_congr; intro v _; simp only [par, Bool.true_xor]; rw [sgn_not']; grind246  rw [e, rsum_mul_left]247  have e2 : rsum (bitvecs n) (fun v => sgn (par (false :: v))) = rsum (bitvecs n) (fun v => sgn (par v)) := by248    apply rsum_congr; intro v _; simp [par]249  rw [e2]; grind250251/-- CONVENTION ADAPTER: for m ≥ 1, E[1_C · (−1)^PAR] = −scorr/2. -/252theorem indicator_signed {m : Nat} (hm : 1 ≤ m) (C : Circ) :253    rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) / (2 : Rat) ^ m = -(scorr m C) / 2 := by254  have hpt : ∀ y : List Bool, ind (eval (vfun y) C) * sgn (par y) =255      (1 / 2) * sgn (par y) + ((-1) * (if eval (vfun y) C = par y then 1 else 0) + 1 / 2) := by256    intro y257    cases eval (vfun y) C <;> cases par y <;> simp [ind, sgn] <;> grind258  rw [rsum_congr (fun y _ => hpt y), rsum_add, rsum_add, rsum_mul_left, rsum_mul_left, rsum_const,259    sgn_par_sum hm, length_bitvecs]260  unfold scorr agree261  have hT : (0 : Rat) < (2 : Rat) ^ m := two_pow_pos' m262  have hc : (((2 ^ m : Nat) : Rat)) = (2 : Rat) ^ m := by simp263  rw [hc]264  generalize rsum (bitvecs m) (fun y => if eval (vfun y) C = par y then (1 : Rat) else 0) = A265  generalize (2 : Rat) ^ m = T at hT ⊢266  have hT' : T ≠ 0 := Rat.ne_of_gt hT267  grind268269/-! ## The external input and its consequences -/270271/-- Negligible nonnegative rational sequence: below every inverse polynomial eventually. -/272def Negligible (f : Nat → Rat) : Prop :=273  (∀ n, 0 ≤ f n) ∧ ∀ k : Nat, ∃ n0 : Nat, ∀ n, n0 ≤ n → f n * ((n : Rat) + 1) ^ k ≤ 1274275/-- Classical-convention correlation bound for given depth, gate count and input length:276    every negation-normal formula with AND/OR depth ≤ d and ≤ S AND/OR gates reading m ≥ 1277    inputs has |signed correlation with parity| ≤ δ. -/278def ClassicalCorr (d S m : Nat) (δ : Rat) : Prop :=279  ∀ C : Circ, negLeaf C = true → aoDepth C ≤ d → aoGates C ≤ S → maxInput C ≤ m →280    -δ ≤ scorr m C ∧ scorr m C ≤ δ281282/-- THE EXTERNAL CLASSICAL THEOREM (Håstad 2014, Cor. 3.2, negligible family form), a283    hypothesis: for every depth d and polynomial gate bound c·m^k there is a negligible δ284    with ClassicalCorr d (c·m^k) m (δ m) for all m ≥ 1. -/285def HastadNegl : Prop :=286  ∀ d c k : Nat, ∃ δ : Nat → Rat, Negligible δ ∧ ∀ m, 1 ≤ m → ClassicalCorr d (c * m ^ k) m (δ m)287288theorem classicalCorr_mono {d S S' m : Nat} {δ : Rat} (h : ClassicalCorr d S' m δ) (hS : S ≤ S') :289    ClassicalCorr d S m δ :=290  fun C h1 h2 h3 h4 => h C h1 h2 (Nat.le_trans h3 hS) h4291292theorem classicalCorr_mono_d {d d' S m : Nat} {δ : Rat} (h : ClassicalCorr d' S m δ) (hd : d ≤ d') :293    ClassicalCorr d S m δ :=294  fun C h1 h2 h3 h4 => h C h1 (Nat.le_trans h2 hd) h3 h4295296/-- TRIVIAL DEPTH/SIZE CASES: Håstad's corollary is stated for depth d ≥ 2 and nontrivial297    size; the family form HastadNegl follows from the instances with d ≥ 2, c ≥ 1, k ≥ 1298    alone, since ClassicalCorr is monotone in depth and size. -/299theorem hastadNegl_of_deep300    (h : ∀ d c k : Nat, 2 ≤ d → 1 ≤ c → 1 ≤ k →301      ∃ δ : Nat → Rat, Negligible δ ∧ ∀ m, 1 ≤ m → ClassicalCorr d (c * m ^ k) m (δ m)) :302    HastadNegl := by303  intro d c k304  obtain ⟨δ, hδ, hc⟩ := h (d + 2) (c + 1) (k + 1) (by omega) (by omega) (by omega)305  refine ⟨δ, hδ, fun m hm => ?_⟩306  have hS : c * m ^ k ≤ (c + 1) * m ^ (k + 1) :=307    Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right hm (by omega))308  exact classicalCorr_mono_d (classicalCorr_mono (hc m hm) hS) (by omega)309310/-- ADAPTER: the classical-convention bound gives the phase-3 indicator premise with δ/2. -/311theorem premise_of_classical {d S m : Nat} {δ : Rat} (hm : 1 ≤ m) (h : ClassicalCorr d S m δ) :312    ParityCorrPremise d S m (δ / 2) := by313  intro C hd hs hmx314  have hC := h (nnf false C) (negLeaf_nnf false C) (by rw [aoDepth_nnf]; exact Nat.le_trans (aoDepth_le C) hd)315    (by rw [aoGates_nnf]; exact Nat.le_trans (aoGates_le C) hs) (by rw [maxInput_nnf]; exact hmx)316  have he : scorr m (nnf false C) = scorr m C := by317    unfold scorr agree318    rw [rsum_congr (fun y _ => by rw [eval_nnf, Bool.false_xor])]319  rw [he] at hC320  rw [indicator_signed hm C]321  obtain ⟨h1, h2⟩ := hC322  have two : (0 : Rat) < 2 := by decide323  have a1 := div_le_div_of_le two (show -scorr m C ≤ δ by grind)324  have a2 := div_le_div_of_le two (show -δ ≤ -scorr m C by grind)325  have e1 : -(δ / 2) = -δ / 2 := by grind326  rw [e1]327  exact ⟨a2, a1⟩328329theorem premise_mono {d S m : Nat} {ε ε' : Rat} (h : ParityCorrPremise d S m ε) (he : ε ≤ ε') :330    ParityCorrPremise d S m ε' := by331  intro C h1 h2 h3; obtain ⟨a, b⟩ := h C h1 h2 h3; constructor <;> grind332333/-- WORST-CASE HARDNESS FROM THE EXTERNAL INPUT: HastadNegl ⇒ ParityNotAC0. -/334theorem parityNotAC0_of_hastad (hH : HastadNegl) : ParityNotAC0 := by335  intro d c k336  obtain ⟨δ, ⟨hnn, hneg⟩, hcorr⟩ := hH d c k337  obtain ⟨n0, hn0⟩ := hneg 1338  refine ⟨max n0 1, fun m hm => hard_of_premise (ε := 1 / 4) (by omega) (by grind)339    (premise_mono (premise_of_classical (by omega) (hcorr m (by omega))) ?_)⟩340  have h1 := hn0 m (by omega)341  have hm1 : (1 : Rat) ≤ (m : Rat) := by exact_mod_cast (show 1 ≤ m by omega)342  have hpos := hnn m343  simp only [Rat.pow_one] at h1344  -- δ m · (m + 1) ≤ 1 with m ≥ 1 gives δ m ≤ 1/2 < 1345  have : δ m ≤ 1 / 2 := by346    have h2 : δ m * 2 ≤ δ m * ((m : Rat) + 1) := Rat.mul_le_mul_of_nonneg_left (by grind) hpos347    grind348  have h3 := div_le_div_of_le (show (0 : Rat) < 2 by decide) this349  have e : (1 / 2 : Rat) / 2 = 1 / 4 := by grind350  rw [e] at h3; exact h3351352/-! ## The asymptotic single-channel bound (Theorem thm:search-gap (i)) -/353354/-- Sum of δ(m) over the restriction supports N+1 ≤ m ≤ B(N+1) (an upper bound for each355    δ(m)/2, uniform over the supports). -/356def etaSum (δ : Nat → Rat) (B N : Nat) : Rat :=357  rsum ((List.range (B * (N + 1) + 1)).filter (fun m => decide (N + 1 ≤ m))) δ358359theorem rsum_nonneg' {l : List Nat} {f : Nat → Rat} (h : ∀ x ∈ l, 0 ≤ f x) : 0 ≤ rsum l f := by360  induction l with361  | nil => rw [rsum_nil]; exact Rat.le_refl362  | cons a l ih =>363    simp only [rsum_cons]364    have := h a (by simp); have := ih (fun x hx => h x (List.mem_cons_of_mem _ hx)); grind365366theorem term_le_rsum {l : List Nat} {f : Nat → Rat} (h : ∀ x ∈ l, 0 ≤ f x) {a : Nat} (ha : a ∈ l) :367    f a ≤ rsum l f := by368  induction l with369  | nil => cases ha370  | cons b l ih =>371    simp only [rsum_cons]372    rcases List.mem_cons.mp ha with rfl | h'373    · have := rsum_nonneg' (fun x hx => h x (List.mem_cons_of_mem _ hx)); grind374    · have := ih (fun x hx => h x (List.mem_cons_of_mem _ hx)) h'; have := h b (by simp); grind375376theorem pow_cast_le {N m k : Nat} (h : N ≤ m) : ((N : Rat) + 1) ^ k ≤ ((m : Rat) + 1) ^ k := by377  have : ((N + 1 : Nat) : Rat) ^ k ≤ ((m + 1 : Nat) : Rat) ^ k := by378    rw [← Rat.natCast_pow, ← Rat.natCast_pow]; exact_mod_cast Nat.pow_le_pow_left (show N + 1 ≤ m + 1 by omega) k379  simpa using this380381theorem term_shift {x : Rat} {N m k : Nat} (hx : 0 ≤ x) (h : x * ((m : Rat) + 1) ^ k ≤ 1) (hNm : N ≤ m) :382    x * ((N : Rat) + 1) ^ k ≤ 1 :=383  Rat.le_trans (Rat.mul_le_mul_of_nonneg_left (pow_cast_le hNm) hx) h384385theorem rsum_count_le {L : List Nat} {δ : Nat → Rat} {Q : Rat} (h : ∀ m ∈ L, δ m * Q ≤ 1) :386    rsum L δ * Q ≤ (L.length : Rat) := by387  induction L with388  | nil => rw [rsum_nil, Rat.zero_mul]; simp; exact Rat.le_refl389  | cons a L ih =>390    simp only [rsum_cons, List.length_cons]391    have h1 := h a (by simp)392    have h2 := ih (fun m hm => h m (List.mem_cons_of_mem _ hm))393    generalize rsum L δ = R at h2 ⊢394    generalize δ a = x at h1 ⊢395    have e : (x + R) * Q = x * Q + R * Q := by grind396    rw [e]397    push_cast398    grind399400theorem half_le_self {x : Rat} (hx : 0 ≤ x) : x / 2 ≤ x :=401  le_div_of_mul_le (by decide) (by grind)402403theorem le_one_of_mul {Y Q : Rat} (hQ : 0 < Q) (h : Y * Q ≤ Q) : Y ≤ 1 :=404  Rat.le_of_mul_le_mul_right (by rw [Rat.one_mul]; exact h) hQ405406theorem pow_two_split (a e x : Rat) (k : Nat) : a * e * x ^ k * (x * x) = a * (e * x ^ (k + 2)) := by407  rw [Rat.pow_succ, Rat.pow_succ]; grind408409/-- Negligibility of the support-uniform error for fixed B (any constant factor a). -/410theorem etaSum_negligible {δ : Nat → Rat} (hδ : Negligible δ) (B : Nat) (a : Nat) :411    Negligible (fun N => (a : Rat) * etaSum δ B N) := by412  obtain ⟨hnn, hneg⟩ := hδ413  have ha0 : (0 : Rat) ≤ (a : Rat) := by exact_mod_cast Nat.zero_le a414  have hη : ∀ N, 0 ≤ etaSum δ B N := fun N => rsum_nonneg' (fun m _ => hnn m)415  refine ⟨fun N => Rat.mul_nonneg ha0 (hη N), fun k => ?_⟩416  obtain ⟨n1, hn1⟩ := hneg (k + 2)417  refine ⟨n1 + a * (B + 1), fun N hN => ?_⟩418  have hNpos : (0 : Rat) < (N : Rat) + 1 := by419    have : (0 : Rat) ≤ (N : Rat) := by exact_mod_cast Nat.zero_le N420    grind421  have hQ : (0 : Rat) ≤ ((N : Rat) + 1) ^ (k + 2) := Rat.le_of_lt (Rat.pow_pos hNpos)422  -- sum bound423  have hsum : etaSum δ B N * ((N : Rat) + 1) ^ (k + 2) ≤424      (((List.range (B * (N + 1) + 1)).filter (fun m => decide (N + 1 ≤ m))).length : Rat) := by425    unfold etaSum426    apply rsum_count_le427    intro m hm428    simp only [List.mem_filter, List.mem_range, decide_eq_true_eq] at hm429    exact term_shift (hnn m) (hn1 m (by omega)) (by omega)430  have hlen : ((List.range (B * (N + 1) + 1)).filter (fun m => decide (N + 1 ≤ m))).length ≤ (B + 1) * (N + 1) := by431    have h1 := List.length_filter_le (fun m => decide (N + 1 ≤ m)) (List.range (B * (N + 1) + 1))432    rw [List.length_range] at h1433    have : B * (N + 1) + 1 ≤ (B + 1) * (N + 1) := by rw [Nat.add_mul, Nat.one_mul]; omega434    omega435  have hcount : a * ((B + 1) * (N + 1)) ≤ (N + 1) * (N + 1) := by436    rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right _ (by omega)437  have hlenR : (a : Rat) * ((((List.range (B * (N + 1) + 1)).filter (fun m => decide (N + 1 ≤ m))).length : Rat)) ≤438      ((N : Rat) + 1) * ((N : Rat) + 1) := by439    have h1 : ((a * (((List.range (B * (N + 1) + 1)).filter (fun m => decide (N + 1 ≤ m))).length) : Nat) : Rat) ≤440        (((N + 1) * (N + 1) : Nat) : Rat) := by441      exact_mod_cast Nat.le_trans (Nat.mul_le_mul_left a hlen) hcount442    push_cast at h1443    exact h1444  apply le_one_of_mul (Rat.mul_pos hNpos hNpos)445  show (a : Rat) * etaSum δ B N * ((N : Rat) + 1) ^ k * (((N : Rat) + 1) * ((N : Rat) + 1)) ≤ _446  rw [pow_two_split]447  exact Rat.le_trans (Rat.mul_le_mul_of_nonneg_left hsum ha0) hlenR448449def uparE (B c k : Nat) : PE Nat :=450  12 * ((vB + 2) * PE.c (B + 2) * ((PE.c c * vB ^ k + 1) * (PE.c c * vB ^ k + 1) + 2)) ^ 10451452theorem uparE_eval (B c k N : Nat) : PE.eval (fun _ N => N + 1) (uparE B c k) N =453    12 * (((N + 1) + 2) * (B + 2) * ((c * (N + 1) ^ k + 1) * (c * (N + 1) ^ k + 1) + 2)) ^ 10 := rfl454455/-- The premise size of the correlation bridge is polynomial in N + 1 for fixed B. -/456theorem upar_poly (B c k : Nat) : PolyIn (fun _ : Nat => True) (fun N => N + 1)457    (fun N => 12 * (((N + 1) + 2) * (B + 2) * ((c * (N + 1) ^ k + 1) * (c * (N + 1) ^ k + 1) + 2)) ^ 10) :=458  polyE (ι := Nat) (fun i _ => Nat.succ_le_succ (Nat.zero_le i)) (fun _ N => N + 1) (fun _ _ _ => Nat.le_refl _)459    (uparE B c k) _ (fun N => (uparE_eval B c k N).symm)460461def netE (W L c k : Nat) : PE Nat := 2 * (PE.c (2 * W + 3) ^ L * (PE.c c * vB ^ k + 1) ^ (W * L)) + PE.c c * vB ^ k462463theorem netE_eval (W L c k N : Nat) : PE.eval (fun _ N => N + 1) (netE W L c k) N =464    2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L)) + c * (N + 1) ^ k := rfl465466/-- The network readout size is polynomial in N + 1. -/467theorem netsize_poly (W L c k : Nat) : PolyIn (fun _ : Nat => True) (fun N => N + 1)468    (fun N => 2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L)) + c * (N + 1) ^ k) :=469  polyE (ι := Nat) (fun i _ => Nat.succ_le_succ (Nat.zero_le i)) (fun _ N => N + 1) (fun _ _ _ => Nat.le_refl _)470    (netE W L c k) _ (fun N => (netE_eval W L c k N).symm)471472/-- ASYMPTOTIC SINGLE-CHANNEL THEOREM (thm:search-gap (i), asymptotic form), conditional473    only on the external classical input.  Fix B ≥ 2 and j < B.  Let R N b be binary474    readout formulas for N+1 heaps with BBound of FIXED depth d and size s N, index width475    r N, where s and r are polynomially bounded in N+1.  Then there is a negligible η with476      success_N ≤ 2/(2^B − 1) + η N   for every N. -/477theorem search_gap_asymptotic (hH : HastadNegl) {B j : Nat} (hj : j < B)478    (R : Nat → Bool → BCirc) (r s : Nat → Nat) (d : Nat)479    (hb : ∀ N b, BBound (R N b) (N + 1) B (r N) d (s N))480    (hpoly : ∃ c k, ∀ N, s N ≤ c * (N + 1) ^ k ∧ r N ≤ c * (N + 1) ^ k) :481    ∃ η : Nat → Rat, Negligible η ∧ ∀ N,482      succCountRO B (N + 1) (binReadoutOf B (N + 1) (R N)) j / nonzeroCount B (N + 1) ≤483        2 / (((2 ^ B : Nat) : Rat) - 1) + η N := by484  obtain ⟨c, k, hck⟩ := hpoly485  -- the premise size: 12 Upar(N+1) B ((r+1)(s+1))^10 is polynomial in N+1, hence in m ≥ N+1486  let S' : Nat → Nat := fun N => 12 * Upar (N + 1) B ((r N + 1) * (s N + 1)) ^ 10487  obtain ⟨C, K, hCK⟩ := upar_poly B c k488  have hS'le : ∀ N, S' N ≤ C * (N + 1) ^ K := by489    intro N490    refine Nat.le_trans ?_ (hCK N trivial)491    show 12 * Upar (N + 1) B ((r N + 1) * (s N + 1)) ^ 10 ≤ _492    unfold Upar493    apply Nat.mul_le_mul_left494    apply Nat.pow_le_pow_left495    apply Nat.mul_le_mul_left496    have h1 := (hck N).1; have h2 := (hck N).2497    have := Nat.mul_le_mul (show r N + 1 ≤ c * (N + 1) ^ k + 1 by omega) (show s N + 1 ≤ c * (N + 1) ^ k + 1 by omega)498    omega499  obtain ⟨δ, hδ, hcorr⟩ := hH (d + 2 + 11) C K500  refine ⟨fun N => (((2 ^ B - 1 : Nat) : Rat)) * etaSum δ B N, ?_, fun N => ?_⟩501  · exact etaSum_negligible hδ B (2 ^ B - 1)502  · have hbound := binary_readout_bound hj (R N) (hb N) (ε := etaSum δ B N) (fun m hm1 hm2 => by503      have hcl := classicalCorr_mono (hcorr m (by omega)) (show S' N ≤ C * m ^ K from504        Nat.le_trans (hS'le N) (Nat.mul_le_mul_left C (Nat.pow_le_pow_left hm1 K)))505      refine premise_mono (premise_of_classical (by omega) hcl) (Rat.le_trans (half_le_self (hδ.1 m)) ?_)506      apply term_le_rsum (fun x _ => hδ.1 x)507      simp only [List.mem_filter, List.mem_range, decide_eq_true_eq]; omega)508    have e : (((2 ^ B : Nat) : Rat) - 1) = (((2 ^ B - 1 : Nat) : Rat)) := (natCast_pred B).symm509    rw [e] at hbound ⊢510    exact hbound511512/-- The same for readouts computed by fixed-scale threshold networks (W, L fixed,513    polynomial widths), compiled by the finite-input compiler. -/514theorem search_gap_asymptotic_net (hH : HastadNegl) {B j W L : Nat} (hj : j < B)515    (nets : Nat → Bool → List Layer) (r : Nat → Nat) (hlen : ∀ N b, (nets N b).length ≤ L)516    (hv : ∀ N b, NetValid W (nets N b)) (hr : ∀ N, N + 1 ≤ 2 ^ r N)517    (hpoly : ∃ c k, ∀ N b, NetBounded (c * (N + 1) ^ k) (nets N b) ∧ r N ≤ c * (N + 1) ^ k) :518    ∃ η : Nat → Rat, Negligible η ∧ ∀ N,519      succCountRO B (N + 1) (binReadoutOf B (N + 1) (fun b => netBCirc W B (N + 1) (r N) (nets N b))) j /520          nonzeroCount B (N + 1) ≤ 2 / (((2 ^ B : Nat) : Rat) - 1) + η N := by521  obtain ⟨c, k, hck⟩ := hpoly522  let s : Nat → Nat := fun N => 2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L))523  apply search_gap_asymptotic hH hj (fun N b => netBCirc W B (N + 1) (r N) (nets N b)) r s (3 * L)524  · intro N b525    have hb := netBCirc_BBound (B := B) (N := N + 1) (r := r N) (nets N b) (hv N b) (hck N b).1 (hr N)526    have hl := hlen N b527    refine bbound_mono hb (Nat.mul_le_mul_left 3 hl) ?_528    have e1 : (2 * W + 3) ^ (nets N b).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl529    have e2 : (c * (N + 1) ^ k + 1) ^ (W * (nets N b).length) ≤ (c * (N + 1) ^ k + 1) ^ (W * L) :=530      Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)531    have := Nat.mul_le_mul e1 e2532    show 2 * ((2 * W + 3) ^ (nets N b).length * (c * (N + 1) ^ k + 1) ^ (W * (nets N b).length)) ≤ s N533    simp only [s]; omega534  · obtain ⟨C, K, hCK⟩ := netsize_poly W L c k535    refine ⟨C, K, fun N => ⟨?_, ?_⟩⟩536    · have h1 := hCK N trivial; dsimp only at h1537      show 2 * ((2 * W + 3) ^ L * (c * (N + 1) ^ k + 1) ^ (W * L)) ≤ C * (N + 1) ^ K; omega538    · have h1 := hCK N trivial; have h2 := (hck N false).2; dsimp only at h1; omega539540/-! ## Axiom audit -/541542#print axioms aoDepth_and543#print axioms aoDepth_or544#print axioms aoGates_and545#print axioms aoGates_or546#print axioms negLeaf_and547#print axioms negLeaf_or548#print axioms nnf_and549#print axioms nnf_or550#print axioms any_not_eq551#print axioms all_not_eq552#print axioms eval_nnf553#print axioms negLeaf_nnf554#print axioms listMax_map_congr555#print axioms sum_map_congr'556#print axioms aoDepth_nnf557#print axioms aoGates_nnf558#print axioms maxInput_nnf559#print axioms aoDepth_le560#print axioms aoGates_le561#print axioms dnf_aoDepth562#print axioms sgn_not'563#print axioms sgn_par_sum564#print axioms indicator_signed565#print axioms classicalCorr_mono566#print axioms classicalCorr_mono_d567#print axioms hastadNegl_of_deep568#print axioms premise_of_classical569#print axioms premise_mono570#print axioms parityNotAC0_of_hastad571#print axioms rsum_nonneg'572#print axioms term_le_rsum573#print axioms pow_cast_le574#print axioms term_shift575#print axioms rsum_count_le576#print axioms half_le_self577#print axioms le_one_of_mul578#print axioms pow_two_split579#print axioms etaSum_negligible580#print axioms uparE_eval581#print axioms upar_poly582#print axioms netE_eval583#print axioms netsize_poly584#print axioms search_gap_asymptotic585#print axioms search_gap_asymptotic_net586587