Reductions of the coloring family

Three reductions, one per problem of the family:

• DescriptiveComplexity.threeCol_fo_reduction_kCol: 3-colorability reduces to k-colorability for every k = 3 + m, by padding the graph with m universal vertices. An interpretation cannot add constantly many elements to a universe, so the new vertices become tags, hence blown-up independent classes (DescriptiveComplexity.padColorInterp, tag type Option (Fin m)); this is harmless, because a proper coloring gives the classes pairwise disjoint sets of colors, all disjoint from the colors of the original part, leaving exactly three for it.

• DescriptiveComplexity.threeCol_ordered_fo_reduction_chromaticNumber: 3-colorability reduces to Chromatic Number, an ordered reduction (DescriptiveComplexity.chromInterp, tag Fin 4, dimension 1). The graph is kept on the copy of tag 0; the marked set must have exactly three elements, which no order-free interpretation can produce, so it is {0, 1, 2} × {minimum}, definable with DescriptiveComplexity.minF. The three spare copies are not only scaffolding for the threshold: the target problem ignores self-loops while 3-colorability does not, so a self-looped vertex is turned into the K₄ formed by its four copies, which no 3-coloring survives.

• DescriptiveComplexity.chromaticNumber_fo_reduction_cliqueCover and DescriptiveComplexity.cliqueCover_fo_reduction_chromaticNumber: the two threshold problems are interreducible by edge complementation, reusing DescriptiveComplexity.complEdgeInterp of the clique family unchanged: covering by cliques is coloring the complement, and complementing off the diagonal exchanges the two conflict relations while keeping the marked set.

The padding interpretation

Tags are Option (Fin m): the tag none carries the original graph, and each tag some i carries one blown-up universal vertex.

def DescriptiveComplexity.padColorInterp (m : ℕ) : FOInterpretation FirstOrder.Language.graph FirstOrder.Language.graph (Option (Fin m)) 1

The padding interpretation adding m universal (blown-up) vertices to a graph: the none-copy keeps the original adjacency, each some i-copy is an independent set, and any two elements with different tags are adjacent.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.padColorInterp_isQuantifierFree (m : ℕ) : (padColorInterp m).IsQuantifierFree

The padding interpretation is quantifier-free.

@[simp]

