Star edge colorings and subcubic simple graphs

Definition

opg37271_star_edge_coloring

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsedge-coloringgraph-theoryopen-problem

This module fixes the graph-theoretic language used for OPG-37271.

For a simple graph $G$ and a color type $K$ , an edge coloring assigns a member of $K$ to every unordered edge. It is proper when distinct edges meeting at a vertex receive distinct colors. A forbidden four-edge path consists of five pairwise distinct consecutive vertices, and a forbidden four-cycle consists of four pairwise distinct cyclic vertices. In either configuration, bichromaticity is represented by equality of the two pairs of opposite-position edge colors.

A star edge coloring is a proper edge coloring with neither forbidden configuration. The proposition

\operatorname{HasStarEdgeColoring}(G,k)

means that such a coloring exists with palette $\operatorname{Fin}(k)$ . Finally, $G$ is subcubic when every neighbor set has extended cardinality at most three. Paths are simple but are not required to be induced, and four-cycles are checked separately.

Definition code

import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
import Mathlib.Data.Set.Card

namespace OPG37271

universe u

/-- An edge coloring of a simple graph by colors in `K`. -/
abbrev EdgeColoring {V : Type u} (G : SimpleGraph V) (K : Type*) :=
  G.EdgeLabeling K

/-- A proper edge coloring: two distinct edges incident with one vertex
receive different colors. -/
def IsProperEdgeColoring {V : Type u} {G : SimpleGraph V} {K : Type*}
    (c : EdgeColoring G K) : Prop :=
  ∀ (v u w : V) (hvu : G.Adj v u) (hvw : G.Adj v w),
    u ≠ w → c.get v u hvu ≠ c.get v w hvw

/-- A simple path of four edges whose edge colors alternate between two colors. -/
def HasBicoloredPathFour {V : Type u} {G : SimpleGraph V} {K : Type*}
    (c : EdgeColoring G K) : Prop :=
  ∃ v₀ v₁ v₂ v₃ v₄ : V,
    [v₀, v₁, v₂, v₃, v₄].Nodup ∧
    ∃ (h₀₁ : G.Adj v₀ v₁) (h₁₂ : G.Adj v₁ v₂)
      (h₂₃ : G.Adj v₂ v₃) (h₃₄ : G.Adj v₃ v₄),
      c.get v₀ v₁ h₀₁ = c.get v₂ v₃ h₂₃ ∧
      c.get v₁ v₂ h₁₂ = c.get v₃ v₄ h₃₄

/-- A cycle of four edges whose edge colors alternate between two colors. -/
def HasBicoloredCycleFour {V : Type u} {G : SimpleGraph V} {K : Type*}
    (c : EdgeColoring G K) : Prop :=
  ∃ v₀ v₁ v₂ v₃ : V,
    [v₀, v₁, v₂, v₃].Nodup ∧
    ∃ (h₀₁ : G.Adj v₀ v₁) (h₁₂ : G.Adj v₁ v₂)
      (h₂₃ : G.Adj v₂ v₃) (h₃₀ : G.Adj v₃ v₀),
      c.get v₀ v₁ h₀₁ = c.get v₂ v₃ h₂₃ ∧
      c.get v₁ v₂ h₁₂ = c.get v₃ v₀ h₃₀

/-- A star edge coloring is proper and has no bichromatic simple path or cycle
of four edges. Paths need not be induced. -/
def IsStarEdgeColoring {V : Type u} {G : SimpleGraph V} {K : Type*}
    (c : EdgeColoring G K) : Prop :=
  IsProperEdgeColoring c ∧
    ¬ HasBicoloredPathFour c ∧
    ¬ HasBicoloredCycleFour c

/-- Existence of a star edge coloring using a palette of `k` labeled colors. -/
def HasStarEdgeColoring {V : Type u} (G : SimpleGraph V) (k : ℕ) : Prop :=
  ∃ c : EdgeColoring G (Fin k), IsStarEdgeColoring c

/-- A simple graph is subcubic when every vertex has at most three neighbors. -/
def IsSubcubic {V : Type u} (G : SimpleGraph V) : Prop :=
  ∀ v : V, (G.neighborSet v).encard ≤ 3

end OPG37271

Source

Open Problem Garden, OPG-37271, https://www.openproblemgarden.org/comment/reply/37271; definition also stated in Lei--Shi--Song, Star chromatic index of subcubic multigraphs, J. Graph Theory 88 (2018), 566--576, https://arxiv.org/abs/1701.04105v3, Section 1

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

`EdgeColoring`

For a vertex type $V$ , a simple graph $G$ on $V$ , and a color type $K$ , $\operatorname{EdgeColoring}(G,K)$ is the type of edge labelings of $G$ by elements of $K$ : every edge of $G$ is assigned a color in $K$ . For adjacent vertices $v,u$ , written $G.\operatorname{Adj}(v,u)$ , the value $c.\operatorname{get}(v,u,h)$ is the color assigned by $c$ to that edge, using an adjacency proof $h$ .

