Lax Lean Archive

Clique Is in A[1]

Lax496464.WH_D02_CliqueInA1 · concepts/Lax496464/WH_D02_CliqueInA1.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 A[1] [FG06, Example 5.8]: a graph has a clique of kk vertices exactly when it satisfies the Σ1\Sigma_1-sentence

    cliquek  =  ∃x1…∃xk(⋀1≤i<j≤k¬ xi=xj  ∧⋀1≤i<j≤kExixj),\mathrm{clique}_k \;=\; \exists x_1 \dots \exists x_k \Big(\bigwedge_{1 \le i < j \le k} \neg\, x_i = x_j \;\wedge \bigwedge_{1 \le i < j \le k} E x_i x_j\Big),

    so (G,k)↦(G,cliquek)(G, k) \mapsto (G, \mathrm{clique}_k) is an fpt-reduction from pp-Clique to p-MC(Σ1)p\text{-MC}(\Sigma_1). The formula depends on kk only and has size O(k2)O(k^2), the new parameter.

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

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

    1 clique_le_pMC proven

    2 clique_mem_A1 proven

    Lean source view on GitHub

    1import Lax496464.WH_D01_CliqueInW1
    2
    3/-!
    4---
    5title: Clique Is in A[1]
    6type: theorem
    7---
    8pp-Clique is in A[1] [FG06, Example 5.8]: a graph has a clique of kk vertices exactly when it
    9satisfies the Σ1\Sigma_1-sentence
    10
    11cliquek  =  ∃x1…∃xk(⋀1≤i<j≤k¬ xi=xj  ∧⋀1≤i<j≤kExixj),\mathrm{clique}_k \;=\; \exists x_1 \dots \exists x_k \Big(\bigwedge_{1 \le i < j \le k} \neg\, x_i = x_j \;\wedge \bigwedge_{1 \le i < j \le k} E x_i x_j\Big),
    12
    13
    14so (G,k)↦(G,cliquek)(G, k) \mapsto (G, \mathrm{clique}_k) is an fpt-reduction from pp-Clique to
    15p-MC(Σ1)p\text{-MC}(\Sigma_1). The formula depends on kk only and has size O(k2)O(k^2), the new parameter.
    16-/
    17
    18namespace Lax496464.WH_D02_CliqueInA1
    19
    20open Lax496464.WH_B2_FirstOrder Lax496464.WH_B3_LogicProblems Lax496464.WH_B4_Hierarchies
    21open Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
    22
    23/-- **The reduction:** `p-Clique ≤fpt p-MC(Σ_1)`. -/
    24axiom clique_le_pMC : Clique ≤ᶠᵖᵗ pMC {φ | IsSigma 1 φ}
    25
    26/-- **`p-Clique ∈ A[1]`.** -/
    27axiom clique_mem_A1 : Clique ∈ A 1
    28
    29end Lax496464.WH_D02_CliqueInA1
    30
    Show ProofShow Proof
    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…