Planar orientations, directed cycles, and acyclic two-colorings

Definition

opg169_planar_dichromatic

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

combinatoricsdirected-graphsgraph-theoryopen-problemplanar-graphs

This module couples a binary directed relation to an underlying finite simple graph by requiring exactly one direction on every edge and no arcs on nonedges. Planarity is represented by an injective crossing-free straight-line drawing of the underlying graph.

A directed cycle is a cyclic list of at least three distinct vertices following directed arcs. A two-coloring is valid when neither full induced color class contains such a cycle; colors may be unused. Strong connectivity uses nonempty reflexive-transitive directed reachability.

A least-order counterexample is planar, uncolorable, and smaller than every other uncolorable planar orientation in the same universe. The module also defines the underlying minimum-degree-three condition.

Definition code

import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Real.Basic
import Mathlib.Logic.Relation
import Mathlib.Data.Set.Card

namespace OPG169

universe u

abbrev Digraph (V : Type u) := V → V → Prop
abbrev Point := ℝ × ℝ

def pointOnSegment (a b : Point) (t : ℝ) : Point :=
  ((1 - t) * a.1 + t * b.1, (1 - t) * a.2 + t * b.2)

def closedSegment (a b : Point) : Set Point :=
  {x | ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧ x = pointOnSegment a b t}

/-- A straight-line planar embedding of the underlying simple graph. -/
def IsPlanar {V : Type u} (G : SimpleGraph V) : Prop :=
  ∃ p : V → Point,
    Function.Injective p ∧
    (∀ ⦃a b v : V⦄, G.Adj a b → v ≠ a → v ≠ b → p v ∉ closedSegment (p a) (p b)) ∧
    (∀ ⦃a b c d : V⦄, G.Adj a b → G.Adj c d →
      a ≠ c → a ≠ d → b ≠ c → b ≠ d →
      Disjoint (closedSegment (p a) (p b)) (closedSegment (p c) (p d)))

/-- `D` chooses exactly one direction for every edge of `G` and no arcs for
nonedges. -/
def IsOrientationOf {V : Type u} (D : Digraph V) (G : SimpleGraph V) : Prop :=
  (∀ v : V, ¬ D v v) ∧
  (∀ ⦃u v : V⦄, D u v → G.Adj u v) ∧
  ∀ ⦃u v : V⦄, G.Adj u v →
    (D u v ∨ D v u) ∧ ¬ (D u v ∧ D v u)

/-- A list of at least two distinct vertices joined cyclically by directed
arcs. In an orientation of a simple graph such a cycle necessarily has at
least three vertices. -/
def IsDirectedCycle {V : Type u} (D : Digraph V) (vs : List V) : Prop :=
  ∃ x y : V, ∃ middle : List V,
    vs = x :: (middle ++ [y]) ∧ 3 ≤ vs.length ∧
    vs.Nodup ∧ vs.Chain' D ∧ D y x

/-- The vertices of one color induce an acyclic digraph. -/
def ColorClassAcyclic {V : Type u} (D : Digraph V)
    (color : V → Fin 2) (k : Fin 2) : Prop :=
  ¬ ∃ vs : List V,
    IsDirectedCycle D vs ∧ ∀ v ∈ vs, color v = k

/-- A two-coloring in which both full induced color classes are acyclic.
Either color may be unused. -/
def IsAcyclicTwoColoring {V : Type u} (D : Digraph V)
    (color : V → Fin 2) : Prop :=
  ∀ k : Fin 2, ColorClassAcyclic D color k

def HasAcyclicTwoColoring {V : Type u} (D : Digraph V) : Prop :=
  ∃ color : V → Fin 2, IsAcyclicTwoColoring D color

/-- Nonempty strong connectivity under directed reachability. -/
def IsStronglyConnected {V : Type u} (D : Digraph V) : Prop :=
  Nonempty V ∧ ∀ u v : V, Relation.ReflTransGen D u v

