W[1] = A[1]

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

proven

Loading review…

The first level of the W-hierarchy equals the first level of the A-hierarchy [FG06, Theorem 6.35].

$\mathrm{A}[1] \subseteq \mathrm{W}[1]$ : every problem of A[1] fpt-reduces to Clique ( $WH_D06_CliqueA1Complete$ ), which is in W[1] ( $WH_D01_CliqueInW1$ ).
$\mathrm{W}[1] \subseteq \mathrm{A}[1]$ : every problem of W[1] fpt-reduces to some $p\text{-WD}_\varphi$ with $\varphi \in \Pi_1$ , which fpt-reduces to $p\text{-WSat}(d\text{-CNF})$ ( $WH_D07_DefinabilityToWSat$ ), which is in A[1] ( $WH_D08_WSatInA1$ ).

Concept map

12 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_B4_Hierarchies
2
3	/-!
4	---
5	title: W[1] = A[1]
6	type: theorem
7	---
8	The first level of the W-hierarchy equals the first level of the A-hierarchy [FG06, Theorem 6.35].
9
10	* $\mathrm{A}[1] \subseteq \mathrm{W}[1]$ : every problem of A[1] fpt-reduces to Clique
11	(`WH_D06_CliqueA1Complete`), which is in W[1] (`WH_D01_CliqueInW1`).
12	* $\mathrm{W}[1] \subseteq \mathrm{A}[1]$ : every problem of W[1] fpt-reduces to some
13	$p\text{-WD}_\varphi$ with $\varphi \in \Pi_1$ , which fpt-reduces to $p\text{-WSat}(d\text{-CNF})$
14	(`WH_D07_DefinabilityToWSat`), which is in A[1] (`WH_D08_WSatInA1`).
15	-/
16
17	namespace Lax496464.WH_D09_W1EqA1
18
19	open Lax496464.WH_B4_Hierarchies
20
21	/-- `W[1] = A[1]` [FG06, Theorem 6.35]. -/
22	axiom W1_eq_A1 : W 1 = A 1
23
24	end Lax496464.WH_D09_W1EqA1
25

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