#P is closed under parsimonious reductions
Lax366625.SharpPClosure · concepts/Lax366625/SharpPClosure.lean · lax-366625
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Membership in #P travels backward along ordered parsimonious reductions and along relativized ordered parsimonious reductions: if a counting problem reduces to a problem of #P, it is in #P. The witnesses of the target, pulled back along the interpretation, are witnesses of the source; for a relativized reduction, the kernel pins the pulled relations to the definable domain, which makes the correspondence of witnesses a bijection. Membership reads a problem on its finite instances only.
Concept map
Evidence
This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.
1 SharpP_mem_congr_finite proven
2 SharpP_mem_of_orderedParsimonious proven
3 SharpP_mem_of_relOrderedParsimonious proven
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | import Lax904597.Interpretations |
| 3 | import Lax904597.Relativized |
| 4 | import Lax904597.SecondOrder |
| 5 | import Lax904597.Classes |
| 6 | import Lax904597.Sat |
| 7 | import Lax904597.Machines |
| 8 | import Lax535992.HornSat |
| 9 | import Lax535992.CircuitValue |
| 10 | import Lax535992.DeterministicMachines |
| 11 | import Lax535992.ClassPTIME |
| 12 | import Lax366625.CountingProblems |
| 13 | import Lax366625.CountingClasses |
| 14 | import Lax366625.WitnessCounting |
| 15 | import Lax366625.SecondOrderCounting |
| 16 | import Lax366625.QuantitativeLogic |
| 17 | import Lax366625.CountingSat |
| 18 | import Lax366625.MachineNumbers |
| 19 | import Lax366625.CountingRuns |
| 20 | import Lax366625.NumberedCircuits |
| 21 | import Lax366625.HornNumbers |
| 22 | |
| 23 | /-! |
| 24 | --- |
| 25 | title: #P is closed under parsimonious reductions |
| 26 | type: theorem |
| 27 | --- |
| 28 | Membership in #P travels backward along ordered parsimonious reductions and |
| 29 | along relativized ordered parsimonious reductions: if a counting problem |
| 30 | reduces to a problem of #P, it is in #P. The witnesses of the target, pulled |
| 31 | back along the interpretation, are witnesses of the source; for a |
| 32 | relativized reduction, the kernel pins the pulled relations to the definable |
| 33 | domain, which makes the correspondence of witnesses a bijection. Membership |
| 34 | reads a problem on its finite instances only. |
| 35 | -/ |
| 36 | |
| 37 | namespace Lax366625.SharpPClosure |
| 38 | |
| 39 | open FirstOrder FirstOrder.Language |
| 40 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder |
| 41 | open Lax904597.Classes Lax904597.Sat Lax904597.Machines |
| 42 | open Lax535992.ClassPTIME |
| 43 | open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting |
| 44 | open Lax366625.SecondOrderCounting |
| 45 | open Lax366625.QuantitativeLogic Lax366625.CountingSat Lax366625.MachineNumbers |
| 46 | open Lax366625.CountingRuns |
| 47 | open Lax366625.NumberedCircuits Lax366625.HornNumbers |
| 48 | |
| 49 | /-- Membership in SharpP travels backward along ordered parsimonious reductions. -/ |
| 50 | axiom SharpP_mem_of_orderedParsimonious : |
| 51 | ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational] |
| 52 | {C : CountingProblem L} {D : CountingProblem L'}, |
| 53 | OrderedParsimoniousReduction C D → SharpP.Mem D → SharpP.Mem C |
| 54 | |
| 55 | /-- Membership in SharpP travels backward along relativized ordered |
| 56 | parsimonious reductions. -/ |
| 57 | axiom SharpP_mem_of_relOrderedParsimonious : |
| 58 | ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational] |
| 59 | {C : CountingProblem L} {D : CountingProblem L'}, |
| 60 | RelOrderedParsimoniousReduction C D → SharpP.Mem D → SharpP.Mem C |
| 61 | |
| 62 | /-- Membership in SharpP only depends on the finite instances of a problem. -/ |
| 63 | axiom SharpP_mem_congr_finite : ∀ {L : Language.{0, 0}} [L.IsRelational] {C D : CountingProblem L}, |
| 64 | (∀ (A : Type) [L.Structure A] [Finite A], C A = D A) → (SharpP.Mem C ↔ SharpP.Mem D) |
| 65 | |
| 66 | end Lax366625.SharpPClosure |
| 67 |
Builds on
Lax366625.CountingClassesLax366625.CountingProblemsLax366625.CountingRunsLax366625.CountingSatLax366625.HornNumbersLax366625.MachineNumbersLax366625.NumberedCircuitsLax366625.QuantitativeLogicLax366625.SecondOrderCountingLax366625.WitnessCountingLax535992.CircuitValueLax535992.ClassPTIMELax535992.DeterministicMachinesLax535992.HornSatLax904597.ClassesLax904597.InterpretationsLax904597.MachinesLax904597.ProblemsLax904597.RelativizedLax904597.SatLax904597.SecondOrder
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments