exp_dominates_poly
Exponential growth eventually overtakes any fixed polynomial. Researchers proving circuit lower bounds for SAT cite this fact to convert exponential gate-count lower bounds into super-polynomial size statements. The argument lifts the inequality to the reals, invokes Mathlib's tendsto_pow_const_div_const_pow_of_one_lt to obtain an eventual bound on the ratio, then clears denominators with positivity and field simplification.
claimFor any natural numbers $C$ and $d$ there exists a natural number $m_0$ such that for all natural numbers $m$ with $m_0 ≤ m$, $C · m^d < 2^m$.
background
The module formalizes circuit lower bounds from J-frustration in the Recognition Science framework. J-frustration quantifies the multiplicative cost structure induced by the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. High frustration on unsatisfiable 3-SAT formulas forces exponential circuit size via topological obstructions, as described in the module overview.
proof idea
The proof first reduces the statement to the reals by casting. It applies tendsto_pow_const_div_const_pow_of_one_lt (with base 2 > 1) to obtain that $n^d / 2^n$ is eventually less than $1/(C+1)$. The inequality is then rewritten via div_lt_iff₀, multiplied through by the positive term $C+1$, and simplified with field_simp and linarith to recover the original bound.
why it matters in Recognition Science
This theorem is invoked inside p_neq_np_conditional to conclude that the exponential lower bound $2^{n/k}$ from the uniform topological obstruction exceeds any fixed polynomial. It completes the analytic step in the conditional P ≠ NP argument. In the Recognition framework it supports the claim that J-frustration on 3-SAT instances produces super-polynomial circuit complexity, consistent with the eight-tick octave and phi-ladder structure.
scope and limits
- Does not supply an explicit closed-form value for m₀.
- Does not apply when C or d are not natural numbers.
- Does not address constants arising from specific circuit constructions.
- Does not prove the uniform topological obstruction hypothesis itself.
formal statement (Lean)
137private theorem exp_dominates_poly (C d : ℕ) :
138 ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → C * m ^ d < 2 ^ m := by
proof body
Tactic-mode proof.
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. -/