Lax Lean Archive

Clique Is in W[1]

Lax496464.WH_D01_CliqueInW1 · concepts/Lax496464/WH_D01_CliqueInW1.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-Clique is in W[1] [FG06, Example 5.2]. A set XX of vertices is a clique exactly when the graph satisfies the Π1\Pi_1-sentence [FG06, Example 4.39]

    clique(X)  =  ∀y ∀z ((Xy∧Xz∧¬ y=z)→Eyz),\mathrm{clique}(X) \;=\; \forall y\,\forall z\,\big((Xy \wedge Xz \wedge \neg\, y = z) \to Eyz\big),

    so pp-Clique fpt-reduces to p-WDcliquep\text{-WD}_{\mathrm{clique}}: the graph becomes the structure whose universe is its vertex set and whose one relation is its edge relation, and kk is unchanged.

    Concept map
    15 concepts; 2 descendants hidden
    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 clique_isParameterized proven

    2 clique_le_pWD proven

    3 clique_mem_W1 proven

    4 cliqueFormula_isPi proven

    5 cliqueFormula_isSentence proven

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2import Lax496464.WH_C1_GraphProblems
    3
    4/-!
    5---
    6title: Clique Is in W[1]
    7type: theorem
    8---
    9pp-Clique is in W[1] [FG06, Example 5.2]. A set XX of vertices is a clique exactly when the graph
    10satisfies the Π1\Pi_1-sentence [FG06, Example 4.39]
    11
    12clique(X)  =  ∀y ∀z ((Xy∧Xz∧¬ y=z)→Eyz),\mathrm{clique}(X) \;=\; \forall y\,\forall z\,\big((Xy \wedge Xz \wedge \neg\, y = z) \to Eyz\big),
    13
    14so pp-Clique fpt-reduces to p-WDcliquep\text{-WD}_{\mathrm{clique}}: the graph becomes the structure whose
    15universe is its vertex set and whose one relation is its edge relation, and kk is unchanged.
    16
    17# Formalization Notes
    18
    19In `cliqueFormula` the variables y,zy, z are 0,10, 1, the edge relation EE is the binary symbol 00,
    20and XX is unary. The edge relation contains both (u,v)(u, v) and (v,u)(v, u) for every edge uvuv.
    21-/
    22
    23namespace Lax496464.WH_D01_CliqueInW1
    24
    25open Lax496464.WH_B2_FirstOrder Lax496464.WH_B3_LogicProblems Lax496464.WH_B4_Hierarchies
    26open Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
    27
    28/-- `clique(X) = ∀y ∀z ((Xy ∧ Xz ∧ ¬ y = z) → E y z)`. -/
    29def cliqueFormula : Formula :=
    30 .all 0 (.all 1 (Formula.imp
    31 (.and (.setVar [0]) (.and (.setVar [1]) (.neg (.eq 0 1))))
    32 (.rel 0 [0, 1])))
    33
    34/-- `clique(X)` is a `Π_1`-formula. -/
    35axiom cliqueFormula_isPi : IsPi 1 cliqueFormula
    36
    37/-- `clique(X)` is a sentence. -/
    38axiom cliqueFormula_isSentence : IsSentence cliqueFormula
    39
    40/-- The parameter of `p-Clique` is computable in polynomial time. -/
    41axiom clique_isParameterized : IsParameterized Clique
    42
    43/-- **The reduction:** `p-Clique ≤fpt p-WD_clique`. -/
    44axiom clique_le_pWD : Clique ≤ᶠᵖᵗ pWD cliqueFormula 1
    45
    46/-- **`p-Clique ∈ W[1]`.** -/
    47axiom clique_mem_W1 : Clique ∈ W 1
    48
    49end Lax496464.WH_D01_CliqueInW1
    50
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    In cliqueFormulacliqueFormula the variables y,zy, z are 0,10, 1, the edge relation EE is the binary symbol 00, and XX is unary. The edge relation contains both (u,v)(u, v) and (v,u)(v, u) for every edge uvuv.

    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…