`IsProperEdgeColoring`

For vertex type $V$ , simple graph $G$ on $V$ , color type $K$ , and edge coloring $c : \operatorname{EdgeColoring}(G,K)$ , the predicate asserts that for every three vertices $v,u,w\in V$ , every proof $h_{vu}$ that $v$ is adjacent to $u$ , and every proof $h_{vw}$ that $v$ is adjacent to $w$ , if $u\ne w$ , then the two incident edges receive different colors:

u\ne w \;\Longrightarrow\; c.\operatorname{get}(v,u,h_{vu})\ne c.\operatorname{get}(v,w,h_{vw}).

`HasBicoloredPathFour`

For a vertex type $V$ , simple graph $G$ on $V$ , color type $K$ , and edge coloring $c : \operatorname{EdgeColoring}(G,K)$ , the predicate asserts that there exist vertices $v_0,v_1,v_2,v_3,v_4\in V$ such that the list $[v_0,v_1,v_2,v_3,v_4]$ has no repeated vertices, together with adjacency proofs

h_{01}:G.\operatorname{Adj}(v_0,v_1),\quad h_{12}:G.\operatorname{Adj}(v_1,v_2),\quad h_{23}:G.\operatorname{Adj}(v_2,v_3),\quad h_{34}:G.\operatorname{Adj}(v_3,v_4),

such that the first and third edges have the same color and the second and fourth edges have the same color:

c.\operatorname{get}(v_0,v_1,h_{01}) = c.\operatorname{get}(v_2,v_3,h_{23}) \quad\text{and}\quad c.\operatorname{get}(v_1,v_2,h_{12}) = c.\operatorname{get}(v_3,v_4,h_{34}).

`HasBicoloredCycleFour`

For a vertex type $V$ , simple graph $G$ on $V$ , color type $K$ , and edge coloring $c : \operatorname{EdgeColoring}(G,K)$ , the predicate asserts that there exist vertices $v_0,v_1,v_2,v_3\in V$ such that the list $[v_0,v_1,v_2,v_3]$ has no repeated vertices, together with adjacency proofs

h_{01}:G.\operatorname{Adj}(v_0,v_1),\quad h_{12}:G.\operatorname{Adj}(v_1,v_2),\quad h_{23}:G.\operatorname{Adj}(v_2,v_3),\quad h_{30}:G.\operatorname{Adj}(v_3,v_0),

such that opposite edges have matching colors:

c.\operatorname{get}(v_0,v_1,h_{01}) = c.\operatorname{get}(v_2,v_3,h_{23}) \quad\text{and}\quad c.\operatorname{get}(v_1,v_2,h_{12}) = c.\operatorname{get}(v_3,v_0,h_{30}).

`IsStarEdgeColoring`

For a vertex type $V$ , simple graph $G$ on $V$ , color type $K$ , and edge coloring $c : \operatorname{EdgeColoring}(G,K)$ , the predicate asserts all of the following: for every $v,u,w\in V$ , every $h_{vu}:G.\operatorname{Adj}(v,u)$ , and every $h_{vw}:G.\operatorname{Adj}(v,w)$ , $u\ne w$ implies

c.\operatorname{get}(v,u,h_{vu})\ne c.\operatorname{get}(v,w,h_{vw});

there do not exist five pairwise distinct vertices $v_0,\ldots,v_4$ with the four consecutive adjacencies $v_0\!-\!v_1\!-\!v_2\!-\!v_3\!-\!v_4$ whose first and third edge colors agree and whose second and fourth edge colors agree; and there do not exist four pairwise distinct vertices $v_0,\ldots,v_3$ with adjacencies $v_0\!-\!v_1$ , $v_1\!-\!v_2$ , $v_2\!-\!v_3$ , and $v_3\!-\!v_0$ whose opposite edge colors agree in the two corresponding pairs.

`HasStarEdgeColoring`

For a vertex type $V$ , a simple graph $G$ on $V$ , and a natural number $k$ , the predicate asserts that there exists an edge coloring

c:\operatorname{EdgeColoring}(G,\operatorname{Fin}(k)),

where $\operatorname{Fin}(k)$ is the type of the $k$ available finite colors, such that $c$ satisfies the full IsStarEdgeColoring condition described above: it is proper, has no bicolored path of the specified four-edge form, and has no bicolored cycle of the specified four-edge form. No assumption that $k>0$ is included; in particular, $k=0$ is allowed.

`IsSubcubic`

For a vertex type $V$ and a simple graph $G$ on $V$ , the predicate asserts that every vertex $v\in V$ has at most three distinct neighbors:

\operatorname{encard}\bigl(\{u\in V\mid G.\operatorname{Adj}(v,u)\}\bigr)\le 3.

Here the neighbor set consists exactly of the vertices adjacent to $v$ , and the assertion is made for every vertex, with no separate finiteness assumption.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph