Sequential composition of two decider machines computes conjunction

Proved

CookLevin.sequentialMachine_decides_and

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

closure-propertycomplexity-theorypolynomial-timeturing-machine

Let $f$ and $g$ be Boolean predicates of an instance string $x$ and witness string $w$ . Suppose concrete well-formed multi-tape Turing machines $M_f$ and $M_g$ decide $f$ and $g$ , respectively, within polynomial bounds.

Then there is a well-formed multi-tape Turing machine $M$ and natural numbers $c_1,d_1,c_2,d_2$ such that, for every $x$ and $w$ , $M$ decides their conjunction within the sum of two polynomial bounds:

\operatorname{time}_M(x,w) \le\operatorname{polyBound}(c_1,d_1,|x|+|w|)+\operatorname{polyBound}(c_2,d_2,|x|+|w|).

Its verdict is $f(x,w)\wedge g(x,w)$ . This isolates the reusable machine-construction step needed to prove closure of polynomial-time decidable predicates under conjunction.

Formalization Note The hypotheses expose the two source machines, their well-formedness proofs, and their DecidesIn guarantees explicitly; the conclusion packages the composed machine and its summed running-time bound.

Preamble

import Definitions.Def_CookLevin_Complexity

Formal statement

namespace CookLevin
theorem sequentialMachine_decides_and
    (f g : List Bool → List Bool → Bool)
    (Mf Mg : Machine)
    (kf Gf cf df kg Gg cg dg : Nat)
    (hMf : TuringMachine kf Gf Mf)
    (hMg : TuringMachine kg Gg Mg)
    (hf : ∀ x w : List Bool,
      DecidesIn Mf kf (boolsToSymbols x) (boolsToSymbols w)
        (polyBound cf df (x.length + w.length)) (f x w))
    (hg : ∀ x w : List Bool,
      DecidesIn Mg kg (boolsToSymbols x) (boolsToSymbols w)
        (polyBound cg dg (x.length + w.length)) (g x w)) :
    ∃ (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

Rizvonium, cook_levin_lean_v1, CookLevinLean/Theorem.lean, conjunction-closure construction used for satVerifier_polyTimeDecidable: https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Theorem.lean#L9

View graph