Lax Lean Archive

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

The degree of a problem

Lax604544.Degrees · concepts/Lax604544/Degrees.lean · lax-604544

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

    The degree of a decision problem Q0Q_0 is the class of the problems that reduce to Q0Q_0 by an ordered first-order reduction, with the cofinal hardness of the NP core. It is a complexity class defined by no logic and no machine, only by a problem: a problem is complete for the degree of Q0Q_0 when it has, under first-order reductions, exactly the difficulty of Q0Q_0.

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

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Interpretations
    3import Lax904597.Classes
    4
    5/-!
    6---
    7title: The degree of a problem
    8type: definition
    9---
    10The degree of a decision problem Q0Q_0 is the class of the problems that
    11reduce to Q0Q_0 by an ordered first-order reduction, with the cofinal
    12hardness of the NP core. It is a complexity class defined by no logic and no
    13machine, only by a problem: a problem is complete for the degree of Q0Q_0
    14when it has, under first-order reductions, exactly the difficulty of
    15Q0Q_0.
    16-/
    17
    18namespace Lax604544.Degrees
    19
    20open FirstOrder FirstOrder.Language
    21open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes
    22
    23/-- **The degree of a problem**: the problems that ordered first-order reduce
    24to `Q₀`, as a complexity class with cofinal hardness. -/
    25def below {L₀ : Language.{0, 0}} [L₀.IsRelational] (Q₀ : DecisionProblem L₀) : ComplexityClass :=
    26 ComplexityClass.ofMem fun P => Nonempty (OrderedFOReduction P Q₀)
    27
    28end Lax604544.Degrees
    29
    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…