Composition of formula transducer and equality comparator

Open

CookLevin.isFormulaStringB_machine_from_transducer_comparator

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

isformulastringbsequential-compositionturing-machineverifier

Given a transducer Turing machine $M_1$ that computes the formula round-trip encoding $x \mapsto \mathrm{encodeFormula}(\mathrm{decodeFormula}(x))$ in $c_1 (|x| + 1)^2$ steps, and a comparator Turing machine $M_2$ that decides string equality in $c_2 (|x| + 1)$ steps, their sequential composition yields a Turing machine $M$ that decides isFormulaStringB x within the composite step bound:

T(x) = c_1 (|x| + 1)^2 + c_2 (|x| + 1).

The composite machine first executes $M_1$ to write the round-trip encoding onto a work tape, and subsequently executes $M_2$ to compare the original input with the re-encoded string, writing the boolean equality verdict to the verdict tape.

Preamble

import Definitions.Def_CookLevin_Verifier

Formal statement

namespace CookLevin
theorem isFormulaStringB_machine_from_transducer_comparator
    (c1 : Nat) (M1 : Machine) (k1 G1 : Nat) (hwf1 : TuringMachine k1 G1 M1)
    (htrans : ∀ x w : List Bool,
      (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2)).1 = M1.length ∧
      outputOf k1 (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (c1 * (x.length + 1) ^ 2))
        (c1 * (x.length + 1) ^ 2 + 2) = encodeFormula (decodeFormula x))
    (c2 : Nat) (M2 : Machine) (k2 G2 : Nat) (hwf2 : TuringMachine k2 G2 M2)
    (hcomp : ∀ x y : List Bool,
      DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols y)
        (c2 * (x.length + 1))
        (decide (y = x))) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c1 * (x.length + 1) ^ 2 + c2 * (x.length + 1))
          (isFormulaStringB x) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Verifier.lean#L36

View graph