Lax Lean Archive

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

⊕SAT and Mod_k-SAT are complete

Lax175070.ParitySatComplete · concepts/Lax175070/ParitySatComplete.lean · lax-175070

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

    ⊕SAT is ⊕P-complete and Modk_k-SAT is Modk_kP-complete. More generally, the parity, and the residue modulo kk, of every parsimoniously #P-complete counting problem are complete for ⊕P and Modk_kP: a parsimonious reduction preserves every property of the count. And a problem is in ⊕P, or in Modk_kP, exactly when it reduces by an ordered first-order reduction to the parity, or the residue, of the number of accepting runs of a nondeterministic Turing machine.

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

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

    1 mem_modP_iff_le_mod_sharpNtmAccept proven

    2 mem_parityP_iff_le_parity_sharpNtmAccept proven

    3 modP_complete_of_sharpP_parsimoniousComplete proven

    4 modSat_modP_complete proven

    5 parityP_complete_of_sharpP_parsimoniousComplete proven

    6 paritySat_parityP_complete proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax485149.Problems
    3import Lax485149.Complement
    4import Lax904597.Classes
    5import Lax904597.Sat
    6import Lax904597.Interpretations
    7import Lax904597.Machines
    8import Lax564036.Hierarchy
    9import Lax366625.CountingProblems
    10import Lax366625.CountingClasses
    11import Lax366625.WitnessCounting
    12import Lax366625.CountingSat
    13import Lax366625.CountingRuns
    14import Lax175070.CountDefinability
    15import Lax175070.SelectedSat
    16
    17/-!
    18---
    19title: ⊕SAT and Mod_k-SAT are complete
    20type: theorem
    21---
    22⊕SAT is ⊕P-complete and Modk_k-SAT is Modk_kP-complete. More generally,
    23the parity, and the residue modulo kk, of every parsimoniously #P-complete
    24counting problem are complete for ⊕P and Modk_kP: a parsimonious reduction
    25preserves every property of the count. And a problem is in ⊕P, or in
    26Modk_kP, exactly when it reduces by an ordered first-order reduction to the
    27parity, or the residue, of the number of accepting runs of a
    28nondeterministic Turing machine.
    29-/
    30
    31namespace Lax175070.ParitySatComplete
    32
    33open FirstOrder FirstOrder.Language
    34open Lax904597.Problems Lax904597.Classes Lax904597.Sat Lax904597.Interpretations
    35 Lax904597.Machines Lax564036.Hierarchy
    36open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
    37 Lax366625.CountingSat
    38open Lax366625.CountingRuns Lax175070.CountDefinability Lax175070.SelectedSat Lax485149.Problems
    39open Lax485149.Complement
    40
    41/-- ⊕SAT is ⊕P-complete. -/
    42axiom paritySat_parityP_complete :
    43 ParityP.Complete ParitySAT
    44
    45/-- Mod_k-SAT is Mod_k P-complete. -/
    46axiom modSat_modP_complete :
    47 ∀ (k : ℕ), (ModP k).Complete (ModSAT k)
    48
    49/-- The parity of a parsimoniously #P-complete problem is ⊕P-complete. -/
    50axiom parityP_complete_of_sharpP_parsimoniousComplete :
    51 ∀ {L : Language.{0, 0}} [L.IsRelational] {C : CountingProblem L},
    52 SharpP.ParsimoniousComplete C → ParityP.Complete (decide Odd C)
    53
    54/-- The residue modulo `k` of a parsimoniously #P-complete problem is Mod_k P-complete. -/
    55axiom modP_complete_of_sharpP_parsimoniousComplete :
    56 ∀ {L : Language.{0, 0}} [L.IsRelational] (k : ℕ) {C : CountingProblem L},
    57 SharpP.ParsimoniousComplete C → (ModP k).Complete (decide (fun c => ¬ k ∣ c) C)
    58
    59/-- ⊕P is reducibility to the parity of the number of accepting runs. -/
    60axiom mem_parityP_iff_le_parity_sharpNtmAccept :
    61 ∀ {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L),
    62 ParityP.Mem P ↔ Nonempty (OrderedFOReduction P (decide Odd SharpNTMAccept))
    63
    64/-- Mod_k P is reducibility to the residue of the number of accepting runs. -/
    65axiom mem_modP_iff_le_mod_sharpNtmAccept :
    66 ∀ {L : Language.{0, 0}} [L.IsRelational] (k : ℕ) (P : DecisionProblem L),
    67 (ModP k).Mem P ↔ Nonempty (OrderedFOReduction P (decide (fun c => ¬ k ∣ c) SharpNTMAccept))
    68
    69end Lax175070.ParitySatComplete
    70
    Show 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…