Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Counting classes

Lax366625.CountingClasses · concepts/Lax366625/CountingClasses.lean · lax-366625

definition

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

    Definition

    A counting class is given by a membership predicate and a hardness predicate on counting problems over arbitrary relational vocabularies. The classes of this submission are built from their membership predicate: a problem CC is parsimoniously hard for the class when every member of the class reduces to CC by a relativized ordered parsimonious reduction, and parsimoniously complete when it is moreover a member.

    Concept map
    5 concepts; 14 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax366625.CountingProblems
    3
    4/-!
    5---
    6title: Counting classes
    7type: definition
    8---
    9A counting class is given by a membership predicate and a hardness predicate
    10on counting problems over arbitrary relational vocabularies. The classes of
    11this submission are built from their membership predicate: a problem CC is
    12parsimoniously hard for the class when every member of the class reduces to
    13CC by a relativized ordered parsimonious reduction, and parsimoniously
    14complete when it is moreover a member.
    15-/
    16
    17namespace Lax366625.CountingClasses
    18
    19open FirstOrder FirstOrder.Language
    20open Lax904597.Problems Lax366625.CountingProblems
    21
    22/-- A counting class: a membership predicate and a hardness predicate on
    23counting problems, over arbitrary relational vocabularies. -/
    24structure CountingClass where
    25 /-- The counting problems belonging to the class. -/
    26 Mem : ∀ {L : Language.{0, 0}} [L.IsRelational], CountingProblem L → Prop
    27 /-- The counting problems every problem of the class reduces to. -/
    28 ParsimoniousHard : ∀ {L : Language.{0, 0}} [L.IsRelational], CountingProblem L → Prop
    29
    30/-- The class with the given membership, a problem being hard when every member
    31reduces to it by a relativized ordered parsimonious reduction. -/
    32def CountingClass.ofMem
    33 (Mem : ∀ {L₀ : Language.{0, 0}} [L₀.IsRelational], CountingProblem L₀ → Prop) :
    34 CountingClass where
    35 Mem C := Mem C
    36 ParsimoniousHard C := ∀ {L'' : Language.{0, 0}} [L''.IsRelational] (D : CountingProblem L''),
    37 Mem D → Nonempty (RelOrderedParsimoniousReduction D C)
    38
    39/-- A counting problem is parsimoniously complete for a class when it belongs
    40to it and is parsimoniously hard for it. -/
    41def CountingClass.ParsimoniousComplete (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational]
    42 (C : CountingProblem L) : Prop :=
    43 K.Mem C ∧ K.ParsimoniousHard C
    44
    45end Lax366625.CountingClasses
    46
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…