Quadratic bound is dominated by a polynomial bound

Proved

CookLevin.polyBound_of_quad

by Mazecto · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

cost-modelpolynomial-timequadratic-time

Every quadratic step bound of the form $c_0 (n + 1)^2$ is bounded by the canonical polynomial bound $\mathrm{polyBound}(c, d, n) = c (n + 1)^d$ .

Specifically, for any coefficient $c_0 \in \mathbb{N}$ , choosing $c = c_0$ and degree $d = 2$ yields:

c_0 (n + 1)^2 \le \mathrm{polyBound}(c_0, 2, n) = c_0 (n + 1)^2

which holds with equality for all $n \in \mathbb{N}$ .

This lemma bridges quadratic-time machine algorithms into the formal polynomial-time complexity framework PolyTimeDecidable.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem polyBound_of_quad (c0 : Nat) :
    ∃ c d : Nat, ∀ n : Nat, c0 * (n + 1) ^ 2 ≤ polyBound c d n := by sorry
end CookLevin

Source