Lax678846.NondeterministicPolynomialTime
NP through polynomially bounded certificates
concepts/Lax678846/NondeterministicPolynomialTime.lean · lax-678846
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
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.
Lean source view on GitHub
| 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 |
Builds on
Used by
From Mathlib
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments