doubling_separation

formal source

 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
 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