Lax Lean Archive

NP is a complexity class

Lax904597.NPClass · concepts/Lax904597/NPClass.lean · lax-904597

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    The library this submission comes from makes closure under reductions part of the definition of a complexity class; these are the closure facts for NP, and for cofinal hardness in general. Membership in NP travels backward along first-order and ordered first-order reductions and depends only on the finite instances of a problem. Cofinal hardness, for any membership predicate, travels forward along first-order, ordered and relativized ordered reductions and depends only on finite instances.

    Finally, cofinal hardness is the usual notion: PP is cofinally hard for a collection exactly when every problem of the collection reduces to PP.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

    1 cofinalHard_congr proven

    2 cofinalHard_iff proven

    3 cofinalHard_of_foReduction proven

    4 cofinalHard_of_orderedReduction proven

    5 cofinalHard_of_relOrderedReduction proven

    6 NP_mem_congr_finite proven

    7 NP_mem_of_foReduction proven

    8 NP_mem_of_orderedReduction proven

    Lean source view on GitHub

    1import Lax904597.Classes
    2
    3/-!
    4---
    5title: NP is a complexity class
    6type: theorem
    7---
    8The library this submission comes from makes closure under reductions part
    9of the definition of a complexity class; these are the closure facts for
    10NP, and for cofinal hardness in general. Membership in NP travels backward
    11along first-order and ordered first-order reductions and depends only on
    12the finite instances of a problem. Cofinal hardness, for any membership
    13predicate, travels forward along first-order, ordered and relativized
    14ordered reductions and depends only on finite instances.
    15
    16Finally, cofinal hardness is the usual notion: PP is cofinally hard for a
    17collection exactly when every problem of the collection reduces to PP.
    18-/
    19
    20namespace Lax904597.NPClass
    21
    22open FirstOrder FirstOrder.Language
    23open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder
    24 Lax904597.Classes
    25
    26/-- Membership in NP travels backward along first-order reductions. -/
    27axiom NP_mem_of_foReduction : ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    28 {P : DecisionProblem L} {Q : DecisionProblem L'}, FOReduction P Q → NP.Mem Q → NP.Mem P
    29
    30/-- Membership in NP travels backward along ordered first-order reductions. -/
    31axiom NP_mem_of_orderedReduction : ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    32 {P : DecisionProblem L} {Q : DecisionProblem L'}, OrderedFOReduction P Q → NP.Mem Q → NP.Mem P
    33
    34/-- Membership in NP depends only on the finite instances of a problem. -/
    35axiom NP_mem_congr_finite : ∀ {L : Language.{0, 0}} [L.IsRelational] {P Q : DecisionProblem L},
    36 (∀ (A : Type) [L.Structure A] [Finite A], P A ↔ Q A) → (NP.Mem P ↔ NP.Mem Q)
    37
    38/-- Cofinal hardness travels forward along first-order reductions. -/
    39axiom cofinalHard_of_foReduction :
    40 ∀ {Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], DecisionProblem L₀ → Prop}
    41 {L₁ L₂ : Language.{0, 0}} [L₁.IsRelational] [L₂.IsRelational]
    42 {P : DecisionProblem L₁} {Q : DecisionProblem L₂},
    43 FOReduction P Q → CofinalHard Mem P → CofinalHard Mem Q
    44
    45/-- Cofinal hardness travels forward along ordered first-order reductions. -/
    46axiom cofinalHard_of_orderedReduction :
    47 ∀ {Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], DecisionProblem L₀ → Prop}
    48 {L₁ L₂ : Language.{0, 0}} [L₁.IsRelational] [L₂.IsRelational]
    49 {P : DecisionProblem L₁} {Q : DecisionProblem L₂},
    50 OrderedFOReduction P Q → CofinalHard Mem P → CofinalHard Mem Q
    51
    52/-- Cofinal hardness travels forward along relativized ordered first-order
    53reductions. -/
    54axiom cofinalHard_of_relOrderedReduction :
    55 ∀ {Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], DecisionProblem L₀ → Prop}
    56 {L₁ L₂ : Language.{0, 0}} [L₁.IsRelational] [L₂.IsRelational]
    57 {P : DecisionProblem L₁} {Q : DecisionProblem L₂},
    58 RelOrderedFOReduction P Q → CofinalHard Mem P → CofinalHard Mem Q
    59
    60/-- Cofinal hardness depends only on the finite instances of a problem. -/
    61axiom cofinalHard_congr :
    62 ∀ {Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], DecisionProblem L₀ → Prop}
    63 {L₁ : Language.{0, 0}} [L₁.IsRelational] {P P' : DecisionProblem L₁},
    64 (∀ (A : Type) [L₁.Structure A] [Finite A], P A ↔ P' A) →
    65 CofinalHard Mem P → CofinalHard Mem P'
    66
    67/-- Over a relational vocabulary, cofinal hardness is the usual notion: every
    68problem of the collection reduces to `P`. -/
    69axiom cofinalHard_iff : ∀ {L : Language.{0, 0}} [L.IsRelational]
    70 (Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], DecisionProblem L₀ → Prop)
    71 (P : DecisionProblem L),
    72 CofinalHard Mem P ↔
    73 ∀ {L'' : Language.{0, 0}} [L''.IsRelational] (Q : DecisionProblem L''),
    74 Mem Q → Nonempty (RelOrderedFOReduction Q P)
    75
    76end Lax904597.NPClass
    77
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…