Conjunction of deciders runs in sum of polynomial bounds

Proved

CookLevin.polyTimeDecidable_and_sum

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

complexity-theorypolynomial-timeturing-machineverifier

Given two polynomial-time decidable binary predicates $f$ and $g$ , there exists a multi-tape Turing machine $M$ that decides their boolean conjunction

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

with step count bounded by the sum of two polynomial bounds $\mathrm{polyBound}(c_1, d_1, |x| + |w|) + \mathrm{polyBound}(c_2, d_2, |x| + |w|)$ .

The machine $M$ sequentially executes the decision procedure for $f$ and, upon acceptance, the decision procedure for $g$ , writing the conjunction of their verdicts to the verdict tape.

Preamble

import Definitions.Def_CookLevin_Complexity

Formal statement

namespace CookLevin
theorem polyTimeDecidable_and_sum (f g : List Bool → List Bool → Bool)
    (hf : PolyTimeDecidable f) (hg : PolyTimeDecidable g) :
    ∃ (M : Machine) (k G c1 d1 c2 d2 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (polyBound c1 d1 (x.length + w.length) + polyBound c2 d2 (x.length + w.length))
          (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