ColorSym need not find an existing list multicoloring

Abstract

A colorable K4 list assignment defeats every ColorSym execution.

Definition 1.1 (Color support).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall c\in \mathbb{Z},\mathrm{supp}\left(L,c\right)=\mathrm{Finset}.\mathrm{filter}\left(\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto c\in L\left(i\right),\mathrm{Finset}.\mathrm{univ}\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.supp (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

The support of an integer color is the set of vertices whose lists contain it. Vertices of the complete graph are indexed by Fin n, with the paper’s indices shifted down by one.

Definition 1.2 (Proper intersections).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall S\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{Ip}\left(L,S\right)=\mathrm{Finset}.\mathrm{filter}\left(\mathrm{fun}(c:\mathbb{Z})\mapsto \mathrm{supp}\left(L,c\right)=S,\mathrm{Finset}.\mathrm{biUnion}\left(\mathrm{Finset}.\mathrm{univ},L\right)\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.Ip (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 2.1, p. 59, defines the proper intersection by taking the intersection of the selected lists and removing the union of all other lists. Here colors are integers in the union of the lists, filtered by exact support; the empty support has empty proper intersection.

Definition 1.3 (List multicoloring).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall b\in \mathbb{N},\forall p\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\mathrm{IsColoring}\left(L,b,p\right)=\left((\forall i\in \mathrm{Fin}\left(n\right),(p\left(i\right)\subseteq L\left(i\right))\wedge (\mathrm{Finset}.\mathrm{card}\left(p\left(i\right)\right)=b))\wedge (\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),(i\ne j)\Rightarrow (\mathrm{Disjoint}\left(p\left(i\right),p\left(j\right)\right)))\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.IsColoring (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 1, pp. 57–58: “a coloring function φ on the vertices of G that assigns to each vertex v a subset of b elements from L(v) in such a way that φ(u) ∩ φ(v) = ∅ for any uv ∈ E(G)”. For a complete graph, every pair of distinct vertices is adjacent. The symbol p denotes φ.

Definition 1.4 (Existence of a list multicoloring).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall b\in \mathbb{N},\mathrm{Colorable}\left(L,b\right)=\left(\exists p\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\mathrm{IsColoring}\left(L,b,p\right)\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.Colorable (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

A list assignment is colorable when such a family of disjoint b-element subsets exists.

Definition 1.5 (Order of supports).

$$\forall n\in \mathbb{N},\forall ord\in \mathrm{List}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\mathrm{AdmissibleOrder}\left(ord\right)=\left((\mathrm{List}.\mathrm{Nodup}\left(ord\right))\wedge \left((\forall S\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),(S\in ord)\iff (2\le \mathrm{Finset}.\mathrm{card}\left(S\right)))\wedge (\mathrm{List}.\mathrm{Pairwise}\left(\mathrm{fun}(S:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{fun}(T:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{Finset}.\mathrm{card}\left(S\right)\le \mathrm{Finset}.\mathrm{card}\left(T\right),ord\right))\right)\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.AdmissibleOrder (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “Otherwise, for each set S with |S| = i, consider |Ip(S)|”. The order contains every support of size at least two exactly once, with nondecreasing size.

Definition 1.6 (Choosing a color).

$$\forall pick\in \mathrm{Finset}\left(\mathbb{Z}\right)\to \mathbb{Z},\mathrm{AdmissiblePick}\left(pick\right)=\left(\forall s\in \mathrm{Finset}\left(\mathbb{Z}\right),(\mathrm{Finset}.\mathrm{Nonempty}\left(s\right))\Rightarrow (pick\left(s\right)\in s)\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.AdmissiblePick (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “Remove a color from Ip(S) and assign it to vj.” The function pick selects an element from every nonempty integer-color pool.

Definition 1.7 (Least-loaded vertex and tie breaking).

$$\forall n\in \mathbb{N},\forall S\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall w\in \mathrm{Fin}\left(n\right)\to \mathbb{N},((\mathrm{Finset}.\mathrm{sort}\left(\mathrm{Finset}.\mathrm{filter}\left(\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \forall j\in \mathrm{Fin}\left(n\right),(j\in S)\Rightarrow (w\left(i\right)\le w\left(j\right)),S\right),\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto i\le j\right)=[])\Rightarrow (\mathrm{best}\left(S,w\right)=\mathrm{none}))\wedge (\forall j\in \mathrm{Fin}\left(n\right),\forall rest\in \mathrm{List}\left(\mathrm{Fin}\left(n\right)\right),(\mathrm{Finset}.\mathrm{sort}\left(\mathrm{Finset}.\mathrm{filter}\left(\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \forall j\in \mathrm{Fin}\left(n\right),(j\in S)\Rightarrow (w\left(i\right)\le w\left(j\right)),S\right),\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto i\le j\right)=\mathrm{List}.\mathrm{cons}\left(j,rest\right))\Rightarrow (\mathrm{best}\left(S,w\right)=\mathrm{some}\left(j\right)))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.best (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “let j ∈ S be the index for which w(j) is minimum (if more than one j with minimum w, then take the smallest index)”. Sorting the set of minimizers in ascending vertex order selects exactly this vertex.

Definition 1.8 (Stopping condition).

$$\forall n\in \mathbb{N},\forall b\in \mathbb{N},\forall st\in (\mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right))\times (\mathrm{Fin}\left(n\right)\to \mathbb{N}),\mathrm{stopped}\left(b,st\right)=\mathrm{decide}\left(\forall j\in \mathrm{Fin}\left(n\right),b\le (st).2\left(j\right)\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.stopped (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “If wi ≥ b for each i or i = n + 1, then Stop.” The first component of st records output sets and the second records their loads. Exhausting the support list implements the terminal step n + 1.

Definition 1.9 (Assigning one color).

$$\forall n\in \mathbb{N},\forall st\in (\mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right))\times (\mathrm{Fin}\left(n\right)\to \mathbb{N}),\forall j\in \mathrm{Fin}\left(n\right),\forall c\in \mathbb{Z},\mathrm{assign}\left(st,j,c\right)=⟨\mathrm{Function}.\mathrm{update}\left((st).1,j,\mathrm{insert}\left(c,(st).1\left(j\right)\right)\right),\mathrm{Function}.\mathrm{update}\left((st).2,j,(st).2\left(j\right)+1\right)⟩$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.assign (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

A color is inserted at the selected vertex and its load increases by one.

Definition 1.10 (Processing one proper intersection).

$$\forall n\in \mathbb{N},\forall S\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall b\in \mathbb{N},\forall pick\in \mathrm{Finset}\left(\mathbb{Z}\right)\to \mathbb{Z},\forall pool\in \mathrm{Finset}\left(\mathbb{Z}\right),\forall st\in (\mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right))\times (\mathrm{Fin}\left(n\right)\to \mathbb{N}),(\mathrm{runPool}\left(S,b,pick,0,pool,st\right)=st)\wedge (\forall fuel\in \mathbb{N},\mathrm{runPool}\left(S,b,pick,fuel+1,pool,st\right)=\mathrm{if}\mathrm{stopped}\left(b,st\right)\mathrm{then}st\mathrm{else}\mathrm{if}pool=\varnothing \mathrm{then}st\mathrm{else}\mathrm{match}\mathrm{best}\left(S,(st).2\right)\mathrm{with}|\mathrm{none}\mapsto st|\mathrm{some}\left(j\right)\mapsto \mathrm{let}c:=pick\left(pool\right);\mathrm{runPool}\left(S,b,pick,fuel,\mathrm{Finset}.\mathrm{erase}\left(pool,c\right),\mathrm{assign}\left(st,j,c\right)\right))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.runPool (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “Goto Step i until Ip(S) is empty.” The fuel is initially the pool cardinality. Each assignment erases the chosen color, so an admissible pick decreases that cardinality by one.

Definition 1.11 (Processing all supports).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall b\in \mathbb{N},\forall pick\in \mathrm{Finset}\left(\mathbb{Z}\right)\to \mathbb{Z},\forall st\in (\mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right))\times (\mathrm{Fin}\left(n\right)\to \mathbb{N}),(\mathrm{runSupports}\left(L,b,pick,[],st\right)=st)\wedge (\forall S\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall ord\in \mathrm{List}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\mathrm{runSupports}\left(L,b,pick,\mathrm{List}.\mathrm{cons}\left(S,ord\right),st\right)=\mathrm{runSupports}\left(L,b,pick,ord,\mathrm{runPool}\left(S,b,pick,\mathrm{Finset}.\mathrm{card}\left(\mathrm{Ip}\left(L,S\right)\right),\mathrm{Ip}\left(L,S\right),st\right)\right))$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.runSupports (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Each support is processed with its proper intersection as the color pool. The empty list returns the current pair of outputs and loads.

Definition 1.12 (Singleton proper intersections).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\mathrm{initial}\left(L\right)=⟨\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{Ip}\left(L,\{i\}\right),\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{Finset}.\mathrm{card}\left(\mathrm{Ip}\left(L,\{i\}\right)\right)⟩$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.initial (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “Color every proper intersections of sets of size 1: vi gets |Ip({i})| colors. Thus wi = |Ip({i})|.” All singleton proper intersections are assigned before shared colors are processed.

Definition 1.13 (ColorSym output).

$$\forall n\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),\forall b\in \mathbb{N},\forall ord\in \mathrm{List}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\forall pick\in \mathrm{Finset}\left(\mathbb{Z}\right)\to \mathbb{Z},\mathrm{colorSym}\left(L,b,ord,pick\right)=(\mathrm{runSupports}\left(L,b,pick,ord,\mathrm{initial}\left(L\right)\right)).1$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.colorSym (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

The output is the first component of the final pair after the singleton step and all ordered supports.

Definition 1.14 (ColorSym optimality conjecture).

$$claim=\left(\forall n\in \mathbb{N},\forall a\in \mathbb{N},\forall b\in \mathbb{N},\forall L\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),(\forall i\in \mathrm{Fin}\left(n\right),\mathrm{Finset}.\mathrm{card}\left(L\left(i\right)\right)=a)\Rightarrow ((\mathrm{Colorable}\left(L,b\right))\Rightarrow (\exists ord\in \mathrm{List}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right),\exists pick\in \mathrm{Finset}\left(\mathbb{Z}\right)\to \mathbb{Z},(\mathrm{AdmissibleOrder}\left(ord\right))\wedge \left((\mathrm{AdmissiblePick}\left(pick\right))\wedge (\exists p\in \mathrm{Fin}\left(n\right)\to \mathrm{Finset}\left(\mathbb{Z}\right),(\mathrm{IsColoring}\left(L,b,p\right))\wedge (\forall i\in \mathrm{Fin}\left(n\right),p\left(i\right)\subseteq \mathrm{colorSym}\left(L,b,ord,pick\right)\left(i\right)))\right)))\right)$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.claim (✓ std3).

Citation. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Section 3.1, p. 63: “We conjecture that this algorithm is optimal (i.e., produces an (L, b)-coloring if K_n is (L, b)-colorable).” The parameters n, a and b are natural numbers, L assigns finite integer-color lists, and every list has exactly a elements. The formula allows any admissible support order and color selection, and asks only for a b-coloring contained in the output.

Theorem 1.15 (The optimality conjecture is false).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.result (✓ std3). ∎

Resolves. Problems/godin-grisot-togni-2022-colorsym-optimality (refuted) by D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.result.

Source. Repository-derived.

Acknowledgement. Jean-Christophe Godin; Rémi Grisot; Olivier Togni (2025). On List Coloring with Separation of the Complete Graph and Set System Intersections. DOI: 10.5614/ejgta.2025.13.1.5. URL: https://arxiv.org/abs/2209.03436.

Commentary.

Take four lists {1,2,3,4,5,6}, {1,2,3,4,7,8}, {5,6,9,10,11,12}, and {5,6,13,14,15,16}, and b = 4. The disjoint subsets {1,2,5,6}, {3,4,7,8}, {9,10,11,12}, and {13,14,15,16} form a 4-coloring. Every ColorSym execution has final loads (5,3,4,4), independently of color choice. Vertex 2 receives only three colors. Current-load balancing spends the pair pool on vertex 1 before its later triple pool, while vertex 2 has no later supply.

References

• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.AdmissibleOrder
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.AdmissiblePick
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.Colorable
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.Ip
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.IsColoring
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.assign
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.best
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.claim
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.colorSym
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.initial
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.result
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.runPool
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.runSupports
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.stopped
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/ColorSymOptimalityRefutation.supp