Exact-time decision contracts are monotone after halting

Proved

CookLevin.DecidesIn_mono

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

cook-levintime-paddingturing-machine

If a machine has halted with Boolean verdict $b$ after exactly $t$ interpreter steps, then it has the same halted configuration and verdict after every later time $T\ge t$ .

This padding lemma converts exact summed-time machine constructions into larger polynomial clocks.

Formal statement

import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.DecidesIn_mono
    {M : Machine} {k : Nat} {xs ws : List Symbol}
    {t T : Nat} {b : Bool}
    (h : DecidesIn M k xs ws t b) (hle : t ≤ T) :
    DecidesIn M k xs ws T b := by sorry

Source

Existing CookLevin.decidesIn_of_le in Def_CookLevin_Reduction; used under https://prove2.me/theorems/6c12ec80

View graph