module module

`IndisputableMonolith.Complexity.PvsNPFromBIT`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

def bitBandwidthPerCycle L45
theorem bitBandwidthPerCycle_eq L47
theorem bitBandwidthPerCycle_pos L50
def bandwidthBudget L54
theorem bandwidthBudget_zero L56
theorem bandwidthBudget_succ L59
def npWorkload L67
theorem npWorkload_pos L69
theorem certify_requires_budget L77
theorem insufficient_budget_no_certify L84
theorem cycles_lower_bound L94
theorem npWorkload_succ L104
theorem doubling_separation L110
structure PvsNPFromBITCert L117
def pVsNPFromBITCert L129
theorem pvsNP_one_statement L143