A deterministic computation has a unique verdict

Proved

CookLevin.DecidesIn_verdict_unique

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

cook-levindeterminismturing-machine

If the same deterministic machine, initial configuration, and exact running time satisfy the decision contract with two Boolean verdicts $b_1$ and $b_2$ , then $b_1=b_2$ .

This is the functionality principle for the designated verdict cell and is reusable when auditing machine contracts.

Formal statement

import Definitions.Def_CookLevin_Cost
open CookLevin

theorem CookLevin.DecidesIn_verdict_unique
    {M : Machine} {k : Nat} {xs ws : List Symbol}
    {t : Nat} {b₁ b₂ : Bool}
    (h₁ : DecidesIn M k xs ws t b₁)
    (h₂ : DecidesIn M k xs ws t b₂) :
    b₁ = b₂ := by sorry

Source

Immediate consequence of the definition of DecidesIn in CookLevin_Cost; used in analysis of https://prove2.me/theorems/48716741-a120-417c-84e7-c6ce080b0f98

View graph