The known seven-color bound for finite subcubic simple graphs

Open

OPG37271.subcubic_seven_color_bound

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

combinatoricsedge-coloringgraph-theoryopen-problem

Let $G$ be a finite simple graph in which every vertex has at most three neighbors. Then $G$ admits a star edge coloring with seven colors:

\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 7.

A star edge coloring is proper and has no bichromatic simple path or cycle of four edges. The path is not required to be induced. This is the established general upper bound that precedes the six-color conjecture.

Preamble

import Definitions.Def_opg37271_star_edge_coloring

Formal statement

namespace OPG37271

universe u

/-- The known general upper bound: every finite subcubic simple graph has a
star edge coloring with seven colors. -/
theorem subcubic_seven_color_bound
    {V : Type u} [Fintype V] (G : SimpleGraph V)
    (hsubcubic : IsSubcubic G) :
    HasStarEdgeColoring G 7 := by sorry

end OPG37271

Source

Dvořák--Mohar--Šámal, Star chromatic index, J. Graph Theory 72 (2013), 313--326, https://arxiv.org/abs/1011.3376, subcubic seven-color theorem; restated as Theorem 1.3(a) in Lei--Shi--Song, Star chromatic index of subcubic multigraphs, J. Graph Theory 88 (2018), 566--576, https://arxiv.org/abs/1701.04105v3

Read-back

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

For every finite type $V$ , every simple graph $G$ on $V$ , and every hypothesis that each vertex has at most three neighbors,

\forall v\in V,\quad \operatorname{encard}\bigl(\{u\in V\mid G\text{ is adjacent to }v\text{ and }u\}\bigr)\le 3,

there exists an assignment $c$ of one of the seven colors $\{0,1,\ldots,6\}$ to every edge of $G$ such that: (i) whenever $u\neq w$ are both adjacent to the same vertex $v$ , the colors assigned to the edges $vu$ and $vw$ are different; (ii) there do not exist five pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ with consecutive adjacencies $v_0v_1,v_1v_2,v_2v_3,v_3v_4$ such that the colors of $v_0v_1$ and $v_2v_3$ are equal and the colors of $v_1v_2$ and $v_3v_4$ are equal; and (iii) there do not exist four pairwise distinct vertices $v_0,v_1,v_2,v_3$ with adjacencies $v_0v_1,v_1v_2,v_2v_3,v_3v_0$ such that the colors of $v_0v_1$ and $v_2v_3$ are equal and the colors of $v_1v_2$ and $v_3v_0$ are equal.

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