pith. machine review for the scientific record. sign in
def 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)

 129def pVsNPFromBITCert : PvsNPFromBITCert where
 130  bw_per_cycle_eq := bitBandwidthPerCycle_eq

proof body

Definition body.

 131  bw_per_cycle_pos := bitBandwidthPerCycle_pos
 132  budget_zero := bandwidthBudget_zero
 133  budget_succ := bandwidthBudget_succ
 134  npWorkload_pos := npWorkload_pos
 135  npWorkload_succ := npWorkload_succ
 136  cycles_lower_bound := @cycles_lower_bound
 137  doubling_separation := doubling_separation
 138
 139/-- **P vs NP ONE-STATEMENT.** Per-cycle BIT bandwidth = 360; an NP-search
 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. -/

depends on (20)

Lean names referenced from this declaration's body.