NP through polynomially bounded certificates

Lax988886.NondeterministicPolynomialTime · concepts/Lax988886/NondeterministicPolynomialTime.lean · lax-988886

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

1	import Lax988886.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 Lax988886.NondeterministicPolynomialTime
28
29	open Lax988886.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 Lax988886.NondeterministicPolynomialTime
43