Cook–Levin output: bounded bit prefix and terminating cell

Proved

CookLevin.computesInTime_output_spec

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

complexity-theorycook-levinturing-machines

For every well-formed machine computing f within T, the output f(x) has length at most T(|x|). Each output cell j+1 contains the encoding of the corresponding bit f(x)[j], and the following cell is a non-bit symbol. Every decoding fuel strictly greater than T(|x|) returns the same f(x). These are properties of the actual output tape after execution, not assumptions about a normalized tape representation.

Preamble

import Definitions.Def_CookLevin_Cost
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.computesInTime_output_spec {k G : Nat} (M : Machine)
    (hM : TuringMachine k G M) (T : Nat → Nat) (f : List Bool → List Bool)
    (hcomp : ComputesInTime M k T f) (x : List Bool) :
    let cfg := execute M (startConfig2 k (boolsToSymbols x) []) (T x.length)
    (f x).length ≤ T x.length ∧
      (∀ j, (hj : j < (f x).length) →
        tapeFun cfg (verdictTape k) (j + 1) = boolSym ((f x)[j])) ∧
      symBool? (tapeFun cfg (verdictTape k) ((f x).length + 1)) = none ∧
      ∀ fuel, T x.length < fuel → outputOf k cfg fuel = f x := by sorry

Source

Direct proofs from the CookLevin Basic and Cost execution semantics, developed for output concatenation in the polynomial-time SAT reduction.

View graph