npWorkload_succ

formal source

 101/-! ## §4. Doubling separation -/
 102
 103/-- Adding one bit to the search space doubles the workload. -/
 104theorem npWorkload_succ (n : ℕ) :
 105    npWorkload (n + 1) = 2 * npWorkload n := by
 106  unfold npWorkload; rw [pow_succ]; ring
 107
 108/-- **STRUCTURAL DOUBLING.** Each additional input bit forces a doubling
 109of the bandwidth budget required. -/
 110theorem doubling_separation (n : ℕ) :
 111    npWorkload (n + 1) - npWorkload n = npWorkload n := by
 112  rw [npWorkload_succ]
 113  omega
 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