The coloring family: definitions

Three problems built on one generic property, DescriptiveComplexity.ColorableOn: a map into Fin k separating the pairs related by a conflict relation.

• DescriptiveComplexity.KCol k, on FirstOrder.Language.graph-structures: is the graph k-colorable, for a k fixed once and for all? The conflict relation is adjacency, so a self-loop makes the instance a no-instance, and DescriptiveComplexity.kCol_three identifies KCol 3 with DescriptiveComplexity.ThreeCol.
• DescriptiveComplexity.ChromaticNumber, on FirstOrder.Language.markedGraph-structures: is the chromatic number at most k, where k is the cardinality of the marked set (DescriptiveComplexity.Numbers.Unary)? This is Karp's CHROMATIC NUMBER, with k part of the instance rather than of the problem.
• DescriptiveComplexity.CliqueCover, on the same vocabulary: can the vertices be covered by at most k cliques? A clique cover is a proper coloring of the complement graph, so this is the same generic property with the conflict relation complemented – which is why one interpretation reduces each of the two threshold problems to the other, exactly as in DescriptiveComplexity.Problems.CliqueFamily.

Loops, and why the two threshold problems ignore them

The two marked-graph problems take their conflict relation off the diagonal (x ≠ y ∧ …), i.e. they are about the underlying loopless graph, which is the convention of the clique family on this vocabulary. It is also what makes them interreducible by edge complementation: complementing off the diagonal is an involution on loopless graphs, but forgets loops. The price is paid once, in the reduction from 3-colorability (DescriptiveComplexity.Problems.Coloring.Reductions), whose input is loop-sensitive: a self-looped vertex is turned into a K₄, which no 3-coloring survives.

The palette form of a threshold

A k-coloring with k the cardinality of the marked set can equivalently be given as a map into the marked set itself (DescriptiveComplexity.paletteColorableOn_iff): the marked elements are k colors. This is the form the second-order definitions guess, since it needs only a binary relation variable, where the number k is not available to the formulas.

The generic property

def DescriptiveComplexity.ColorableOn {A : Type} (Cfl : A → A → Prop) (k : ℕ) : Prop

A k-coloring for the conflict relation Cfl: a map into Fin k giving distinct values to conflicting elements.

Equations

• DescriptiveComplexity.ColorableOn Cfl k = ∃ (c : A → Fin k), ∀ (x y : A), Cfl x y → c x ≠ c y

def DescriptiveComplexity.PaletteColorableOn {A : Type} (Cfl : A → A → Prop) (Kp : A → Prop) : Prop

A coloring whose palette is the marked set itself: a map into the Kp-marked elements giving distinct values to conflicting elements.

Equations

• DescriptiveComplexity.PaletteColorableOn Cfl Kp = ∃ (col : A → A), (∀ (x : A), Kp (col x)) ∧ ∀ (x y : A), Cfl x y → col x ≠ col y

theorem DescriptiveComplexity.paletteColorableOn_iff {A : Type} [Finite A] (Cfl : A → A → Prop) (Kp : A → Prop) : PaletteColorableOn Cfl Kp ↔ ColorableOn Cfl {x : A | Kp x}.ncard

Colors are the marked elements: on a finite universe, colorability with as many colors as the marked set is colorability by the marked set. This is the bridge between the numeric reading of the threshold and its second-order rendering, where the coloring is guessed as a binary relation variable.

theorem DescriptiveComplexity.colorableOn_congr {A : Type} {Cfl Cfl' : A → A → Prop} {k : ℕ} (h : ∀ (x y : A), Cfl x y ↔ Cfl' x y) : ColorableOn Cfl k ↔ ColorableOn Cfl' k

ColorableOn only depends on the extension of the conflict relation.

