Sequential composition of verifier machines decides conjunction

Open

CookLevin.verifierMachine_and_sum

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

complexity-theorysequential-compositionturing-machineverifier

Given two concrete verifier machines $\mathrm{mf}$ and $\mathrm{mg}$ deciding binary predicates $f$ and $g$ respectively, there exists a composed multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ that decides their conjunction:

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

within the exact sum of the two polynomial step bounds:

\mathrm{polyBound}(\mathrm{mf}.c, \mathrm{mf}.d, |x| + |w|) + \mathrm{polyBound}(\mathrm{mg}.c, \mathrm{mg}.d, |x| + |w|).

The machine $M$ is constructed by sequentially combining the transition tables of $\mathrm{mf}$ and $\mathrm{mg}$ , running $\mathrm{mf}$ on the input $(x, w)$ and, upon an accepting verdict on the verdict tape, running $\mathrm{mg}$ on the same input, producing the final conjunction verdict.

Preamble

import Definitions.Def_CookLevin_Complexity

Formal statement

namespace CookLevin
theorem verifierMachine_and_sum (f g : List Bool → List Bool → Bool)
    (mf : VerifierMachine f) (mg : VerifierMachine g) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (polyBound mf.c mf.d (x.length + w.length) + polyBound mg.c mg.d (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