Cook–Levin computation: monotonicity of runtime bounds
ProvedCookLevin.computesInTime_monocomplexity-theorycook-levinturing-machines
For a well-formed machine, ComputesInTime M k T f remains true when T is replaced by any pointwise larger bound S. The result preserves the original function f under the model’s larger output-decoding fuel S(|x|)+2.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.computesInTime_mono {k G : Nat} (M : Machine) (hM : TuringMachine k G M)
(T S : Nat → Nat) (f : List Bool → List Bool)
(hcomp : ComputesInTime M k T f) (hTS : ∀ n, T n ≤ S n) :
ComputesInTime M k S f := by sorrySource
Direct proofs from the CookLevin Basic and Cost execution semantics, developed for output concatenation in the polynomial-time SAT reduction.