bitBandwidthPerCycle_pos

formal source

  47theorem bitBandwidthPerCycle_eq : bitBandwidthPerCycle = 360 := by
  48  unfold bitBandwidthPerCycle; norm_num
  49
  50theorem bitBandwidthPerCycle_pos : 0 < bitBandwidthPerCycle := by
  51  rw [bitBandwidthPerCycle_eq]; norm_num
  52
  53/-- Total bandwidth in `t` cycles. -/
  54def bandwidthBudget (t : ℕ) : ℕ := bitBandwidthPerCycle * t
  55
  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