Domination of product by sum squared

Proved

CookLevin.product_le_quad

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

algebracost-modelmonotonicityproductquadratic-time

For any leading constant $c_1 \in \mathbb{N}$ and lengths $x, w \in \mathbb{N}$ , the product $(x + 1)(w + 1)$ scaled by $c_1$ is bounded by the quadratic sum $(x + w + 1)^2$ scaled by $c_1$ :

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

Since $x + 1 \le x + w + 1$ and $w + 1 \le x + w + 1$ , multiplying the two inequalities preserves the order on natural numbers: $(x + 1)(w + 1) \le (x + w + 1)^2$ . Scaling both sides by $c_1$ yields the result.

This algebraic bound bridges the product-time complexity $O(|x| \cdot |w|)$ of CNF evaluation into the quadratic complexity bound $O((|x|+|w|+1)^2)$ .

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem product_le_quad (c1 x w : Nat) :
    c1 * (x + 1) * (w + 1) ≤ c1 * (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