pith. machine review for the scientific record. sign in
structure definition def or abbrev

PvsNPFromBITCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 117structure PvsNPFromBITCert where
 118  bw_per_cycle_eq : bitBandwidthPerCycle = 360
 119  bw_per_cycle_pos : 0 < bitBandwidthPerCycle
 120  budget_zero : bandwidthBudget 0 = 0
 121  budget_succ : ∀ t, bandwidthBudget (t + 1) = bandwidthBudget t + bitBandwidthPerCycle
 122  npWorkload_pos : ∀ n, 0 < npWorkload n
 123  npWorkload_succ : ∀ n, npWorkload (n + 1) = 2 * npWorkload n
 124  cycles_lower_bound :
 125    ∀ {n t : ℕ}, 360 * t < 2 ^ n → bandwidthBudget t < npWorkload n
 126  doubling_separation :
 127    ∀ n, npWorkload (n + 1) - npWorkload n = npWorkload n
 128

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.