String equality decided in linear time by multi-tape Turing machine

Proved

CookLevin.tapeEquality_comparator

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

comparatorlinear-timestring-equalityturing-machine

There exists a multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ that decides equality between two binary strings $x$ and $y$ :

V(x, y) = [y = x]

within linear time $c_2 (|x| + 1)$ for a constant $c_2 \in \mathbb{N}$ .

The machine advances its heads simultaneously across tape 0 (holding $x$ ) and tape 1 (holding $y$ ), comparing tape symbols at each position until encountering a blank. If all symbols match and blanks are reached concurrently, the machine writes $\mathbf{1}$ (accept) to cell 1 of the verdict tape; otherwise, it writes $\mathbf{0}$ (reject). The total step count is linear in the length of the strings.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem tapeEquality_comparator :
    ∃ (M : Machine) (k G c2 : Nat),
      TuringMachine k G M ∧
      ∀ x y : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols y)
          (c2 * (x.length + 1))
          (decide (y = x)) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Basic.lean#L70

View graph