Clique Is A[1]-Complete

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

proven

Loading review…

$p$ -Clique is A[1]-complete under fpt-reductions [FG06, Theorem 6.1].

It is in A[1] ( $WH_D02_CliqueInA1$ ), and it is A[1]-hard by the chain

p\text{-MC}(\Sigma_1) \le p\text{-MC}(\Sigma_1^+) \le p\text{-MC}(\Sigma_1^+[2]) \le p\text{-MC}(\Sigma_1[2]) \le p\text{-Clique}

of $WH_D03_NegationElimination$ , $WH_D04_IncidenceStructure$ , the inclusion $\Sigma_1^+[2] \subseteq \Sigma_1[2]$ , and $WH_D05_BinaryToClique$ .

Concept map

17 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

1	import Lax496464.WH_D02_CliqueInA1
2
3	/-!
4	---
5	title: Clique Is A[1]-Complete
6	type: theorem
7	---
8	$p$ -Clique is A[1]-complete under fpt-reductions [FG06, Theorem 6.1].
9
10	It is in A[1] (`WH_D02_CliqueInA1`), and it is A[1]-hard by the chain
11
12	$p\text{-MC}(\Sigma_1) \le p\text{-MC}(\Sigma_1^+) \le p\text{-MC}(\Sigma_1^+[2]) \le p\text{-MC}(\Sigma_1[2]) \le p\text{-Clique}$
13
14
15	of `WH_D03_NegationElimination`, `WH_D04_IncidenceStructure`, the inclusion
16	$\Sigma_1^+[2] \subseteq \Sigma_1[2]$ , and `WH_D05_BinaryToClique`.
17	-/
18
19	namespace Lax496464.WH_D06_CliqueA1Complete
20
21	open Lax496464.WH_B4_Hierarchies Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
22
23	/-- `p-Clique` is A[1]-complete [FG06, Theorem 6.1]. -/
24	axiom clique_A1_complete : Complete (A 1) Clique
25
26	end Lax496464.WH_D06_CliqueA1Complete
27

Builds on

Used by

none

From Mathlib

none

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

Loading discussion…

Lax Lean Archive