Runtime extension preserves Turing machine decision verdict

Proved

CookLevin.decidesIn_time_add

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

cost-modeldecidesininvarianceruntime-extensionturing-machine

If a multi-tape Turing machine $M$ with $k$ tapes decides a verdict $b \in \mathbb{B}$ on input strings $(xs, ws)$ within $t_1$ steps, then running $M$ for any additional $t_2$ steps preserves the exact same halting state and verdict bit:

\mathrm{DecidesIn}(M, k, xs, ws, t_1, b) \implies \mathrm{DecidesIn}(M, k, xs, ws, t_1 + t_2, b).

Because $M$ halts at or before step $t_1$ , the configuration reached at step $t_1$ is in the halting state $M.\mathrm{length}$ . By execute_of_halted_le, any subsequent execution steps leave the state and all tape contents completely unchanged. In particular, the verdict tape cell 1 continues to hold $\mathrm{boolSym}(b)$ at step $t_1 + t_2$ .

This is a foundational invariance lemma for the cost model of multi-tape Turing machines.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem decidesIn_time_add (M : Machine) (k : Nat) (xs ws : List Symbol) (t1 t2 : Nat) (b : Bool)
    (h : DecidesIn M k xs ws t1 b) :
    DecidesIn M k xs ws (t1 + t2) b := by sorry
end CookLevin

Source

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

View graph