Core machine construction for transducer-decider pipeline

Open

CookLevin.transducer_pipe_decider_core

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

compositioncook-levinpipelineturing-machine

Given well-formed machines M1 and M2, there exists a fused machine M such that: if M1 halts at time T1 on inputs (xs, ws) producing output y, and M2 decides verdict b on (xs, boolsToSymbols(y)) within T2 steps, then M decides b on (xs, ws) within T1 + T2 steps.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin

theorem transducer_pipe_decider_core
    (M1 : Machine) (k1 G1 : Nat) (hwf1 : TuringMachine k1 G1 M1)
    (M2 : Machine) (k2 G2 : Nat) (hwf2 : TuringMachine k2 G2 M2) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ (xs ws : List Symbol) (T1 T2 : Nat) (y : List Bool) (b : Bool),
        (execute M1 (startConfig2 k1 xs ws) T1).1 = M1.length →
        outputOf k1 (execute M1 (startConfig2 k1 xs ws) T1) (T1 + 2) = y →
        DecidesIn M2 k2 xs (boolsToSymbols y) T2 b →
        DecidesIn M k xs ws (T1 + T2) b := by
  sorry

end CookLevin

Source

Core machine construction for CookLevin.transducer_decider_pipeline_general

View graph