theorem DescriptiveComplexity.ColorableOn.of_equiv {A B : Type} (u : B ≃ A) {CflB : B → B → Prop} {CflA : A → A → Prop} {k : ℕ} (hcfl : ∀ (b b' : B), CflB b b' ↔ CflA (u b) (u b')) (h : ColorableOn CflB k) : ColorableOn CflA k

ColorableOn transports along an equivalence commuting with the conflict relations.

theorem DescriptiveComplexity.ColorableOn.equiv_iff {A B : Type} (u : B ≃ A) {CflB : B → B → Prop} {CflA : A → A → Prop} {k : ℕ} (hcfl : ∀ (b b' : B), CflB b b' ↔ CflA (u b) (u b')) : ColorableOn CflB k ↔ ColorableOn CflA k

ColorableOn transports along an equivalence, iff version.

k-colorability, for a fixed k

def DescriptiveComplexity.KColorable (k : ℕ) (V : Type) [FirstOrder.Language.graph.Structure V] : Prop

A Language.graph-structure is k-colorable if the vertices can be colored with k colors so that adjacent vertices get distinct colors.

Equations

• DescriptiveComplexity.KColorable k V = DescriptiveComplexity.ColorableOn (fun (x y : V) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) k

theorem DescriptiveComplexity.kColorable_iso {k : ℕ} {A B : Type} [FirstOrder.Language.graph.Structure A] [FirstOrder.Language.graph.Structure B] (e : FirstOrder.Language.graph.Equiv A B) : KColorable k A ↔ KColorable k B

k-colorability is isomorphism-invariant.

def DescriptiveComplexity.KCol (k : ℕ) : DecisionProblem FirstOrder.Language.graph

k-colorability, as a problem on Language.graph-structures.

Equations

• DescriptiveComplexity.KCol k = { Holds := fun (V : Type) (inst : FirstOrder.Language.graph.Structure V) => DescriptiveComplexity.KColorable k V, iso_invariant := ⋯ }

theorem DescriptiveComplexity.kCol_three : KCol 3 = ThreeCol

At k = 3, k-colorability is 3-colorability.

Chromatic number and clique cover, with the threshold in the instance

def DescriptiveComplexity.MGConflict {A : Type} [FirstOrder.Language.markedGraph.Structure A] (x y : A) : Prop

The conflict relation of the chromatic-number problem: adjacency off the diagonal.

Equations

• DescriptiveComplexity.MGConflict x y = (x ≠ y ∧ DescriptiveComplexity.MGAdj x y)

def DescriptiveComplexity.MGCoConflict {A : Type} [FirstOrder.Language.markedGraph.Structure A] (x y : A) : Prop

The conflict relation of the clique-cover problem: non-adjacency off the diagonal – two vertices may share a clique exactly when they are adjacent.

Equations

• DescriptiveComplexity.MGCoConflict x y = (x ≠ y ∧ ¬DescriptiveComplexity.MGAdj x y)

def DescriptiveComplexity.HasSmallChromaticNumber (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph has chromatic number at most the size of its marked set. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasSmallChromaticNumber A = (Finite A ∧ DescriptiveComplexity.ColorableOn DescriptiveComplexity.MGConflict {x : A | DescriptiveComplexity.MGMarked x}.ncard)

def DescriptiveComplexity.HasSmallCliqueCover (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph can be covered by at most as many cliques as its marked set has elements.

Equations

• DescriptiveComplexity.HasSmallCliqueCover A = (Finite A ∧ DescriptiveComplexity.ColorableOn DescriptiveComplexity.MGCoConflict {x : A | DescriptiveComplexity.MGMarked x}.ncard)

theorem DescriptiveComplexity.hasSmallChromaticNumber_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasSmallChromaticNumber A ↔ HasSmallChromaticNumber B

The chromatic-number property is isomorphism-invariant.

theorem DescriptiveComplexity.hasSmallCliqueCover_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasSmallCliqueCover A ↔ HasSmallCliqueCover B

The clique-cover property is isomorphism-invariant.

def DescriptiveComplexity.ChromaticNumber : DecisionProblem FirstOrder.Language.markedGraph

CHROMATIC NUMBER, as a problem on marked graphs: can the graph be properly colored with as many colors as the marked set has elements?

Equations

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

def DescriptiveComplexity.CliqueCover : DecisionProblem FirstOrder.Language.markedGraph

CLIQUE COVER, as a problem on marked graphs: can the vertices be covered by at most as many cliques as the marked set has elements?

Equations

• DescriptiveComplexity.CliqueCover = { Holds := fun (A : Type) (inst : FirstOrder.Language.markedGraph.Structure A) => DescriptiveComplexity.HasSmallCliqueCover A, iso_invariant := ⋯ }