bandwidthBudget_succ

formal source

  56theorem bandwidthBudget_zero : bandwidthBudget 0 = 0 := by
  57  unfold bandwidthBudget; ring
  58
  59theorem bandwidthBudget_succ (t : ℕ) :
  60    bandwidthBudget (t + 1) = bandwidthBudget t + bitBandwidthPerCycle := by
  61  unfold bandwidthBudget; ring
  62
  63/-! ## §2. NP-search workload -/
  64
  65/-- The minimum number of distinguishable comparisons required to
  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