exp_dominates_poly

formal source

 134/-- **Exponential eventually dominates any polynomial.**
 135    For any C, d, there exists m₀ such that C * m^d < 2^m for all m ≥ m₀.
 136    Proof uses Mathlib's `tendsto_pow_const_div_const_pow_of_one_lt`. -/
 137private theorem exp_dominates_poly (C d : ℕ) :
 138    ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → C * m ^ d < 2 ^ m := by
 139  suffices h : ∃ m₀ : ℕ, ∀ m, m₀ ≤ m → (C : ℝ) * (m : ℝ) ^ d < (2 : ℝ) ^ m by
 140    obtain ⟨m₀, hm₀⟩ := h; exact ⟨m₀, fun m hm => by exact_mod_cast hm₀ m hm⟩
 141  have htend := tendsto_pow_const_div_const_pow_of_one_lt d
 142    (show (1 : ℝ) < 2 by norm_num)
 143  have hev : ∀ᶠ n : ℕ in Filter.atTop,
 144      (n : ℝ) ^ d / (2 : ℝ) ^ n < 1 / ((C : ℝ) + 1) :=
 145    htend.eventually (Iio_mem_nhds (by positivity : (0 : ℝ) < 1 / ((↑C : ℝ) + 1)))
 146  rw [Filter.eventually_atTop] at hev
 147  obtain ⟨m₀, hm₀⟩ := hev
 148  exact ⟨m₀, fun m hm => by
 149    have hlt := hm₀ m hm
 150    have h2 : (0 : ℝ) < (2 : ℝ) ^ m := by positivity
 151    have hC1 : (0 : ℝ) < (C : ℝ) + 1 := by positivity
 152    have hmd : (0 : ℝ) ≤ (m : ℝ) ^ d := by positivity
 153    rw [div_lt_iff₀ h2] at hlt
 154    have key := mul_lt_mul_of_pos_left hlt hC1
 155    rw [show ((C : ℝ) + 1) * ((1 / ((C : ℝ) + 1)) * (2 : ℝ) ^ m) = (2 : ℝ) ^ m from by
 156      field_simp] at key
 157    linarith⟩
 158
 159/-- **THEOREM (P ≠ NP from Uniform Topological Obstruction).**
 160
 161    If the uniform topological obstruction holds with parameter k, then for
 162    sufficiently large n, no polynomial-size circuit can decide satisfiability.
 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₀ : ℕ),