time_bounded_mono

theoremverified

If T and T' are time bounds with T n ≤ T' n for every n, then every language decidable in time T is decidable in time T'.

Statement

theorem time_bounded_mono {Γ : Type} {T T' : ℕ → ℕ} (h : ∀ n, T n ≤ T' n) {L : Language Γ}
    (hL : TimeBounded Γ T L) : TimeBounded Γ T' L

Source

Sipser, Sec. 7.1 (DTIME is monotone in the time bound); folklore

Verified

10 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 1

TimeBoundedA language L over an alphabet Γ is decidable in time T (T : ℕ → ℕ) if there is a total decider f : List Γ → Bool together with a Turing…

Used by 1

poly_time_subset_exp_timeEvery language in P is in EXP: if L is decidable in time p(n) for a polynomial p, then L is decidable in time 2^(p(n)).

Read back from the Lean

For every type Γ, every pair of functions T, T' : ℕ → ℕ, and every language L over Γ, if (h) for every natural number n, T n ≤ T' n, and if (hL) L is TimeBounded with time bound T, then L is TimeBounded with time bound T'. In explicit quantifier order: for all Γ, for all T T' : ℕ → ℕ, if ∀ n, T n ≤ T' n, then for all L : Language Γ, TimeBounded Γ T L implies TimeBounded Γ T' L. The theorem thus asserts monotonicity of the predicate TimeBounded in its time-bound argument: pointwise increasing the allowed time bound preserves time-boundedness of a language. There is no finiteness assumption on Γ, and T and T' are arbitrary functions ℕ → ℕ.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- Time-bounded decidability is monotone in the time bound. -/
theorem time_bounded_mono {Γ : Type} {T T' : ℕ → ℕ} (h : ∀ n, T n ≤ T' n) {L : Language Γ}
    (hL : TimeBounded Γ T L) : TimeBounded Γ T' L := by
  rcases hL with ⟨f, ⟨M, hM⟩, hf⟩
  exact ⟨f, ⟨M, fun n => le_trans (hM n) (h n)⟩, hf⟩

Discuss this result Challenge it