Lax Lean Archive

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

One-call reductions compose, and the one-call closure

Lax859101.OneCallClosure · concepts/Lax859101/OneCallClosure.lean · lax-859101

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

    One-call reductions compose: the post-processing term of the second is substituted for the oracle in the first, pulled back through the first interpretation. A relativized ordered parsimonious reduction is a one-call reduction with the oracle as its term. The one-call closure of a class contains the class and is closed under one-call reductions, one-call hardness travels forward along them, and one-call hardness is hardness for the whole closure. A parsimoniously #P-complete problem is one-call #P-complete.

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

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

    1 oneCall_of_relOrderedParsimonious proven

    2 oneCall_trans proven

    3 oneCallComplete_sharpP_of_parsimoniousComplete proven

    4 oneCallHard_iff proven

    5 oneCallHard_of_oneCall proven

    6 oneCallMem_of_mem proven

    7 oneCallMem_of_oneCall proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Sat
    3import Mathlib.ModelTheory.Graph
    4import Lax799700.SetFamily
    5import Lax366625.CountingProblems
    6import Lax366625.CountingClasses
    7import Lax366625.WitnessCounting
    8import Lax366625.CountingSat
    9import Lax859101.OneCallReductions
    10import Lax859101.SubtractiveReductions
    11import Lax859101.CountingDnf
    12import Lax859101.CountingNaeSat
    13import Lax859101.CountingRestrictedSat
    14import Lax859101.CountingAllSets
    15import Lax859101.CountingBipartite
    16
    17/-!
    18---
    19title: One-call reductions compose, and the one-call closure
    20type: theorem
    21---
    22One-call reductions compose: the post-processing term of the second is
    23substituted for the oracle in the first, pulled back through the first
    24interpretation. A relativized ordered parsimonious reduction is a one-call
    25reduction with the oracle as its term. The one-call closure of a class
    26contains the class and is closed under one-call reductions, one-call
    27hardness travels forward along them, and one-call hardness is hardness for
    28the whole closure. A parsimoniously #P-complete problem is one-call
    29#P-complete.
    30-/
    31
    32namespace Lax859101.OneCallClosure
    33
    34open FirstOrder FirstOrder.Language FirstOrder.Language.Structure
    35open Lax904597.Problems Lax904597.Sat Lax799700.SetFamily
    36open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
    37 Lax366625.CountingSat
    38open Lax859101.OneCallReductions Lax859101.SubtractiveReductions Lax859101.CountingDnf
    39 Lax859101.CountingNaeSat Lax859101.CountingRestrictedSat Lax859101.CountingAllSets
    40 Lax859101.CountingBipartite
    41
    42/-- One-call reductions compose. -/
    43axiom oneCall_trans :
    44 ∀ {L L' L'' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational] [L''.IsRelational]
    45 {C : CountingProblem L} {D : CountingProblem L'} {E : CountingProblem L''},
    46 Nonempty (OneCallReduction C D) → Nonempty (OneCallReduction D E) → Nonempty
    47 (OneCallReduction C E)
    48
    49/-- A relativized ordered parsimonious reduction is a one-call reduction. -/
    50axiom oneCall_of_relOrderedParsimonious :
    51 ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational] {C : CountingProblem L}
    52 {D : CountingProblem L'},
    53 Nonempty (RelOrderedParsimoniousReduction C D) → Nonempty (OneCallReduction C D)
    54
    55/-- A problem of a class is in its one-call closure. -/
    56axiom oneCallMem_of_mem :
    57 ∀ (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational] {C : CountingProblem L},
    58 K.Mem C → OneCallMem K C
    59
    60/-- The one-call closure is closed under one-call reductions. -/
    61axiom oneCallMem_of_oneCall :
    62 ∀ (K : CountingClass) {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    63 {C : CountingProblem L} {D : CountingProblem L'},
    64 Nonempty (OneCallReduction C D) → OneCallMem K D → OneCallMem K C
    65
    66/-- One-call hardness travels forward along one-call reductions. -/
    67axiom oneCallHard_of_oneCall :
    68 ∀ (K : CountingClass) {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    69 {C : CountingProblem L} {D : CountingProblem L'},
    70 Nonempty (OneCallReduction C D) → OneCallHard K C → OneCallHard K D
    71
    72/-- One-call hardness is hardness for the one-call closure. -/
    73axiom oneCallHard_iff :
    74 ∀ (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational] {C : CountingProblem L},
    75 OneCallHard K C ↔ ∀ {L'' : Language.{0, 0}} [L''.IsRelational] (D : CountingProblem L''),
    76 OneCallMem K D → Nonempty (OneCallReduction D C)
    77
    78/-- A parsimoniously #P-complete problem is one-call #P-complete. -/
    79axiom oneCallComplete_sharpP_of_parsimoniousComplete :
    80 ∀ {L : Language.{0, 0}} [L.IsRelational] {C : CountingProblem L},
    81 SharpP.ParsimoniousComplete C → OneCallComplete SharpP C
    82
    83end Lax859101.OneCallClosure
    84
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…