certify_requires_budget

formal source

  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
 100
 101/-! ## §4. Doubling separation -/
 102
 103/-- Adding one bit to the search space doubles the workload. -/
 104theorem npWorkload_succ (n : ℕ) :
 105    npWorkload (n + 1) = 2 * npWorkload n := by
 106  unfold npWorkload; rw [pow_succ]; ring
 107