Connectivity of directed graphs

DefinitionDirected paths#✓fully proved

A directed path in a digraph \(D\) is a finite, possibly empty, sequence of vertices of \(D\) with no vertex repeated in which each vertex is joined to the next by an arc of \(D\).

def IsDirectedPath {V : Type} (D : Digraph V) (p : List V) : Prop :=
  p.Nodup ∧ p.IsChain D.Adj

Used by 1

Used byInternally disjoint directed paths

DefinitionInternal vertices of a path#✓fully proved

The internal vertices of a path given as a vertex list (all but the first and the last).

def internalVertices {V : Type} (p : List V) : List V :=
  p.tail.dropLast

Used by 1

Used byInternally disjoint directed paths

DefinitionInternally disjoint directed paths#✓fully proved

Let \(D\) be a digraph, \(r\) a natural number and \(y\), \(x\) vertices of \(D\). We write \(\kappa(y, x) \ge r\) when there are \(r\) pairwise distinct directed paths in \(D\) from \(y\) to \(x\), no two of which share an internal vertex. Here a directed path from \(y\) to \(x\) is a sequence of distinct vertices starting at \(y\) and ending at \(x\) in which each vertex is joined to the next by an arc of \(D\), and its internal vertices are all its vertices except the first and the last.

def HasInternallyDisjointPaths {V : Type} (D : Digraph V) (r : ℕ) (y x : V) : Prop :=
  ∃ P : Fin r → List V,
    (∀ i, IsDirectedPath D (P i) ∧ (P i).head? = some y ∧ (P i).getLast? = some x) ∧
      ∀ i j, i ≠ j → P i ≠ P j ∧ ∀ v ∈ internalVertices (P i), v ∉ internalVertices (P j)

Uses 2 · Used by 1

Statement usesDirected paths · Internal vertices of a path

Used byHamidoune's reverse-connectivity conjecture for some \(r \ge 3\)

DefinitionHamidoune's reverse-connectivity conjecture for some \(r \ge 3\)#✓fully proved

The statement that there is a natural number \(r \ge 3\) such that every digraph \(D\) without loops or parallel arcs on a finite nonempty vertex set, in which every vertex has at least \(r\) out-neighbours and at least \(r\) in-neighbours, has an arc \((x, y)\) from \(x\) to \(y\) with \(\kappa(y, x) \ge r\), that is, with \(r\) pairwise distinct directed paths from \(y\) to \(x\), no two of which share an internal vertex. Here a directed path is a sequence of distinct vertices in which each vertex is joined to the next by an arc, and its internal vertices are all its vertices except the first and the last.

def hamidouneSomeRAtLeastThree : Prop :=
  ∃ r : ℕ, 3 ≤ r ∧ ∀ (V : Type) [Finite V] [Nonempty V] (D : Digraph V), (∀ v : V, ¬ D.Adj v v) →
    (∀ v : V, r ≤ {w | D.Adj v w}.ncard) → (∀ v : V, r ≤ {u | D.Adj u v}.ncard) →
      ∃ x y : V, D.Adj x y ∧ HasInternallyDisjointPaths D r y x

Uses 1 · Used by 1

Statement usesInternally disjoint directed paths

Used byHamidoune's reverse-connectivity conjecture fails for every \(r \ge 3\)

TheoremHamidoune's reverse-connectivity conjecture fails for every \(r \ge 3\)#●ready to prove

For no natural number \(r \ge 3\) does the following hold: every digraph \(D\) without loops or parallel arcs on a finite nonempty vertex set, in which every vertex has at least \(r\) out-neighbours and at least \(r\) in-neighbours, has an arc \((x, y)\) from \(x\) to \(y\) with \(\kappa(y, x) \ge r\), that is, with \(r\) pairwise distinct directed paths from \(y\) to \(x\), no two of which share an internal vertex. Here a directed path is a sequence of distinct vertices in which each vertex is joined to the next by an arc, and its internal vertices are all its vertices except the first and the last.

Thomassen constructed, for every positive integer \(r\), a digraph without digons with minimum out-degree and minimum in-degree at least \(r\) in which no arc \((x, y)\) has \(\kappa(y, x) \ge 3\); the report notes after Conjecture 6.21 that this is a counterexample for all \(r \ge 3\).

public theorem_wanted hamidouneSomeRAtLeastThree_refuted : ¬ hamidouneSomeRAtLeastThree

Sources

• B. D. Sullivan, A Summary of Problems and Results related to the Caccetta-Haggkvist Conjecture, arXiv:math/0605646, Conjecture 6.21; resolution: C. Thomassen, Even cycles in directed graphs, European J. Combin. 6 (1985) 85-89, as stated in the report's Theorem 5.2 (part ii) and the note after Conjecture 6.21, https://doi.org/10.1016/S0195-6698(85)80025-1.

Uses 1

Statement usesHamidoune's reverse-connectivity conjecture for some \(r \ge 3\)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.