`bitBandwidthPerCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.PvsNPFromBIT
domain: Complexity
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.PvsNPFromBIT on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  42/-! ## §1. Bandwidth of the recognition substrate -/
  43
  44/-- Per-cycle BIT bandwidth: `8 · consciousnessGap = 8 · 45 = 360`. -/
  45def bitBandwidthPerCycle : ℕ := 8 * 45
  46
  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,

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.