The coloring family is NP-complete

Umbrella file for k-colorability, Chromatic Number and Clique Cover (DescriptiveComplexity.KCol, DescriptiveComplexity.ChromaticNumber, DescriptiveComplexity.CliqueCover, defined in DescriptiveComplexity.Problems.Coloring.Defs), collecting the reductions of DescriptiveComplexity.Problems.Coloring.Reductions and deriving NP-completeness from

• the Σ₁ definitions of DescriptiveComplexity.Problems.Coloring.Membership – color classes as k unary relations for the fixed-k problem, a coloring by the marked elements as one binary relation for the two threshold problems;
• the NP-hardness of 3-colorability (DescriptiveComplexity.threeCol_NP_hard), and so ultimately the Cook–Levin theorem, with no machine model anywhere: KCol k for k ≥ 3 by padding, Chromatic Number by the ordered reduction marking three copies of the minimum, and Clique Cover by complementing the edges.

The chain is 3COL ≤ᶠᵒ[≤] ChromaticNumber ≤ᶠᵒ CliqueCover ≤ᶠᵒ ChromaticNumber: the last two problems are interreducible, so it does not matter which of them carries the hardness. As with any complexity-theoretic statement, these results are about finite structures only (DescriptiveComplexity.ComplexityClass.mem_congr_finite/hard_congr_finite).

k-colorability

theorem DescriptiveComplexity.kCol_mem_NP (k : ℕ) : NP.Mem (KCol k)

k-colorability is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.kCol_NP_hard {k : ℕ} (hk : 3 ≤ k) : NP.Hard (KCol k)

For k ≥ 3, k-colorability is NP-hard: 3-colorability, which is NP-hard, reduces to it by padding.

theorem DescriptiveComplexity.kCol_NP_complete {k : ℕ} (hk : 3 ≤ k) : NP.Complete (KCol k)

k-colorability is NP-complete for every k ≥ 3.

Chromatic Number and Clique Cover

theorem DescriptiveComplexity.chromaticNumber_mem_NP : NP.Mem ChromaticNumber

Chromatic Number is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.chromaticNumber_NP_hard : NP.Hard ChromaticNumber

Chromatic Number is NP-hard: 3-colorability, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.chromaticNumber_NP_complete : NP.Complete ChromaticNumber

Chromatic Number is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

theorem DescriptiveComplexity.cliqueCover_mem_NP : NP.Mem CliqueCover

Clique Cover is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.cliqueCover_NP_hard : NP.Hard CliqueCover

Clique Cover is NP-hard: Chromatic Number, which is NP-hard, reduces to it by complementing the edges.

theorem DescriptiveComplexity.cliqueCover_NP_complete : NP.Complete CliqueCover

Clique Cover is NP-complete.