Linear bound is dominated by a polynomial bound

Proved

CookLevin.polyBound_of_linear

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

cost-modellinear-timepolynomial-time

Every linear step bound of the form $c_0 (n + 1)$ is bounded by a 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 = 1$ yields:

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

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

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

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

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

Source