PolyTimeBounded
The class P over alphabet Γ consists of all languages L for which there is a polynomial p : Polynomial ℕ such that L is decidable in time n ↦ p.eval n, i.e. by a Turing machine whose running time on inputs of length n is bounded by p(n).
Statement
def PolyTimeBounded (Γ : Type) (L : Language Γ) : Prop
- Source
- Arora & Barak, Def. 1.4 (P = ∪_c DTIME(n^c)); Sipser, Def. 7.12; Papadimitriou, Def. 2.1 (class P)
- Verified
- 10 Sep 2026
- Axioms
- none listed
- 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
The declaration defines the predicate PolyTimeBounded on an alphabet type Γ and a language L : Language Γ. For any such Γ and L, PolyTimeBounded Γ L holds exactly when there exists a univariate polynomial p over the natural numbers such that L is TimeBounded with time bound T(n) := p.eval n.
Unfolding TimeBounded, this means: there exists a Boolean-valued function f : List Γ → Bool such that (1) there exists a Turing-machine/time certificate M of type Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f whose time function satisfies M.time n ≤ p.eval n for every natural number n, and (2) for every word w : List Γ, w ∈ L if and only if f w = true.
The quantifier structure is ∃ p, ∃ f, (∃ M, ∀ n, ...) ∧ (∀ w, ...): a single polynomial p and a single Boolean function f are chosen first; then there is a machine witness M whose time is bounded pointwise by p.eval at every n; and f is exactly the characteristic function of L. The bound is non-strict (≤). The alphabet Γ is an arbitrary Type; no finiteness or decidable-equality hypothesis appears. The declaration is a definition, not a theorem asserting that any particular language is polynomial-time.
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
/-- The complexity class P over the alphabet Γ: languages decidable in polynomial time. -/ def PolyTimeBounded (Γ : Type) (L : Language Γ) : Prop := ∃ p : Polynomial ℕ, TimeBounded Γ (fun n => p.eval n) L