Lax Lean Archive

The Calculus of FPT-Reductions

Lax496464.WH_A3_ReductionCalculus · concepts/Lax496464/WH_A3_ReductionCalculus.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 rules by which hardness results are combined and applied.

    • Fpt-reducibility is reflexive and transitive [FG06, Lemma 2.3].
    • Hardness is inherited along reductions: if PP is CC-hard and P≤fptQP \le^{\mathrm{fpt}} Q, then QQ is CC-hard. To show a new problem CC-hard, reduce a known CC-hard problem to it.
    • If QQ is CC-complete, a problem is CC-hard exactly when QQ fpt-reduces to it.
    • Membership in [C]fpt[C]^{\mathrm{fpt}} is inherited backwards along reductions, and [C]fpt[C]^{\mathrm{fpt}} is monotone in CC; a problem is [C]fpt[C]^{\mathrm{fpt}}-hard as soon as every member of CC fpt-reduces to it.
    • FPT is closed under fpt-reductions [FG06, Lemma 2.2], so a CC-hard problem in FPT places all of CC in FPT. This is the sense in which W[1]-hardness is a lower bound.
    Concept map
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 closure_mono proven

    2 fptReduces_refl proven

    3 fptReduces_trans proven

    4 hard_closure_of proven

    5 hard_iff_of_complete proven

    6 hard_of_fptReduces proven

    7 mem_closure_of_fptReduces proven

    8 mem_closure_of_mem proven

    9 mem_FPT_of_fptReduces proven

    10 subset_FPT_of_hard proven

    Lean source view on GitHub

    1import Lax496464.WH_A2_FptReductions
    2
    3/-!
    4---
    5title: The Calculus of FPT-Reductions
    6type: theorem
    7---
    8The rules by which hardness results are combined and applied.
    9
    10* Fpt-reducibility is reflexive and transitive [FG06, Lemma 2.3].
    11* **Hardness is inherited along reductions:** if PP is CC-hard and P≤fptQP \le^{\mathrm{fpt}} Q, then
    12 QQ is CC-hard. To show a new problem CC-hard, reduce a known CC-hard problem to it.
    13* If QQ is CC-complete, a problem is CC-hard exactly when QQ fpt-reduces to it.
    14* Membership in [C]fpt[C]^{\mathrm{fpt}} is inherited backwards along reductions, and [C]fpt[C]^{\mathrm{fpt}}
    15 is monotone in CC; a problem is [C]fpt[C]^{\mathrm{fpt}}-hard as soon as every member of CC
    16 fpt-reduces to it.
    17* FPT is closed under fpt-reductions [FG06, Lemma 2.2], so a CC-hard problem in FPT places all of
    18 CC in FPT. This is the sense in which W[1]-hardness is a lower bound.
    19
    20# Formalization Notes
    21
    22Each rule follows from the two machine facts of `WH_A4_MachineFacts` — the identity is computable,
    23and fixed-parameter computations compose — and none of the statements mentions a program.
    24-/
    25
    26namespace Lax496464.WH_A3_ReductionCalculus
    27
    28open Lax888481.ParameterizedComplexity (Problem)
    29open Lax496464.WH_A2_FptReductions
    30
    31/-- **Reflexivity** [FG06, Lemma 2.3]. -/
    32axiom fptReduces_refl (P : Problem) : P ≤ᶠᵖᵗ P
    33
    34/-- **Transitivity** [FG06, Lemma 2.3]. -/
    35axiom fptReduces_trans {P Q R : Problem} : P ≤ᶠᵖᵗ Q → Q ≤ᶠᵖᵗ R → P ≤ᶠᵖᵗ R
    36
    37/-- **Hardness is inherited along fpt-reductions.** -/
    38axiom hard_of_fptReduces {C : Set Problem} {P Q : Problem} : Hard C P → P ≤ᶠᵖᵗ Q → Hard C Q
    39
    40/-- A complete problem of a class is the only one that needs reducing: `P` is `C`-hard exactly
    41when the `C`-complete problem `Q` fpt-reduces to it. -/
    42axiom hard_iff_of_complete {C : Set Problem} {P Q : Problem} (hQ : Complete C Q) :
    43 Hard C P ↔ Q ≤ᶠᵖᵗ P
    44
    45/-- A parameterized member of `C` belongs to `[C]^fpt`. -/
    46axiom mem_closure_of_mem {C : Set Problem} {P : Problem} :
    47 P ∈ C → IsParameterized P → P ∈ Closure C
    48
    49/-- **Membership is inherited backwards along fpt-reductions.** -/
    50axiom mem_closure_of_fptReduces {C : Set Problem} {P Q : Problem} :
    51 IsParameterized P → P ≤ᶠᵖᵗ Q → Q ∈ Closure C → P ∈ Closure C
    52
    53/-- `[·]^fpt` is monotone. -/
    54axiom closure_mono {C C' : Set Problem} : C ⊆ C' → Closure C ⊆ Closure C'
    55
    56/-- To be `[C]^fpt`-hard it suffices that every member of `C` fpt-reduce. -/
    57axiom hard_closure_of {C : Set Problem} {Q : Problem} :
    58 (∀ P ∈ C, P ≤ᶠᵖᵗ Q) → Hard (Closure C) Q
    59
    60/-- **FPT is closed under fpt-reductions** [FG06, Lemma 2.2]. -/
    61axiom mem_FPT_of_fptReduces {P Q : Problem} :
    62 IsParameterized P → P ≤ᶠᵖᵗ Q → Q ∈ FPT → P ∈ FPT
    63
    64/-- **A hard problem in FPT collapses its class into FPT.** -/
    65axiom subset_FPT_of_hard {C : Set Problem} {Q : Problem} :
    66 (∀ P ∈ C, IsParameterized P) → Hard C Q → Q ∈ FPT → C ⊆ FPT
    67
    68end Lax496464.WH_A3_ReductionCalculus
    69
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    Each rule follows from the two machine facts of WHA4MachineFactsWH_A4_MachineFacts — the identity is computable, and fixed-parameter computations compose — and none of the statements mentions a program.

    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…