Modular orientations

DefinitionEdges crossing a cut#✓fully proved

Consider a multigraph with vertex set \(V\) and edge set \(E\) in which each edge has a first and a second endpoint. For a set \(S \subseteq V\), an edge crosses the cut at \(S\) when exactly one of its two endpoints lies in \(S\).

def CrossesCut {V E : Type} (end₁ end₂ : E → V) (S : Set V) (e : E) : Prop :=
  (end₁ e ∈ S ∧ end₂ e ∉ S) ∨ (end₁ e ∉ S ∧ end₂ e ∈ S)

Used by 1

Used bySize of a cut

DefinitionSize of a cut#✓fully proved

Consider a multigraph with finitely many edges in which each edge has a first and a second endpoint. For a set \(S\) of vertices, the size of the cut at \(S\) is the number of edges crossing it, that is, having exactly one endpoint in \(S\). Distinct parallel edges are counted separately.

noncomputable def cutSize {V E : Type} [Fintype E]
    (end₁ end₂ : E → V) (S : Set V) : ℕ := by
  classical
  exact (Finset.univ.filter (CrossesCut end₁ end₂ S)).card

Uses 1 · Used by 1

Statement usesEdges crossing a cut

Used by4k-edge-connected multigraphs

Definition4k-edge-connected multigraphs#✓fully proved

For a natural number \(k\), a finite multigraph is \(4k\)-edge-connected when it has at least two vertices and, for every set \(S\) of vertices such that both \(S\) and its complement are nonempty, at least \(4k\) edges cross the cut at \(S\), that is, have exactly one endpoint in \(S\). Parallel edges are counted separately. For \(k \ge 1\) the condition implies that the multigraph is connected.

noncomputable def IsFourKEdgeConnected {V E : Type} [Fintype V] [Fintype E]
    (k : ℕ) (end₁ end₂ : E → V) : Prop :=
  2 ≤ Fintype.card V ∧
    ∀ S : Set V, S.Nonempty → Sᶜ.Nonempty → 4 * k ≤ cutSize end₁ end₂ S

Uses 1 · Used by 1

Statement usesSize of a cut

Used byJaeger's modular orientation conjecture

DefinitionTail of an oriented edge#✓fully proved

Each edge \(e\) of the multigraph has a reference direction from its first endpoint to its second endpoint, and an orientation chooses for each edge whether to reverse it. The tail of \(e\) is its first endpoint if \(e\) is not reversed and its second endpoint if \(e\) is reversed.

def orientedTail {V E : Type} (end₁ end₂ : E → V)
    (isReversed : E → Bool) (e : E) : V :=
  if isReversed e = true then end₂ e else end₁ e

Used by 1

Used byOutdegree

DefinitionHead of an oriented edge#✓fully proved

Each edge \(e\) of the multigraph has a reference direction from its first endpoint to its second endpoint, and an orientation chooses for each edge whether to reverse it. The head of \(e\) is its second endpoint if \(e\) is not reversed and its first endpoint if \(e\) is reversed.

def orientedHead {V E : Type} (end₁ end₂ : E → V)
    (isReversed : E → Bool) (e : E) : V :=
  if isReversed e = true then end₁ e else end₂ e

Used by 1

Used byIndegree

DefinitionIndegree#✓fully proved

In a multigraph with finitely many edges and a chosen orientation, the indegree of a vertex \(v\) is the number of edges whose head is \(v\), parallel edges counted separately.

noncomputable def indegree {V E : Type} [Fintype E]
    (end₁ end₂ : E → V) (isReversed : E → Bool) (v : V) : ℕ := by
  classical
  exact (Finset.univ.filter (fun e => orientedHead end₁ end₂ isReversed e = v)).card

Uses 1 · Used by 1

Statement usesHead of an oriented edge

Used byModular orientations

DefinitionOutdegree#✓fully proved

In a multigraph with finitely many edges and a chosen orientation, the outdegree of a vertex \(v\) is the number of edges whose tail is \(v\), parallel edges counted separately.

noncomputable def outdegree {V E : Type} [Fintype E]
    (end₁ end₂ : E → V) (isReversed : E → Bool) (v : V) : ℕ := by
  classical
  exact (Finset.univ.filter (fun e => orientedTail end₁ end₂ isReversed e = v)).card

Uses 1 · Used by 1

Statement usesTail of an oriented edge

Used byModular orientations

DefinitionModular orientations#✓fully proved

For a natural number \(k\), an orientation of a multigraph with finitely many edges is a modulo \((2k+1)\) orientation when at every vertex the indegree minus the outdegree is congruent to \(0\) modulo \(2k + 1\).

noncomputable def IsModularOrientation {V E : Type} [Fintype E]
    (k : ℕ) (end₁ end₂ : E → V) (isReversed : E → Bool) : Prop :=
  ∀ v : V,
    (indegree end₁ end₂ isReversed v : ZMod (2 * k + 1)) -
        (outdegree end₁ end₂ isReversed v : ZMod (2 * k + 1)) = 0

Uses 2 · Used by 1

Statement usesIndegree · Outdegree

Used byJaeger's modular orientation conjecture

DefinitionJaeger's modular orientation conjecture#✓fully proved

This is the statement that for every integer \(k \ge 1\), every finite multigraph (loops and parallel edges allowed) that has at least two vertices, and in which every partition of the vertices into two nonempty sets is crossed by at least \(4k\) edges, admits an orientation of its edges in which, at every vertex, the indegree minus the outdegree is divisible by \(2k + 1\).

The parameter \(k\) is positive, as in the source discussion of \((2 + 1/k)\)-flows and its specializations at \(k = 1\) and \(k = 2\).

def conjecture : Prop :=
  ∀ (k : ℕ), 0 < k →
    ∀ (V E : Type) [Fintype V] [Fintype E] (end₁ end₂ : E → V),
      IsFourKEdgeConnected k end₁ end₂ →
        ∃ isReversed : E → Bool, IsModularOrientation k end₁ end₂ isReversed

Uses 2 · Used by 1

Statement uses4k-edge-connected multigraphs · Modular orientations

Used byJaeger's modular orientation conjecture is false

TheoremJaeger's modular orientation conjecture is false#●ready to prove

There exist an integer \(k \ge 1\) and a finite multigraph (loops and parallel edges allowed) with at least two vertices, in which every partition of the vertices into two nonempty sets is crossed by at least \(4k\) edges, such that no orientation of the edges makes the indegree minus the outdegree of every vertex divisible by \(2k + 1\).

Han, Li, Wu and Zhang (J. Combin. Theory Ser. B 131 (2018) 1-11) construct, for every \(k \ge 3\), a \(4k\)-edge-connected graph with no circular \((2+1/k)\)-flow, equivalently no modulo \((2k+1)\) orientation; the cases \(k = 1\) (Tutte's 3-flow conjecture) and \(k = 2\) remain open.

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Daniel W. Cranston and Jiaao Li, Circular flows in planar graphs, SIAM J. Discrete Math. (2020), arXiv:1812.09833, https://arxiv.org/abs/1812.09833.

Uses 1

Statement usesJaeger's modular orientation conjecture

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.