`pvsNP_one_statement`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.PvsNPFromBIT on GitHub at line 143.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 140problem of size `n` requires `≥ ⌈2^n / 360⌉` cycles to certify; each
 141additional input bit doubles the budget. The structural lower bound is
 142exponential in `n` on every BIT-compatible substrate. -/
 143theorem pvsNP_one_statement :
 144    bitBandwidthPerCycle = 360 ∧
 145    (∀ {n t : ℕ}, 360 * t < 2 ^ n → bandwidthBudget t < npWorkload n) ∧
 146    (∀ n, npWorkload (n + 1) = 2 * npWorkload n) :=
 147  ⟨bitBandwidthPerCycle_eq, @cycles_lower_bound, npWorkload_succ⟩
 148
 149end
 150
 151end PvsNPFromBIT
 152end Complexity
 153end IndisputableMonolith

papers checked against this theorem

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