p_neq_np_conditional

formal source

 163
 164    The proof assembles: hypothesis gives gate_count ≥ 2^(n/k), which for
 165    large enough n exceeds any fixed polynomial bound. -/
 166theorem p_neq_np_conditional (hyp : UniformTopologicalObstructionHyp) :
 167    ∀ (poly_k poly_c : ℕ), ∃ (n₀ : ℕ),
 168      ∀ n : ℕ, n₀ ≤ n →
 169        ∀ (f : CNFFormula n), f.isUNSAT →
 170          ∀ (c : BooleanCircuit n), CircuitDecides c f →
 171            ¬ (c.gate_count ≤ poly_c * n ^ poly_k) := by
 172  intro poly_k poly_c
 173  set k := hyp.k
 174  have hk_pos := hyp.k_pos
 175  obtain ⟨m₀, hm₀⟩ := exp_dominates_poly (poly_c * (2 * k) ^ poly_k) poly_k
 176  refine ⟨k * max m₀ 1, fun n hn f hunsat c hdec hle => ?_⟩
 177  set m := n / k
 178  have hm_ge_m₀ : m₀ ≤ m := by
 179    apply (Nat.le_div_iff_mul_le hk_pos).mpr
 180    calc m₀ * k ≤ max m₀ 1 * k := Nat.mul_le_mul_right k (le_max_left m₀ 1)
 181      _ = k * max m₀ 1 := Nat.mul_comm _ _
 182      _ ≤ n := hn
 183  have hm_ge_1 : 1 ≤ m := by
 184    apply (Nat.le_div_iff_mul_le hk_pos).mpr
 185    calc 1 * k = k := Nat.one_mul k
 186      _ = k * 1 := (Nat.mul_one k).symm
 187      _ ≤ k * max m₀ 1 := Nat.mul_le_mul_left k (le_max_right m₀ 1)
 188      _ ≤ n := hn
 189  have hn_le : n ≤ 2 * k * m := by
 190    have h1 : n = k * m + n % k := (Nat.div_add_mod n k).symm
 191    have h2 : n % k < k := Nat.mod_lt n hk_pos
 192    have h3 : k ≤ k * m := Nat.le_mul_of_pos_right k (by linarith : 0 < m)
 193    have h4 : 2 * k * m = k * m + k * m := by ring
 194    linarith
 195  have h_npk : poly_c * n ^ poly_k ≤ poly_c * (2 * k) ^ poly_k * m ^ poly_k := by
 196    calc poly_c * n ^ poly_k