{"id":"palomar/PALOMAR-2026-11-05-000001","url":"https://github.com/jtraverso/rudasova-sotak-equitable-strong/tree/57535a7c821a3186349a815482b5e3a4b987d9d6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-05-000001-v1.json","repo":"https://github.com/jtraverso/rudasova-sotak-equitable-strong","tags":["math.CO","msc:05C15"],"score":0,"title":"Equitable strong (vertex-distinguishing) edge colourings: Rudašová–Soták, Theorem 3.1","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Theorem 3.1 of J. Rudašová and R. Soták, Vertex-distinguishing proper edge colourings of some regular graphs (Discrete Math. 308, 2008). exists_equitable_strong: if a finite simple graph G has a strong (vertex-distinguishing) proper edge colouring with m colours and m ≤ k, then G has an equitable strong proper edge colouring with k colours. One statement. Edge colourings are colourings of the line graph; the palette of a vertex is the set of colours of its edges; strong means distinct vertices have distinct palettes; equitable means the colour classes…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-05","reactions":{},"formalized":true,"formalizes":[{"title":"Vertex-distinguishing proper edge colourings of some regular graphs","identifier":"doi:10.1016/j.disc.2007.07.019","relationship":"formalizes"}]}