Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

NP through polynomially bounded certificates

Lax678846.NondeterministicPolynomialTime · concepts/Lax678846/NondeterministicPolynomialTime.lean · lax-678846

definition

Loading review…

Natural Language Statement

Definition

A bit-string language belongs to NP if membership is equivalent to the existence of a certificate of polynomially bounded length accepted by a deterministic polynomial-time verifier. This is the usual certificate definition of NP. The verifier is a concrete finite multi-stack Turing machine in mathlib, with its machine-step polynomial bound.

The verifier reads a pair of bit strings: the input and the certificate. Each input bit is preceded by a one-bit; a zero-bit terminates the input, and the remaining bits form the certificate. This uniquely decodable pair encoding has length twice the input length plus the certificate length plus one. Runtime is polynomial in this total length; certificate length is bounded by a polynomial in the original input length.

A property belongs to NP when its language of structure encodings does. The language excludes malformed encodings. No logical definability or simulation theorem occurs in this definition.

Concept map

4 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax678846.FiniteStructures
2	import Mathlib.Computability.TuringMachine.Computable
3
4	/-!
5	---
6	title: NP through polynomially bounded certificates
7	type: definition
8	---
9	A bit-string language belongs to NP if membership is equivalent to the
10	existence of a certificate of polynomially bounded length accepted by a
11	deterministic polynomial-time verifier. This is the usual certificate
12	definition of NP. The verifier is a concrete finite multi-stack Turing
13	machine in mathlib, with its machine-step polynomial bound.
14
15	The verifier reads a pair of bit strings: the input and the certificate.
16	Each input bit is preceded by a one-bit; a zero-bit terminates the input,
17	and the remaining bits form the certificate. This uniquely decodable
18	pair encoding has length twice the input length plus the certificate
19	length plus one. Runtime is polynomial in this total length; certificate
20	length is bounded by a polynomial in the original input length.
21
22	A property belongs to NP when its language of structure encodings does.
23	The language excludes malformed encodings. No logical definability or
24	simulation theorem occurs in this definition.
25	-/
26
27	namespace Lax678846.NondeterministicPolynomialTime
28
29	open Lax678846.FiniteStructures
30
31	def encodePair (p : List Bool × List Bool) : List Bool :=
32	p.1.flatMap (fun b => [true, b]) ++ false :: p.2
33
34	def LanguageInNP (L : List Bool → Prop) : Prop :=
35	∃ (V : List Bool × List Bool → Bool) (p : Polynomial Nat),
36	Nonempty (Turing.TM2ComputableInPolyTime encodePair (fun b => [b]) V) ∧
37	∀ w, L w ↔ ∃ c : List Bool, c.length ≤ p.eval w.length ∧ V (w, c) = true
38
39	def InNP {σ : Vocabulary} (Q : Property σ) : Prop :=
40	LanguageInNP (language Q)
41
42	end Lax678846.NondeterministicPolynomialTime
43