npWorkload_pos

formal source

  66certify an NP-search witness of size `n` (i.e., search space `2^n`). -/
  67def npWorkload (n : ℕ) : ℕ := 2 ^ n
  68
  69theorem npWorkload_pos (n : ℕ) : 0 < npWorkload n :=
  70  pow_pos (by norm_num : (0:ℕ) < 2) n
  71
  72/-! ## §3. Lower-bound theorem -/
  73
  74/-- **STRUCTURAL LOWER BOUND.** If a recognition substrate of bandwidth
  75`bitBandwidthPerCycle` certifies an NP-search witness in `t` cycles,
  76then `bandwidthBudget t ≥ npWorkload n`. -/
  77theorem certify_requires_budget {n t : ℕ}
  78    (h : bandwidthBudget t ≥ npWorkload n) :
  79    bitBandwidthPerCycle * t ≥ 2 ^ n := by
  80  unfold bandwidthBudget npWorkload at h
  81  exact h
  82
  83/-- The contrapositive: insufficient budget cannot certify the witness. -/
  84theorem insufficient_budget_no_certify {n t : ℕ}
  85    (h : bitBandwidthPerCycle * t < 2 ^ n) :
  86    bandwidthBudget t < npWorkload n := by
  87  unfold bandwidthBudget npWorkload
  88  exact h
  89
  90/-- **EXPONENTIAL LOWER BOUND.** The minimum number of cycles to
  91certify an NP-search witness of size `n` is `⌈2^n / 360⌉`. We give
  92the strict-floor form: at `t < 2^n / 360`, the budget is strictly
  93smaller than the workload. -/
  94theorem cycles_lower_bound {n t : ℕ}
  95    (h : 360 * t < 2 ^ n) :
  96    bandwidthBudget t < npWorkload n := by
  97  apply insufficient_budget_no_certify
  98  rw [bitBandwidthPerCycle_eq]
  99  exact h