ComputesInTime invariance under arbitrary certificate tape contents

Disproved

CookLevin.computesInTime_ignore_certificate

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

computesintimecost-modelinvarianceturing-machine

Let $M$ be a multi-tape Turing machine computing function $f$ within time bound $T(n)$ on unary input $(x, \varepsilon)$ as characterized by $\mathrm{ComputesInTime}(M, k, T, f)$ . If $M$ leaves the certificate tape 1 unread during its execution, then running $M$ on configuration $\mathrm{startConfig2}(k, x, w)$ with arbitrary certificate $w$ produces the exact same output $f(x)$ within $T(|x|)$ steps:

\forall x, w,\; \mathrm{outputOf}(k, \mathrm{execute}(M, \mathrm{startConfig2}(k, x, w), T(|x|))) = f(x).

This lifting lemma allows transferring time-bounded function computability results established on single-input machines to the two-input verifier machine format.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem computesInTime_ignore_certificate
    (f : List Bool → List Bool) (T : Nat → Nat)
    (M : Machine) (k G : Nat) (hwf : TuringMachine k G M)
    (hcomp : ComputesInTime M k T f) :
    ∀ x w : List Bool,
      (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w)) (T x.length)).1 = M.length ∧
      outputOf k (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w)) (T x.length)) (T x.length + 2) = f x := by sorry
end CookLevin

Source

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

View graph