exp_dominates_poly
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.