Conjunction of PolyTimeDecidable functions is PolyTimeDecidable

Proved

CookLevin.polyTimeDecidable_and

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

closure-propertycomplexity-theorypolynomial-timeturing-machine

If two binary predicates $f$ and $g$ are each polynomial-time decidable (in the sense of PolyTimeDecidable: each is decided by a multi-tape Turing machine running in at most $c(|x|+|w|+1)^d$ steps), then their conjunction

V(x,w) = f(x,w) \wedge g(x,w)

is also polynomial-time decidable.

The proof constructs a composed Turing machine that first runs the machine for $f$ , reads the verdict, and if it accepts, runs the machine for $g$ on a fresh copy of the input. The combined step count is bounded by the sum of the two polynomial bounds, which is itself polynomial.

This is a standard closure property of the class of polynomial-time decidable predicates and is a key building block for showing that the SAT verifier satVerifier is polynomial-time decidable by composing its component checks.

Preamble

import Definitions.Def_CookLevin_Complexity

Formal statement

namespace CookLevin
theorem polyTimeDecidable_and (f g : List Bool → List Bool → Bool)
    (hf : PolyTimeDecidable f) (hg : PolyTimeDecidable g) :
    PolyTimeDecidable (fun x w => f x w && g x w) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Theorem.lean#L9

View graph