NondeterministicPolyTimeBounded

def

A language L over Γ is in NP in verifier form if there are a polynomial p and a language V of words over Γ ⊕ Unit such that V is decidable in time n ↦ p.eval n and, for every word w, w ∈ L holds if and only if there exists a certificate word c over Γ with c.length ≤ p (w.length) and pairEncode w c ∈ V.

Statement

def NondeterministicPolyTimeBounded (Γ : Type) (L : Language Γ) : Prop

Source

Arora & Barak, Def. 2.2 (L ∈ NP iff there is a poly-time V and polynomial p with w ∈ L ↔ ∃ c, |c| ≤ p(|w|) and (w,c) ∈ V); Sipser, Def. 7.16/Thm. 7.20 (equivalence of verifier and nondeterministic-machine definitions)

Verified

10 Sep 2026

Axioms

none listed

Built on 2

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…
pairEncodeFor words w and c over an alphabet Γ, pairEncode w c is the word over Γ ⊕ Unit obtained by writing w, then the single separator symbol…

Used by 1

NPHardA language L over an alphabet Γ is NP-hard if every language L' that is in NP Karp-reduces to L, the languages L' ranging over all…

Read back from the Lean

For a type of symbols Γ and a language L over Γ (i.e. a predicate/set of lists List Γ), NondeterministicPolyTimeBounded Γ L asserts: There exist * a polynomial p : Polynomial ℕ, and * a "verifier" language V over the alphabet Γ ⊕ Unit (i.e. V ⊆ List (Γ ⊕ Unit)), such that BOTH of the following hold: 1. **The verifier is time-bounded by p.** V is decided by a Boolean function f : List (Γ ⊕ Unit) → Bool for which there is a TM2ComputableInTime machine computing Computability.encodeBool f (with identity input/output map) whose running time on inputs of length n is at most p.eval n for every n; and f is correct for V, i.e. for every list w' over Γ ⊕ Unit, w' ∈ V ↔ f w' = true. 2. **L is witnessed by short certificates accepted by V.** For every word w : List Γ: w ∈ L if and only if there exists a certificate c : List Γ with c.length ≤ p.eval w.length (the certificate is short, bounded by p evaluated at the length of w) and such that the encoding pairEncode w c ∈ V, where pairEncode w c is the list over Γ ⊕ Unit obtained by writing w with each symbol wrapped in Sum.inl, then one separator Sum.inr (), then c with each symbol wrapped in Sum.inl. So the declaration says: L is in (nondeterministic) polynomial time — there is a single polynomial p, and a verifier over Γ plus a distinguished separator symbol, running in time p, such that membership of w in L is equivalent to the existence of a certificate c of length at most p(|w|) for which the encoded pair (w, c) is accepted by the verifier. This is a definition (a def), not a theorem, and it introduces no hypotheses of its own beyond its two explicit arguments.

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 class NP in verifier form: membership is witnessed by a polynomially bounded certificate checked in polynomial time. -/
def NondeterministicPolyTimeBounded (Γ : Type) (L : Language Γ) : Prop := ∃ (p : Polynomial ℕ) (V : Language (Γ ⊕ Unit)),
    TimeBounded (Γ ⊕ Unit) (fun n => p.eval n) V ∧
      ∀ w : List Γ, w ∈ L ↔ ∃ c : List Γ, c.length ≤ p.eval w.length ∧ pairEncode w c ∈ V

Discuss this result Challenge it