Documentation

CslibFrontier.Computability.Complexity.Classes.CeqP

Exact counting: C=P #

CeqP consists of zero sets of GapP functions, the gap characterization of C=P Fenner, Fortnow and Kurtz. These are verifier-based counts; no counting machine characterization is assumed.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.CeqP {α : Type} (enc : α ↪ List Bool) :
Set (Set α)

C=P, the zero sets of integer-valued GapP functions Fenner, Fortnow and Kurtz, Fortnow, Classification 4.5.

Instances For
    source
    theorem Cslib.Complexity.mem_CeqP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ CeqP enc ↔ ∃ g ∈ GapP enc, ∀ (a : α), a ∈ A ↔ g a = 0
    source
    theorem Cslib.Complexity.mem_CeqP_iff_exists_SharpP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ CeqP enc ↔ ∃ f ∈ SharpP enc, ∃ g ∈ SharpP enc, ∀ (a : α), a ∈ A ↔ f a = g a

    A language is in C=P iff membership is equality of two accepting counts.

    source
    theorem Cslib.Complexity.coNP_subset_CeqP {α : Type} {enc : α ↪ List Bool} :
    coNP enc ⊆ CeqP enc

    A coNP language is the zero set of the accepting count for its complement.

    source
    theorem Cslib.Complexity.union_mem_CeqP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ CeqP enc) (hB : B ∈ CeqP enc) :
    A ∪ B ∈ CeqP enc

    A product vanishes exactly when one of its factors vanishes.

    source
    theorem Cslib.Complexity.inter_mem_CeqP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ CeqP enc) (hB : B ∈ CeqP enc) :
    A ∩ B ∈ CeqP enc

    A sum of two integer squares vanishes exactly when both vanish.

    source
    theorem Cslib.Complexity.CeqP_subset_PP {α : Type} {enc : α ↪ List Bool} :
    CeqP enc ⊆ PP enc

    C=P ⊆ PP Fortnow, Corollary 4.13: for integer g, the gap 1 - g² is positive precisely at its zeros.

    source
    theorem Cslib.Complexity.PolyTimeReducible.mem_CeqP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ CeqP encB) :
    A ∈ CeqP enc

    C=P is closed under polynomial-time many-one reductions.

    source
    def Cslib.Complexity.coCeqP {α : Type} (enc : α ↪ List Bool) :
    Set (Set α)

    The complement class coC=P. See Fortnow, Classifications 4.8–4.9.

    Instances For
      source
      theorem Cslib.Complexity.mem_coCeqP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ coCeqP enc ↔ Aᶜ ∈ CeqP enc
      source
      @[simp]
      theorem Cslib.Complexity.compl_mem_coCeqP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      Aᶜ ∈ coCeqP enc ↔ A ∈ CeqP enc
      source
      theorem Cslib.Complexity.mem_coCeqP_iff_exists_GapP {α : Type} {enc : α ↪ List Bool} {A : Set α} :
      A ∈ coCeqP enc ↔ ∃ g ∈ GapP enc, ∀ (a : α), a ∈ A ↔ g a ≠ 0

      coC=P consists of the nonzero sets of GapP functions. This is the complement of the zero-set characterization Fortnow, Classifications 4.5 and 4.9.

      source
      theorem Cslib.Complexity.NP_subset_coCeqP {α : Type} {enc : α ↪ List Bool} :
      NP enc ⊆ coCeqP enc

      NP is contained in coC=P Fortnow, Corollary 4.11.

      source
      theorem Cslib.Complexity.coCeqP_subset_PP {α : Type} {enc : α ↪ List Bool} :
      coCeqP enc ⊆ PP enc

      coC=P is contained in PP Fortnow, Corollary 4.10.

      source
      theorem Cslib.Complexity.union_mem_coCeqP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coCeqP enc) (hB : B ∈ coCeqP enc) :
      A ∪ B ∈ coCeqP enc

      Union closure is dual to intersection closure of C=P.

      source
      theorem Cslib.Complexity.inter_mem_coCeqP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coCeqP enc) (hB : B ∈ coCeqP enc) :
      A ∩ B ∈ coCeqP enc

      Intersection closure is dual to union closure of C=P.

      source
      theorem Cslib.Complexity.PolyTimeReducible.mem_coCeqP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ coCeqP encB) :
      A ∈ coCeqP enc

      Polynomial-time reductions preserve coC=P.