Monotonicity of quadratic bound under additional length term

Proved

CookLevin.quad_le_add

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

algebracost-modelmonotonicityquadratic-time

For any leading constant $c_0 \in \mathbb{N}$ and lengths $x, w \in \mathbb{N}$ , the quadratic bound evaluated at $x$ is dominated by the quadratic bound evaluated at the joint sum $x + w$ :

c_0 (x + 1)^2 \le c_0 (x + w + 1)^2.

This inequality follows directly from the monotonicity of addition $x + 1 \le x + w + 1$ , the monotonicity of the power function $n \mapsto n^2$ on natural numbers, and the monotonicity of multiplication by $c_0$ .

This lemma provides the step-count domination required to extend the execution runtime of a unary decision machine to a binary verifier format.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem quad_le_add (c0 x w : Nat) :
    c0 * (x + 1) ^ 2 ≤ c0 * (x + w + 1) ^ 2 := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Cost.lean#L109

View graph