Lax Lean Archive

W[2]-Hardness

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

definition

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

    Definition

    The scheduling development uses W2HardPW2Hard P to state the existence of an FPT-reduction from Hitting Set, parameterized by solution size, to PP. Its interpretation as W[2]-hardness follows from the W[2]-hardness of Hitting Set.

    Concept map
    6 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 7 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.HittingSet
    2
    3/-!
    4---
    5title: W[2]-Hardness
    6type: definition
    7---
    8The scheduling development uses `W2Hard P` to state the existence of an FPT-reduction
    9from Hitting Set, parameterized by solution size, to `P`. Its interpretation as
    10W[2]-hardness follows from the W[2]-hardness of Hitting Set.
    11
    12# Formalization Notes
    13
    14The Lean definition below refers to Hitting Set and FPT-reductions. The scheduling
    15proofs establish these reductions directly. For completeness, the submission also
    16includes the `WH_*` development of the W-hierarchy, following Flum and Grohe (2006).
    17That supporting material goes beyond the scope of the scheduling project and is not
    18needed to state or prove the scheduling reduction.
    19-/
    20
    21namespace Lax496464.W2Hardness
    22
    23open Lax496464.ParameterizedComplexity
    24
    25/-- `P` is **W[2]-hard**: Hitting Set, parameterized by the solution size, fpt-reduces to
    26it. -/
    27def W2Hard (P : Problem) : Prop := HittingSet.byK ≤fpt P
    28
    29end Lax496464.W2Hardness
    30
    Formalization Notes

    The Lean definition below refers to Hitting Set and FPT-reductions. The scheduling proofs establish these reductions directly. For completeness, the submission also includes the WH∗WH_* development of the W-hierarchy, following Flum and Grohe (2006). That supporting material goes beyond the scope of the scheduling project and is not needed to state or prove the scheduling reduction.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…