Lax Lean Archive

Basic Facts About the Hierarchies

Lax496464.WH_B5_HierarchyFacts · concepts/Lax496464/WH_B5_HierarchyFacts.lean · lax-496464

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

    • The defining problems are parameterized problems: the parameters of p-WDφp\text{-WD}_\varphi (the last entry) and of p-MC(Φ)p\text{-MC}(\Phi) (the size of the formula) are computable in polynomial time. Hence p-WDφ∈W[t]p\text{-WD}_\varphi \in \mathrm{W}[t] for every Πt\Pi_t-sentence φ\varphi, and p-MC(Σt)∈A[t]p\text{-MC}(\Sigma_t) \in \mathrm{A}[t].
    • Model checking for a class of formulas fpt-reduces to model checking for any larger class.
    • The hierarchies are increasing: W[t]⊆W[t+1]\mathrm{W}[t] \subseteq \mathrm{W}[t+1] and A[t]⊆A[t+1]\mathrm{A}[t] \subseteq \mathrm{A}[t+1].
    • Conditional lower bounds. A W[t]\mathrm{W}[t]-hard problem in FPT places all of W[t]\mathrm{W}[t] in FPT; so, unless W[t]⊆FPT\mathrm{W}[t] \subseteq \mathrm{FPT}, no W[t]\mathrm{W}[t]-hard problem is fixed-parameter tractable.
    Concept map
    12 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 A_mono proven

    2 not_mem_FPT_of_hard proven

    3 pMC_isParameterized proven

    4 pMC_mem_A proven

    5 pMC_mono proven

    6 pWD_isParameterized proven

    7 pWD_mem_W proven

    8 W_mono proven

    9 W_subset_FPT_of_hard proven

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2
    3/-!
    4---
    5title: Basic Facts About the Hierarchies
    6type: theorem
    7---
    8* The defining problems are parameterized problems: the parameters of p-WDφp\text{-WD}_\varphi (the
    9 last entry) and of p-MC(Φ)p\text{-MC}(\Phi) (the size of the formula) are computable in polynomial time.
    10 Hence p-WDφ∈W[t]p\text{-WD}_\varphi \in \mathrm{W}[t] for every Πt\Pi_t-sentence φ\varphi, and
    11 p-MC(Σt)∈A[t]p\text{-MC}(\Sigma_t) \in \mathrm{A}[t].
    12* Model checking for a class of formulas fpt-reduces to model checking for any larger class.
    13* The hierarchies are increasing: W[t]⊆W[t+1]\mathrm{W}[t] \subseteq \mathrm{W}[t+1] and
    14 A[t]⊆A[t+1]\mathrm{A}[t] \subseteq \mathrm{A}[t+1].
    15* **Conditional lower bounds.** A W[t]\mathrm{W}[t]-hard problem in FPT places all of W[t]\mathrm{W}[t]
    16 in FPT; so, unless W[t]⊆FPT\mathrm{W}[t] \subseteq \mathrm{FPT}, no W[t]\mathrm{W}[t]-hard problem is
    17 fixed-parameter tractable.
    18-/
    19
    20namespace Lax496464.WH_B5_HierarchyFacts
    21
    22open Lax496464.WH_B2_FirstOrder Lax496464.WH_B3_LogicProblems Lax496464.WH_B4_Hierarchies
    23open Lax496464.WH_A2_FptReductions
    24open Lax888481.ParameterizedComplexity (Problem)
    25
    26/-- The parameter of a weighted definability problem is computable in polynomial time. -/
    27axiom pWD_isParameterized (φ : Formula) (s : ℕ) : IsParameterized (pWD φ s)
    28
    29/-- The parameter of a model-checking problem is computable in polynomial time. -/
    30axiom pMC_isParameterized (Φ : Set Formula) : IsParameterized (pMC Φ)
    31
    32/-- Model checking for a class fpt-reduces to model checking for a larger class. -/
    33axiom pMC_mono {Φ Φ' : Set Formula} : Φ ⊆ Φ' → pMC Φ ≤ᶠᵖᵗ pMC Φ'
    34
    35/-- `p-WD_φ ∈ W[t]` for every `Π_t`-sentence `φ`. -/
    36axiom pWD_mem_W {t : ℕ} {φ : Formula} (s : ℕ) : IsPi t φ → IsSentence φ → pWD φ s ∈ W t
    37
    38/-- `p-MC(Σ_t) ∈ A[t]`. -/
    39axiom pMC_mem_A (t : ℕ) : pMC {φ | IsSigma t φ} ∈ A t
    40
    41/-- The W-hierarchy is increasing. -/
    42axiom W_mono (t : ℕ) : W t ⊆ W (t + 1)
    43
    44/-- The A-hierarchy is increasing. -/
    45axiom A_mono (t : ℕ) : A t ⊆ A (t + 1)
    46
    47/-- **A `W[t]`-hard problem in FPT puts `W[t]` into FPT.** -/
    48axiom W_subset_FPT_of_hard {t : ℕ} {P : Problem} : Hard (W t) P → P ∈ FPT → W t ⊆ FPT
    49
    50/-- **Unless `W[t] ⊆ FPT`, no `W[t]`-hard problem is fixed-parameter tractable.** -/
    51axiom not_mem_FPT_of_hard {t : ℕ} {P : Problem} : ¬ W t ⊆ FPT → Hard (W t) P → P ∉ FPT
    52
    53end Lax496464.WH_B5_HierarchyFacts
    54
    Show ProofShow ProofShow ProofShow 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…