/-- A counterexample of least vertex order among all finite planar
orientations in the same universe. -/
def IsLeastOrderCounterexample {V : Type u} [Fintype V]
    (G : SimpleGraph V) (D : Digraph V) : Prop :=
  IsPlanar G ∧ IsOrientationOf D G ∧ ¬ HasAcyclicTwoColoring D ∧
  ∀ (W : Type u) [Fintype W] (H : SimpleGraph W) (E : Digraph W),
    IsPlanar H → IsOrientationOf E H →
    Fintype.card W < Fintype.card V → HasAcyclicTwoColoring E

/-- Every vertex of the underlying graph has degree at least three. -/
def HasMinimumDegreeThree {V : Type u} (G : SimpleGraph V) : Prop :=
  ∀ v : V, 3 ≤ (G.neighborSet v).encard

end OPG169

Source

Open Problem Garden / UnsolvedMath OPG-169, https://www.unsolvedmath.com/problems/OPG-169; critical-digraph comparison: Mohar, Eigenvalues and colorings of digraphs, Section 2, https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf

Read-back

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

Digraph. For a type $V$ , a digraph $D$ on $V$ is a binary relation: for vertices $u,v\in V$ , $D(u,v)$ means there is a directed arc from $u$ to $v$ .

Point and segment definitions. A point is an ordered pair of real numbers. For points $a=(a_1,a_2)$ and $b=(b_1,b_2)$ and a real number $t$ , pointOnSegment is the point $((1-t)a_1+tb_1,(1-t)a_2+tb_2)$ . The closed segment from $a$ to $b$ is the set of points $x$ for which there exists a real $t$ with $0\le t\le 1$ and $x=((1-t)a_1+tb_1,(1-t)a_2+tb_2)$ .

Planarity. For a simple graph $G$ on a type $V$ , IsPlanar G means that there exists an injective map $p:V\to\mathbb R^2$ such that: whenever $a$ and $b$ are adjacent in $G$ and $v$ is different from both $a$ and $b$ , $p(v)$ does not lie on the closed segment from $p(a)$ to $p(b)$ ; and whenever $a$ is adjacent to $b$ , $c$ is adjacent to $d$ , and $a\ne c$ , $a\ne d$ , $b\ne c$ , and $b\ne d$ , the closed segments from $p(a)$ to $p(b)$ and from $p(c)$ to $p(d)$ are disjoint.

Orientation. IsOrientationOf D G means that $D$ has no loops, every directed arc of $D$ joins adjacent vertices of $G$ , and for every edge joining $u$ and $v$ , exactly one of $D(u,v)$ and $D(v,u)$ holds.

Directed cycle. IsDirectedCycle D vs means that there exist vertices $x,y$ and a list middle such that $vs=x$ followed by the elements of middle and then $y$ , that $vs$ has length at least $3$ , that no vertex occurs more than once in $vs$ , that every consecutive pair of vertices in $vs$ is joined by a directed arc of $D$ , and that $D(y,x)$ holds.

Acyclic color classes. Given a digraph $D$ , a coloring $color:V\to\mathrm{Fin}\,2$ and a color $k\in\mathrm{Fin}\,2$ , ColorClassAcyclic D color k means that there is no directed cycle all of whose vertices receive color $k$ . IsAcyclicTwoColoring D color means this holds for each of the two colors, and HasAcyclicTwoColoring D means that at least one coloring $color:V\to\mathrm{Fin}\,2$ has this property; either color is allowed to be unused.

Strong connectivity. IsStronglyConnected D means that $V$ is nonempty and, for every pair of vertices $u,v$ , there is a finite directed walk from $u$ to $v$ using zero or more arcs of $D$ ; in particular, walks of length zero are allowed.

Least-order counterexample. For a type $V$ equipped with a finite-type structure, a simple graph $G$ on $V$ and a digraph $D$ on $V$ , IsLeastOrderCounterexample G D means that $G$ is planar, $D$ is an orientation of $G$ , $D$ has no acyclic two-coloring, and, for every type $W$ in the same universe equipped with a finite-type structure, every simple graph $H$ on $W$ , and every digraph $E$ on $W$ , if $H$ is planar, $E$ is an orientation of $H$ , and the finite cardinality of $W$ is strictly smaller than that of $V$ , then $E$ has an acyclic two-coloring.

Minimum degree. HasMinimumDegreeThree G means that every vertex $v$ has a neighbor set in $G$ whose cardinality is at least $3$ .

Human review

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

View graph