Uniqueness of Turing machine decision verdict

Proved

CookLevin.decidesIn_unique

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

cost-modeldecidesindeterminismturing-machineuniqueness

Every multi-tape Turing machine $M$ is deterministic, so its decision verdict on a fixed input $(xs, ws)$ at a fixed step count $t$ is unique:

\mathrm{DecidesIn}(M, k, xs, ws, t, b_1) \wedge \mathrm{DecidesIn}(M, k, xs, ws, t, b_2) \implies b_1 = b_2.

By definition of $\mathrm{DecidesIn}$ , the symbol in cell 1 of the verdict tape $k - 1$ at step $t$ equals both $\mathrm{boolSym}(b_1)$ and $\mathrm{boolSym}(b_2)$ . Since $\mathrm{boolSym}(\mathrm{true}) = \mathbf{1}$ and $\mathrm{boolSym}(\mathrm{false}) = \mathbf{0}$ are distinct symbols ( $3 \ne 2$ ), the map $\mathrm{boolSym}$ is injective, concluding $b_1 = b_2$ .

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem decidesIn_unique (M : Machine) (k : Nat) (xs ws : List Symbol) (t : Nat) (b1 b2 : Bool)
    (h1 : DecidesIn M k xs ws t b1) (h2 : DecidesIn M k xs ws t b2) :
    b1 = b2 := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Cost.lean#L99

View graph