theorem DescriptiveComplexity.padColor_adj_orig {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![(none, w₁), (none, w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![w₁ 0, w₂ 0]

@[simp]

theorem DescriptiveComplexity.padColor_adj_left {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] (i : Fin m) (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![(some i, w₁), (none, w₂)]

@[simp]

theorem DescriptiveComplexity.padColor_adj_right {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] (i : Fin m) (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![(none, w₁), (some i, w₂)]

@[simp]

theorem DescriptiveComplexity.padColor_adj_pad {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] (i j : Fin m) (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![(some i, w₁), (some j, w₂)] ↔ i ≠ j

The two colors of the padded palette

Correctness of the padding

theorem DescriptiveComplexity.kColorable_map_of_threeColorable {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] (h : ThreeColorable A) : KColorable (3 + m) ((padColorInterp m).Map A)

A 3-coloring of a graph yields a (3 + m)-coloring of the padded graph.

theorem DescriptiveComplexity.threeColorable_of_kColorable_map {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] [Nonempty A] (h : KColorable (3 + m) ((padColorInterp m).Map A)) : ThreeColorable A

A (3 + m)-coloring of the padded graph yields a 3-coloring of the input: each of the m blown-up universal vertices consumes a color of its own, all distinct from the colors of the original copy, which is therefore left with at most three of them. (The input structure must be nonempty: an empty class would consume no color.)

theorem DescriptiveComplexity.threeColorable_iff_kColorable_map {m : ℕ} {A : Type} [FirstOrder.Language.graph.Structure A] [Nonempty A] : ThreeColorable A ↔ KColorable (3 + m) ((padColorInterp m).Map A)

Correctness of the padding interpretation.

def DescriptiveComplexity.threeCol_fo_reduction_kCol (m : ℕ) : FOReduction ThreeCol (KCol (3 + m))

3-colorability FO-reduces to (3 + m)-colorability, by padding the graph with m blown-up universal vertices.

Equations

• One or more equations did not get rendered due to their size.

Chromatic Number and Clique Cover are complements of each other

theorem DescriptiveComplexity.hasSmallChromaticNumber_iff_cliqueCover_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallChromaticNumber A ↔ HasSmallCliqueCover (complEdgeInterp.Map A)

Correctness of the edge complementation, chromatic-number-to-clique-cover direction.

theorem DescriptiveComplexity.hasSmallCliqueCover_iff_chromaticNumber_map (A : Type) [FirstOrder.Language.markedGraph.Structure A] : HasSmallCliqueCover A ↔ HasSmallChromaticNumber (complEdgeInterp.Map A)

Correctness of the edge complementation, clique-cover-to-chromatic-number direction.

def DescriptiveComplexity.chromaticNumber_fo_reduction_cliqueCover : FOReduction ChromaticNumber CliqueCover

Chromatic Number FO-reduces to Clique Cover, by complementing the edges: covering by cliques is coloring the complement.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.cliqueCover_fo_reduction_chromaticNumber : FOReduction CliqueCover ChromaticNumber

Clique Cover FO-reduces to Chromatic Number, by the same complementation.

Equations

• One or more equations did not get rendered due to their size.

3-colorability reduces to Chromatic Number

The threshold must be a marked set of exactly three elements, which no order-free interpretation can produce; with an order it is {0, 1, 2} times the minimum. The fourth tag exists for a different reason: the target problem reads its conflict relation off the diagonal, so a self-loop of the input – which makes it a no-instance – has to be turned into something no 3-coloring survives, and the K₄ on the four copies of the looped vertex is exactly that.

@[reducible, inline]

abbrev DescriptiveComplexity.oGAdjSym : (FirstOrder.Language.graph.sum FirstOrder.Language.order).Relations 2

The adjacency symbol over the ordered expansion of the graph vocabulary.

Equations

• DescriptiveComplexity.oGAdjSym = Sum.inl FirstOrder.Language.adj

noncomputable def DescriptiveComplexity.chromInterp : FOInterpretation (FirstOrder.Language.graph.sum FirstOrder.Language.order) FirstOrder.Language.markedGraph (Fin 4) 1

The interpretation of 3-colorability into Chromatic Number: the graph on the copy of tag 0, a K₄ on the four copies of each self-looped vertex, and the marked set {0, 1, 2} × {minimum} carrying the threshold 3.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.cnPt {A : Type} (i : Fin 4) (v : A) : chromInterp.Map A

The copy of a vertex carried by a tag.

Equations

• DescriptiveComplexity.cnPt i v = (i, fun (x : Fin 1) => v)

theorem DescriptiveComplexity.cnPt_eta {A : Type} (i : Fin 4) (w : Fin 1 → A) : (i, w) = cnPt i (w 0)

theorem DescriptiveComplexity.cnPt_injective {A : Type} (i : Fin 4) : Function.Injective (cnPt i)

@[simp]

theorem DescriptiveComplexity.chrom_adj_zero {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] (v w : A) : MGAdj (cnPt 0 v) (cnPt 0 w) ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![v, w]

@[simp]

theorem DescriptiveComplexity.chrom_adj_same {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] (i : Fin 4) (hi : i ≠ 0) (v w : A) : ¬MGAdj (cnPt i v) (cnPt i w)

@[simp]

theorem DescriptiveComplexity.chrom_adj_diff {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] {i j : Fin 4} (hij : i ≠ j) (v w : A) : MGAdj (cnPt i v) (cnPt j w) ↔ v = w ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![v, v]

@[simp]

theorem DescriptiveComplexity.chrom_marked {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] (i : Fin 4) (v : A) : MGMarked (cnPt i v) ↔ i ≠ 3 ∧ ∀ (a : A), v ≤ a

theorem DescriptiveComplexity.chrom_ncard_marked (A : Type) [FirstOrder.Language.graph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : {p : chromInterp.Map A | MGMarked p}.ncard = 3

The marked set of the interpreted structure has exactly three elements: the first three copies of the minimum.

theorem DescriptiveComplexity.threeColorable_iff_chromaticNumber_map (A : Type) [FirstOrder.Language.graph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ThreeColorable A ↔ HasSmallChromaticNumber (chromInterp.Map A)

Correctness of the interpretation: the graph is 3-colorable iff the interpreted marked graph has chromatic number at most the size of its marked set, which is three.

noncomputable def DescriptiveComplexity.threeCol_ordered_fo_reduction_chromaticNumber : OrderedFOReduction ThreeCol ChromaticNumber

3-colorability ordered-FO-reduces to Chromatic Number: keep the graph, mark three copies of the minimum to carry the threshold, and turn each self-looped vertex into a K₄.

Equations

• One or more equations did not get rendered due to their size.