Lax Lean Archive

Hitting Set Is in W[2]

Lax496464.WH_E1_HittingSetInW2 · concepts/Lax496464/WH_E1_HittingSetInW2.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

    pp-Hitting-Set is in W[2] [FG06, Example 5.2]. A hypergraph becomes the structure whose universe has one element per vertex and one per hyperedge, with unary relations VERT\mathrm{VERT} and EDGE\mathrm{EDGE} distinguishing them and the incidence relation II, where IyxI y x states that vertex yy lies in hyperedge xx. A set XX of kk elements is a hitting set exactly when the structure satisfies the Π2\Pi_2-sentence

    hs(X)=∀x ∀z ∃y ((EDGE x→(Xy∧VERT y∧Iyx))∧(Xz→VERT z)),\mathrm{hs}(X) = \forall x\,\forall z\,\exists y\,\big((\mathrm{EDGE}\,x \to (Xy \wedge \mathrm{VERT}\,y \wedge Iyx)) \wedge (Xz \to \mathrm{VERT}\,z)\big),

    whose second conjunct makes the kk elements of XX vertices [FG06, Example 4.42].

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

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

    1 hittingSet_isParameterized proven

    2 hittingSet_le_pWD proven

    3 hittingSet_mem_W2 proven

    4 hsFormula_isPi proven

    5 hsFormula_isSentence proven

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2import Lax496464.WH_C2_HittingSet
    3
    4/-!
    5---
    6title: Hitting Set Is in W[2]
    7type: theorem
    8---
    9pp-Hitting-Set is in W[2] [FG06, Example 5.2]. A hypergraph becomes the structure whose universe
    10has one element per vertex and one per hyperedge, with unary relations VERT\mathrm{VERT} and
    11EDGE\mathrm{EDGE} distinguishing them and the incidence relation II, where IyxI y x states that vertex
    12yy lies in hyperedge xx. A set XX of kk elements is a hitting set exactly when the structure
    13satisfies the Π2\Pi_2-sentence
    14
    15hs(X)=∀x ∀z ∃y ((EDGE x→(Xy∧VERT y∧Iyx))∧(Xz→VERT z)),\mathrm{hs}(X) = \forall x\,\forall z\,\exists y\,\big((\mathrm{EDGE}\,x \to (Xy \wedge \mathrm{VERT}\,y \wedge Iyx)) \wedge (Xz \to \mathrm{VERT}\,z)\big),
    16
    17
    18whose second conjunct makes the kk elements of XX vertices [FG06, Example 4.42].
    19
    20# Formalization Notes
    21
    22In `hsFormula` the variables x,y,zx, y, z are 0,1,20, 1, 2, and the relation symbols VERT,EDGE,I\mathrm{VERT}, \mathrm{EDGE}, I
    23 are 0,1,20, 1, 2. Since the universe size is written in binary, the reduction first
    24restricts the universe to the elements occurring in the sets and maps instances with kk larger
    25than the universe to a fixed no-instance.
    26-/
    27
    28namespace Lax496464.WH_E1_HittingSetInW2
    29
    30open Lax496464.WH_B2_FirstOrder Lax496464.WH_B3_LogicProblems Lax496464.WH_B4_Hierarchies
    31open Lax496464.WH_A2_FptReductions Lax496464.WH_C2_HittingSet
    32
    33/-- `hs(X) = ∀x ∀z ∃y ((EDGE x → (Xy ∧ VERT y ∧ I y x)) ∧ (Xz → VERT z))`. -/
    34def hsFormula : Formula :=
    35 .all 0 (.all 2 (.ex 1 (.and
    36 (Formula.imp (.rel 1 [0]) (.and (.setVar [1]) (.and (.rel 0 [1]) (.rel 2 [1, 0]))))
    37 (Formula.imp (.setVar [2]) (.rel 0 [2])))))
    38
    39/-- `hs(X)` is a `Π_2`-formula. -/
    40axiom hsFormula_isPi : IsPi 2 hsFormula
    41
    42/-- `hs(X)` is a sentence. -/
    43axiom hsFormula_isSentence : IsSentence hsFormula
    44
    45/-- The parameter of `p-Hitting-Set` is computable in polynomial time. -/
    46axiom hittingSet_isParameterized : IsParameterized HittingSet
    47
    48/-- **The reduction:** `p-Hitting-Set ≤fpt p-WD_hs`. -/
    49axiom hittingSet_le_pWD : HittingSet ≤ᶠᵖᵗ pWD hsFormula 1
    50
    51/-- **`p-Hitting-Set ∈ W[2]`.** -/
    52axiom hittingSet_mem_W2 : HittingSet ∈ W 2
    53
    54end Lax496464.WH_E1_HittingSetInW2
    55
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    In hsFormulahsFormula the variables x,y,zx, y, z are 0,1,20, 1, 2, and the relation symbols VERT,EDGE,I\mathrm{VERT}, \mathrm{EDGE}, I are 0,1,20, 1, 2. Since the universe size is written in binary, the reduction first restricts the universe to the elements occurring in the sets and maps instances with kk larger than the universe to a fixed no-instance.

    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…