poly_time_subset_exp_time
Every 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)).
Statement
theorem poly_time_subset_exp_time {Γ : Type} {L : Language Γ} (h : PolyTimeBounded Γ L) : ExpTimeBounded Γ L
- Source
- Arora & Barak, Sec. 1.2 (P ⊆ EXP, indeed DTIME(n^c) ⊆ DTIME(2^(n^c))); Sipser, Ex. 7.13
- Verified
- 10 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 4
- 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…
- PolyTimeBoundedThe class P over alphabet Γ consists of all languages L for which there is a polynomial p : Polynomial ℕ such that L is decidable in time…
- ExpTimeBoundedThe class EXP over alphabet Γ consists of all languages L for which there is a polynomial p such that L is decidable in time n ↦ 2 ^…
- time_bounded_monoIf 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'.
Read back from the Lean
For an arbitrary type Γ (no finiteness or decidability assumed) and an arbitrary language L over Γ, if L is polynomial-time bounded — i.e. there exists a polynomial p : Polynomial ℕ and a Boolean-valued decision function f : List Γ → Bool such that (a) f is computed by some Turing machine M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f whose running time satisfies M.time n ≤ p.eval n for every n : ℕ, and (b) w ∈ L ↔ f w = true for every w — then L is exponential-time bounded — i.e. there exists a polynomial q : Polynomial ℕ and a Boolean-valued g : List Γ → Bool computed by some machine M' with M'.time n ≤ 2 ^ (q.eval n) for every n : ℕ, and w ∈ L ↔ g w = true for every w. Both the hypothesis and the conclusion are quantified over the fixed Γ and L (they are parameters, not universally quantified inside the statement). The two polynomials p and q are independent of each other; the conclusion does not require q = p, only that some polynomial bound of the form 2^(q.eval n) suffices. The time bound is non-strict (≤) and required for all n : ℕ, not merely infinitely many.
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
/-- P is contained in EXP. -/ theorem poly_time_subset_exp_time {Γ : Type} {L : Language Γ} (h : PolyTimeBounded Γ L) : ExpTimeBounded Γ L := by obtain ⟨p, hp⟩ := h exact ⟨p, time_bounded_mono (fun n => (p.eval n).lt_two_pow_self.le) hp⟩