PvsNPFromBITCert

formal source

 114
 115/-! ## §5. Master certificate -/
 116
 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
 129def pVsNPFromBITCert : PvsNPFromBITCert where
 130  bw_per_cycle_eq := bitBandwidthPerCycle_eq
 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. -/
 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⟩