The orientation reversal calculus

This file develops reversal of sets of edges of a CFOrientation, the two fundamental moves given by directed cycles and directed cuts, and Gioan's theorem relating reversal classes to linear equivalence of orientation divisors.

Contents

1. reverseOn — reverse every edge whose directed pair satisfies a predicate, with the flow and indeg bookkeeping (flow_reverseOn, indeg_reverseOn). This is the coarse move: a predicate on vertex pairs can only turn a whole parallel class at once.
2. DirectedCycle, and the two cycle reversals.
   • reverseCycle (coarse) turns the whole parallel class at each step. indeg_reverseCycle_vert and indeg_reverseCycle_of_notMem are its exact bookkeeping; ordiv_reverseCycle gives equality of ordiv only under a balance hypothesis, and ordiv_reverseCycle_of_simple discharges that hypothesis for simple graphs.
   • reverseCycleOne (fine) turns exactly one edge at each step — the classical move. It preserves every in-degree unconditionally (indeg_reverseCycleOne), hence ordiv (ordiv_reverseCycleOne). DirectedCycle.reversed / .reversedOne say the reversed cycle is again a directed cycle, so "has a directed cycle" survives either reversal.
3. eq_of_indeg_eq_of_isAcyclic — the strengthened uniqueness: if O is acyclic and indeg O = indeg O' pointwise then O = O'. isAcyclic_iff_unique_of_indeg packages it as "an orientation is acyclic iff it is the unique orientation with its indegree function", where the ← direction assumes only that O has no directed 2-cycle.
4. isAcyclic_reverseCut — reversing a directed cut takes acyclic orientations to acyclic ones.
5. ReversalStep / ReversalEquiv, isAcyclic_of_reversalEquiv, and gioan_reversalEquiv_of_linear_equiv — Gioan's theorem, proved. Its two halves are reversalEquiv_of_indeg_eq (the fine cycle move handles a difference of divergence zero) and reversalEquiv_of_potential (the cut move handles the rest); diffFlow is the signed difference vector both of them read, and isDirectedCut_compl_of_min is the one real idea — see the header of "Step 2" below.
6. winnable_ordiv_of_not_isAcyclic and isAcyclic_iff_not_winnable_ordiv, derived from 2+4+5 and unwinnable_iff_exists_acyclic_ordiv.

The path combinatorics is confined to exists_isChain_of_backward_step: a nonempty set of vertices each of which is the head of an edge from another member forces arbitrarily long chains, hence a repeat. It is used three times, for 2, for 3, and for 5.

The edge-level orientation model

CFOrientation used to carry a field no_bidirectional forbidding two parallel edges to point in opposite directions, so an orientation in that model turned each parallel class as a block. Dependency pin 4f06d84 removed it; CFOrientation is now an arbitrary edge-level orientation, i.e. any flow-count vector satisfying count_preserving. Three consequences, all of them realised in this file:

• DirectedCycle now allows two vertices (Fin (len + 2), not Fin (len + 3)): a parallel class with one edge each way is a directed 2-cycle. Only looplessness rules out one-vertex cycles. Both reverseCycle_ne and reverseCycleOne_ne consequently need 1 ≤ C.len: on a 2-cycle the coarse move swaps the two flow counts and the fine move removes and restores one unit each way, so both can return O itself.
• The fine cycle reversal exists, and it is what makes ordiv preservation unconditional. The old "multi-edge caveat" — cycle reversal changes indegrees by the class multiplicity, so ordiv_reverseCycle needs a balance hypothesis — applies to the coarse move only, and the coarse move is now a curiosity rather than the only option.
• isAcyclic_iff_unique_of_indeg no longer needs simplicity, only the absence of a directed 2-cycle; see its docstring for why that residue is not removable.

0. Helpers re-derived from Orientation.lean

Orientation.lean keeps eq_orient, opp_flow, indeg_eq_sum_flow and count_of_multiset_of_count private, so the four facts are re-proved here (same proofs, public names). They are the whole interface this file needs to the flow model.

theorem Utilities.count_multiset_of_count {T : Type u_1} [DecidableEq T] [Fintype T] (f : T → ℕ) (e : T) : Multiset.count e (multisetOfCount f) = f e

multisetOfCount f has count function f. Public re-proof of the private count_of_multiset_of_count of Orientation.lean.

theorem Utilities.flow_orientation_from_flow {G : CFGraph} (f : G.V × G.V → ℕ) (h₁ : ∀ (v w : G.V), f (v, w) + f (w, v) = numEdges G v w) (u v : G.V) : flow (orientationFromFlow f h₁) u v = f (u, v)

The flow of orientationFromFlow f _ is f.

theorem Utilities.orientation_ext {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ∀ (u v : G.V), flow O₁ u v = flow O₂ u v) : O₁ = O₂

Two orientations agreeing on every flow are equal. Public re-proof of the private eq_orient of Orientation.lean.

theorem Utilities.flow_add_flow_rev {G : CFGraph} (O : CFOrientation G) (u v : G.V) : flow O u v + flow O v u = numEdges G u v

The two flows on an undirected edge add up to its multiplicity. Public re-proof of the private opp_flow of Orientation.lean.

theorem Utilities.indeg_eq_sum_flow {G : CFGraph} (O : CFOrientation G) (v : G.V) : indeg G O v = ∑ w : G.V, flow O w v

The in-degree is the total flow into the vertex. Public re-proof of the private indeg_eq_sum_flow of Orientation.lean, by a shorter route (count the filtered multiset pairwise rather than by induction).

theorem Utilities.directed_edge_iff_flow_pos {G : CFGraph} (O : CFOrientation G) (u v : G.V) : directedEdge G O u v ↔ 0 < flow O u v

A directed edge is exactly a pair carrying positive flow.

theorem Utilities.not_directed_edge_self {G : CFGraph} (O : CFOrientation G) (v : G.V) : ¬directedEdge G O v v

No directed loop: G is loopless, so numEdges G v v = 0 and no orientation can carry an edge from v to itself. This is what rules out one-vertex directed cycles.

def Utilities.HasDirectedTwoCycle {G : CFGraph} (O : CFOrientation G) : Prop

A directed 2-cycle: O sends an edge from u to v and another back from v to u. Since the removal of CFOrientation.no_bidirectional from the dependency this is a legal configuration on a parallel class, and it is exactly what the two-vertex directed cycles are.

Equations

• Utilities.HasDirectedTwoCycle O = ∃ (u : G.V) (v : G.V), directedEdge G O u v ∧ directedEdge G O v u

1. Reversing a set of edges

reverseOn O S reverses every edge of O whose directed pair (u, v) satisfies S u v. This is the coarse move: it turns a whole parallel class at once, since S can only see the vertex pair. reverseCycleOne below is the fine move that turns a single edge of each class; see the module docstring for which one is load-bearing where.

def Utilities.reverseFlow {G : CFGraph} (O : CFOrientation G) (S : G.V → G.V → Prop) [DecidableRel S] : G.V × G.V → ℕ

The flow function of reverseOn O S: the edges of the class (u,v) survive unless S u v, and the class (v,u) is added in when S v u.

Equations

• Utilities.reverseFlow O S e = (if S e.1 e.2 then 0 else flow O e.1 e.2) + if S e.2 e.1 then flow O e.2 e.1 else 0

theorem Utilities.reverseFlow_count_preserving {G : CFGraph} (O : CFOrientation G) (S : G.V → G.V → Prop) [DecidableRel S] (u v : G.V) : reverseFlow O S (u, v) + reverseFlow O S (v, u) = numEdges G u v

reverseFlow still saturates every edge multiplicity: each parallel class contributes its full count to exactly one of the two directions.

def Utilities.reverseOn {G : CFGraph} (O : CFOrientation G) (S : G.V → G.V → Prop) [DecidableRel S] : CFOrientation G

Reversing an edge set. reverseOn O S is O with every edge whose directed pair satisfies S turned around.

Equations

• Utilities.reverseOn O S = orientationFromFlow (Utilities.reverseFlow O S) ⋯

theorem Utilities.flow_reverseOn {G : CFGraph} (O : CFOrientation G) (S : G.V → G.V → Prop) [DecidableRel S] (u v : G.V) : flow (reverseOn O S) u v = (if S u v then 0 else flow O u v) + if S v u then flow O v u else 0

The defining flow identity for reverseOn.

theorem Utilities.reverseOn_bot {G : CFGraph} (O : CFOrientation G) : (reverseOn O fun (x x_1 : G.V) => False) = O

Reversing nothing changes nothing.

theorem Utilities.indeg_reverseOn {G : CFGraph} (O : CFOrientation G) (S : G.V → G.V → Prop) [DecidableRel S] (v : G.V) : ↑(indeg G (reverseOn O S) v) = (↑(indeg G O v) - ∑ w : G.V, if S w v then ↑(flow O w v) else 0) + ∑ w : G.V, if S v w then ↑(flow O v w) else 0

The indeg bookkeeping for a reversal. The in-degree of v loses the reversed edges pointing into v and gains the reversed edges pointing out of v.

theorem Utilities.exists_isChain_of_backward_step {V : Type u_1} {R : V → V → Prop} {P : V → Prop} (step : ∀ (v : V), P v → ∃ (u : V), P u ∧ R u v) {v₀ : V} (h₀ : P v₀) (k : ℕ) : ∃ (l : List V), l.length = k + 1 ∧ List.IsChain R l ∧ ∃ (a : V), l.head? = some a ∧ P a

Walking backwards produces arbitrarily long chains. If every member of P is the head of an R-edge from another member, then R-chains of every length exist, each headed by a member of P.

This is the one piece of path combinatorics the file needs, and it is used three times: to see that a directed cycle obstructs acyclicity (not_isAcyclic_of_backward_step), in eq_of_indeg_eq_of_isAcyclic (with P the set of tails of edges where two orientations disagree), and in nonempty_relCycle_of_backward_step, which is what turns the walk into an actual cycle.

theorem Utilities.not_isAcyclic_of_backward_step {G : CFGraph} {O : CFOrientation G} {P : G.V → Prop} (step : ∀ (v : G.V), P v → ∃ (u : G.V), P u ∧ directedEdge G O u v) {v₀ : G.V} (h₀ : P v₀) : ¬isAcyclic G O

The walk-backwards criterion for a directed cycle. If a nonempty set P of vertices has the property that every member is the head of a directed edge from another member, then O is not acyclic: walking backwards produces directed paths of every length, and a path longer than Fintype.card G.V cannot be non-repeating.

2. Cycle reversal

structure Utilities.DirectedCycle {G : CFGraph} (O : CFOrientation G) : Type u_1

A directed cycle of O: len + 2 distinct vertices, indexed cyclically by Fin (len + 2), with a directed edge from each to its successor.

Requiring at least two vertices is no restriction: G is loopless, so no directed cycle has one vertex. Two-vertex cycles (len = 0) are genuine and must be allowed — a parallel class with one edge each way is a directed 2-cycle, which the CFOrientation model represents since no_bidirectional was removed from the dependency. The bound was + 3 while that field existed.

• len : ℕ

  The cycle has len + 2 vertices.

• vert : Fin (self.len + 2) → G.V

  The vertices of the cycle, indexed cyclically.

• vert_inj : Function.Injective self.vert

  The vertices are distinct.

• edge (i : Fin (self.len + 2)) : directedEdge G O (self.vert i) (self.vert (i + 1))

  Consecutive vertices carry a directed edge of O.

def Utilities.DirectedCycle.pred {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) : G.V → G.V → Prop

The set of directed pairs traversed by a directed cycle.

Equations

• C.pred u v = ∃ (i : Fin (C.len + 2)), u = C.vert i ∧ v = C.vert (i + 1)

@[instance_reducible]

instance Utilities.DirectedCycle.instDecidableRelVPred {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) : DecidableRel C.pred

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.DirectedCycle.edge_pred {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) (i : Fin (C.len + 2)) : directedEdge G O (C.vert (i - 1)) (C.vert i)

The predecessor of a cycle vertex along the cycle.

theorem Utilities.DirectedCycle.pred_into {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) (w : G.V) (j : Fin (C.len + 2)) : C.pred w (C.vert j) ↔ w = C.vert (j - 1)

The pairs of C ending at a cycle vertex: only the predecessor edge.

theorem Utilities.DirectedCycle.pred_outOf {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) (w : G.V) (j : Fin (C.len + 2)) : C.pred (C.vert j) w ↔ w = C.vert (j + 1)

The pairs of C starting at a cycle vertex: only the successor edge.

theorem Utilities.DirectedCycle.not_pred_of_notMem {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) {v : G.V} (hv : ∀ (i : Fin (C.len + 2)), v ≠ C.vert i) (w : G.V) : ¬C.pred w v ∧ ¬C.pred v w

A vertex off the cycle meets none of the cycle's pairs.

theorem Utilities.DirectedCycle.flow_pos_of_pred {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) {u v : G.V} (h : C.pred u v) : 0 < flow O u v

Every pair traversed by the cycle carries positive flow.

theorem Utilities.DirectedCycle.not_pred_succ_zero {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) (hlen : 1 ≤ C.len) : ¬C.pred (C.vert (0 + 1)) (C.vert 0)

On a cycle of at least three vertices the first step is not also traversed backwards. This is what fails for a len = 0 cycle, where the two steps are each other's reverse.

theorem Utilities.DirectedCycle.hasDirectedTwoCycle_of_len_eq_zero {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) (h : C.len = 0) : HasDirectedTwoCycle O

A cycle with len = 0 has exactly two vertices, and its two steps are a directed 2-cycle of O.

theorem Utilities.not_isAcyclic_of_directedCycle {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) : ¬isAcyclic G O

An orientation carrying a directed cycle is not acyclic.

Cycles of an arbitrary relation

DirectedCycle O is the case R = directedEdge G O of RelCycle R. The generality is needed exactly once, and it is essential there: reversalEquiv_of_indeg_eq finds its cycle in the relation "O₁ carries strictly more flow than O₂", which is smaller than directedEdge G O₁, and the extra information — that every step of the cycle is a step where the two orientations disagree — is what makes the flow bookkeeping close.

structure Utilities.RelCycle {V : Type u_1} (R : V → V → Prop) : Type u_1

A cycle of a relation R: len + 2 distinct vertices, indexed cyclically, with R holding from each to its successor. DirectedCycle O is RelCycle (directedEdge G O) with a bespoke name.

• len : ℕ

  The cycle has len + 2 vertices.

• vert : Fin (self.len + 2) → V

  The vertices of the cycle, indexed cyclically.

• vert_inj : Function.Injective self.vert

  The vertices are distinct.

• edge (i : Fin (self.len + 2)) : R (self.vert i) (self.vert (i + 1))

  Consecutive vertices are R-related.

def Utilities.RelCycle.op {V : Type u_1} {R : V → V → Prop} (C : RelCycle fun (u v : V) => R v u) : RelCycle R

A cycle of the opposite relation, read backwards, is a cycle of R.

Equations

• C.op = { len := C.len, vert := fun (j : Fin (C.len + 2)) => C.vert (-j), vert_inj := ⋯, edge := ⋯ }

def Utilities.RelCycle.toDirectedCycle {G : CFGraph} {O : CFOrientation G} {R : G.V → G.V → Prop} (C : RelCycle R) (h : ∀ (u v : G.V), R u v → directedEdge G O u v) : DirectedCycle O

A cycle of a relation refining directedEdge G O is a directed cycle of O.

Equations

• C.toDirectedCycle h = { len := C.len, vert := C.vert, vert_inj := ⋯, edge := ⋯ }

theorem Utilities.nonempty_relCycle_of_repeat {V : Type u_1} [Nonempty V] {R : V → V → Prop} (hirr : ∀ (v : V), ¬R v v) (l : List V) (hchain : List.IsChain R l) (a b : ℕ) (hab : a < b) (hb : b < l.length) (heq : l[a] = l[b]) : Nonempty (RelCycle R)

A repeated vertex in an R-chain produces an R-cycle.

The whole construction, with no modular arithmetic beyond fin_val_succ: index the chain by f i = l.getD i v₀ and pick, by Nat.find, the shortest gap m + 1 over all repeats f c = f (c + (m + 1)) of the chain. Minimality makes f c, …, f (c + m) pairwise distinct — a shorter repeat inside that window would be a shorter gap — so they are the vertices of a cycle, closed up by f (c + (m + 1)) = f c. The gap is at least 2, because irreflexivity of R kills gap 1 — and that is the only exclusion needed, since RelCycle (like DirectedCycle) allows two-vertex cycles.

The construction extracts a finite cycle directly from the repeated segment of the chain.

theorem Utilities.nonempty_relCycle_of_backward_step {V : Type u_1} [Finite V] {R : V → V → Prop} (hirr : ∀ (v : V), ¬R v v) {P : V → Prop} (step : ∀ (v : V), P v → ∃ (u : V), P u ∧ R u v) {v₀ : V} (h₀ : P v₀) : Nonempty (RelCycle R)

Walking backwards inside a finite set produces a cycle. Combine exists_isChain_of_backward_step — which makes an R-chain longer than Fintype.card V — with nonempty_relCycle_of_repeat, which turns its unavoidable repeat into a cycle.

theorem Utilities.nonempty_relCycle_of_forward_step {V : Type u_1} [Finite V] {R : V → V → Prop} (hirr : ∀ (v : V), ¬R v v) {P : V → Prop} (step : ∀ (v : V), P v → ∃ (w : V), P w ∧ R v w) {v₀ : V} (h₀ : P v₀) : Nonempty (RelCycle R)

Walking forwards inside a finite set produces a cycle, the mirror image of nonempty_relCycle_of_backward_step obtained by running it on the opposite relation and reading the resulting cycle backwards (RelCycle.op).

theorem Utilities.nonempty_directedCycle_of_not_isAcyclic {G : CFGraph} (O : CFOrientation G) (h : ¬isAcyclic G O) : Nonempty (DirectedCycle O)

Every non-acyclic orientation carries a directed cycle, the converse of not_isAcyclic_of_directedCycle. Failure of acyclicity hands over a directed path with a repeated vertex; nonempty_directedCycle_of_repeat turns the shortest such repeat into a cycle, whose length is at least two because G is loopless.

def Utilities.reverseCycle {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) : CFOrientation G

Cycle reversal. Reverse every edge traversed by the directed cycle C.

Equations

• Utilities.reverseCycle O C = Utilities.reverseOn O C.pred

def Utilities.DirectedCycle.reversed {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) : DirectedCycle (reverseCycle O C)

The reversed cycle is again a directed cycle, now of reverseCycle O C. Hence "has a directed cycle" is preserved by cycle reversal — which is what makes the reversal class of an acyclic orientation consist of acyclic orientations.

Equations

• C.reversed = { len := C.len, vert := fun (j : Fin (C.len + 2)) => C.vert (-j), vert_inj := ⋯, edge := ⋯ }

theorem Utilities.indeg_reverseCycle_vert {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (j : Fin (C.len + 2)) : ↑(indeg G (reverseCycle O C) (C.vert j)) = ↑(indeg G O (C.vert j)) - ↑(flow O (C.vert (j - 1)) (C.vert j)) + ↑(flow O (C.vert j) (C.vert (j + 1)))

The indeg bookkeeping at a vertex on the cycle: it loses the predecessor edge class and gains the successor edge class.

theorem Utilities.indeg_reverseCycle_of_notMem {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) {v : G.V} (hv : ∀ (i : Fin (C.len + 2)), v ≠ C.vert i) : indeg G (reverseCycle O C) v = indeg G O v

The indeg bookkeeping at a vertex off the cycle: nothing changes.

theorem Utilities.ordiv_reverseCycle {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (hbal : ∀ (i : Fin (C.len + 2)), flow O (C.vert (i - 1)) (C.vert i) = flow O (C.vert i) (C.vert (i + 1))) : ordiv G (reverseCycle O C) = ordiv G O

Cycle reversal preserves ordiv exactly, under the balance hypothesis that the edge multiplicity is constant around the cycle.

The hypothesis is an artefact of the coarse move, which reverses a whole parallel class at each step: the indegree at a cycle vertex then moves by the class multiplicity rather than by one. It holds whenever G is simple (ordiv_reverseCycle_of_simple), and it is vacuous for the fine move, which preserves ordiv outright (ordiv_reverseCycleOne).

theorem Utilities.ordiv_reverseCycle_of_simple {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (hsimple : ∀ (u v : G.V), numEdges G u v ≤ 1) : ordiv G (reverseCycle O C) = ordiv G O

On a simple graph the balance hypothesis of ordiv_reverseCycle is automatic: every edge class traversed by the cycle has multiplicity exactly one.

theorem Utilities.reverseCycle_ne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (hlen : 1 ≤ C.len) : reverseCycle O C ≠ O

A cycle reversal genuinely changes the orientation — provided the cycle has at least three vertices (1 ≤ C.len).

The restriction is not removable, and it is the price of the widened CFOrientation model. A len = 0 cycle is a parallel class u ⇄ v carrying flow in both directions; reverseCycle turns the whole class each way at once, i.e. it swaps flow O u v with flow O v u, so on a 2-banana oriented one edge each way it gives back exactly O. With three or more vertices the first step's reverse is not itself a step of the cycle (DirectedCycle.not_pred_succ_zero), so its flow really does drop to zero.

The fine cycle reversal

reverseCycle turns a whole parallel class at every step of the cycle, because reverseOn sees only the vertex pair. reverseCycleOne turns exactly one edge at every step, which is the classical cycle-reversal move of the orientation calculus. It became representable only when no_bidirectional was removed from CFOrientation: splitting a parallel class is precisely what that field forbade. Unlike the coarse move it preserves indeg, and hence ordiv, with no hypothesis at all.

def Utilities.reverseCycleOneFlow {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) : G.V × G.V → ℕ

The flow function of the fine cycle reversal: move one unit of flow backwards along every step of C.

Equations

• Utilities.reverseCycleOneFlow O C e = (flow O e.1 e.2 - if C.pred e.1 e.2 then 1 else 0) + if C.pred e.2 e.1 then 1 else 0

theorem Utilities.reverseCycleOneFlow_count_preserving {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (u v : G.V) : reverseCycleOneFlow O C (u, v) + reverseCycleOneFlow O C (v, u) = numEdges G u v

reverseCycleOneFlow still saturates every edge multiplicity: a step of the cycle moves one unit from one direction to the other, and a pair traversed in both directions (only possible for a len = 0 cycle) loses and regains the same unit.

def Utilities.reverseCycleOne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) : CFOrientation G

Fine cycle reversal. Turn one edge of each parallel class traversed by C.

Equations

• Utilities.reverseCycleOne O C = orientationFromFlow (Utilities.reverseCycleOneFlow O C) ⋯

theorem Utilities.flow_reverseCycleOne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (u v : G.V) : flow (reverseCycleOne O C) u v = (flow O u v - if C.pred u v then 1 else 0) + if C.pred v u then 1 else 0

The defining flow identity for reverseCycleOne.

def Utilities.DirectedCycle.reversedOne {G : CFGraph} {O : CFOrientation G} (C : DirectedCycle O) : DirectedCycle (reverseCycleOne O C)

The reversed cycle is again a directed cycle, now of reverseCycleOne O C. The fine analogue of DirectedCycle.reversed.

Equations

• C.reversedOne = { len := C.len, vert := fun (j : Fin (C.len + 2)) => C.vert (-j), vert_inj := ⋯, edge := ⋯ }

theorem Utilities.indeg_reverseCycleOne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (v : G.V) : indeg G (reverseCycleOne O C) v = indeg G O v

The fine cycle reversal preserves every in-degree. At a cycle vertex it removes one unit of flow on the incoming step and adds one on the outgoing step; off the cycle nothing moves. No balance hypothesis is needed, in contrast to ordiv_reverseCycle.

theorem Utilities.ordiv_reverseCycleOne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) : ordiv G (reverseCycleOne O C) = ordiv G O

The fine cycle reversal preserves ordiv exactly, unconditionally. This is what the coarse ordiv_reverseCycle needs a balance hypothesis for.

theorem Utilities.reverseCycleOne_ne {G : CFGraph} (O : CFOrientation G) (C : DirectedCycle O) (hlen : 1 ≤ C.len) : reverseCycleOne O C ≠ O

A fine cycle reversal genuinely changes the orientation, again provided the cycle has at least three vertices. For a len = 0 cycle the move takes one edge out of each of the two directions of a parallel class and puts one back, so it is the identity.

3. Acyclicity as uniqueness of the indegree function

orientation_determined_by_indegrees in the dependency requires both orientations to be acyclic. Only one of them is really needed, and the proof of the dependency's lemma in fact never uses the second hypothesis — but the hypothesis is in its statement, so the stronger form is re-proved here from not_isAcyclic_of_backward_step.

The mathematical content: the signed set of edges on which O and O' disagree is a circulation (it preserves every indegree), so following disagreements backwards never terminates, which an acyclic O forbids.

theorem Utilities.eq_of_indeg_eq_of_isAcyclic {G : CFGraph} {O O' : CFOrientation G} (hO : isAcyclic G O) (h : ∀ (v : G.V), indeg G O v = indeg G O' v) : O = O'

Acyclic orientations are determined by their indegree function, with acyclicity assumed of only one of the two orientations. Strengthens orientation_determined_by_indegrees (Orientation.lean), which assumes both.

theorem Utilities.isAcyclic_iff_unique_of_indeg {G : CFGraph} (O : CFOrientation G) (hno2 : ¬HasDirectedTwoCycle O) : isAcyclic G O ↔ ∀ (O' : CFOrientation G), (∀ (v : G.V), indeg G O v = indeg G O' v) → O = O'

An orientation is acyclic iff it is the unique orientation with its indegree function — the clean restatement of eq_of_indeg_eq_of_isAcyclic.

→ is unconditional. ← needs a hypothesis, and the hypothesis is exactly "O has no directed 2-cycle" — strictly weaker than the simplicity hypothesis this theorem used to carry, and not removable:

• it is sufficient because a non-acyclic O then carries a directed cycle on at least three vertices, and the fine cycle reversal reverseCycleOne produces a different orientation with the same in-degrees (indeg_reverseCycleOne, reverseCycleOne_ne);
• it is necessary because on the 3-banana the orientation with two edges u → v and one edge v → u has in-degrees (1, 2), and no other orientation of that graph does — the three edges must split (2, 1) — yet it is cyclic. Note that both cycle reversals are useless here: reversing the 2-cycle finely takes one edge out of each direction and puts one back, and coarsely swaps the two counts, which changes the in-degrees.

Simplicity was the right hypothesis only while CFOrientation.no_bidirectional forced cycle reversal to turn whole parallel classes; with that field gone the fine move is available and the only obstruction left is the degenerate 2-cycle.

4. Cocycle (directed cut) reversal

def Utilities.IsDirectedCut {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) : Prop

W is a directed cut of O when every edge between W and its complement leaves W: there is no flow from outside W into W.

Equations

• Utilities.IsDirectedCut O W = ∀ (u v : G.V), u ∉ W → v ∈ W → flow O u v = 0

def Utilities.reverseCut {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) : CFOrientation G

Cocycle reversal. Turn every edge from W to its complement.

Equations

• Utilities.reverseCut O W = Utilities.reverseOn O fun (u v : G.V) => u ∈ W ∧ v ∉ W

theorem Utilities.flow_reverseCut_out {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) {u v : G.V} (hu : u ∈ W) (hv : v ∉ W) : flow (reverseCut O W) u v = 0

After the reversal no edge leaves W.

theorem Utilities.flow_reverseCut_in {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) (hcut : IsDirectedCut O W) {u v : G.V} (hu : u ∉ W) (hv : v ∈ W) : flow (reverseCut O W) u v = flow O v u

The edges that used to leave W now enter it.

theorem Utilities.flow_reverseCut_same {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) {u v : G.V} (h : u ∈ W ↔ v ∈ W) : flow (reverseCut O W) u v = flow O u v

Edges with both ends on the same side of the cut are untouched.

theorem Utilities.isDirectedCut_reverseCut {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) : IsDirectedCut (reverseCut O W) Wᶜ

After reversing the directed cut at W, the complement of W is a directed cut.

theorem Utilities.reverseCut_reverseCut {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) (hcut : IsDirectedCut O W) : reverseCut (reverseCut O W) Wᶜ = O

Cocycle reversal is undone by reversing the complementary cut, so the move is symmetric.

theorem Utilities.isAcyclic_reverseCut {G : CFGraph} (O : CFOrientation G) (W : Finset G.V) (hO : isAcyclic G O) : isAcyclic G (reverseCut O W)

Cocycle reversal preserves acyclicity. A directed path of reverseCut O W first runs outside W and then, once it enters W, stays there — because after the reversal no edge leaves W. Each of the two stretches lies on one side of the cut, where the reversed orientation agrees with O, so each is a directed path of the acyclic O and is therefore non-repeating; and the two stretches are disjoint, being on opposite sides of W.

5. The reversal equivalence and Gioan's theorem

def Utilities.ReversalStep {G : CFGraph} (O₁ O₂ : CFOrientation G) : Prop

One reversal move: turn a directed cycle — finely (reverseCycleOne, one edge at each step, the classical move) or coarsely (reverseCycle, the whole parallel class at each step) — or turn a directed cut. Each in either direction; the relation is symmetric by construction, which is all the ← disjuncts are for.

Both cycle moves are included deliberately. The fine one is the move Gioan's theorem is about, and it is the only one gioan_reversalEquiv_of_linear_equiv actually uses; the coarse one is kept because it costs nothing — isAcyclic_of_reversalStep rules out any cycle reversal at an acyclic orientation — and a larger step relation only makes an implication into ReversalEquiv easier. Concretely, the proof of Gioan's theorem below reaches for exactly two of the six disjuncts: the forward fine cycle reversal and the forward cut reversal.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.ReversalStep.symm {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ReversalStep O₁ O₂) : ReversalStep O₂ O₁

Reversal moves are symmetric.

def Utilities.ReversalEquiv {G : CFGraph} (O₁ O₂ : CFOrientation G) : Prop

Two orientations are reversal equivalent when a finite sequence of cycle and cocycle reversals turns one into the other.

Equations

• Utilities.ReversalEquiv O₁ O₂ = Relation.ReflTransGen Utilities.ReversalStep O₁ O₂

theorem Utilities.ReversalEquiv.refl {G : CFGraph} (O : CFOrientation G) : ReversalEquiv O O

theorem Utilities.ReversalEquiv.symm {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ReversalEquiv O₁ O₂) : ReversalEquiv O₂ O₁

theorem Utilities.ReversalEquiv.trans {G : CFGraph} {O₁ O₂ O₃ : CFOrientation G} (h₁ : ReversalEquiv O₁ O₂) (h₂ : ReversalEquiv O₂ O₃) : ReversalEquiv O₁ O₃

theorem Utilities.isAcyclic_of_reversalStep {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ReversalStep O₁ O₂) (hO₁ : isAcyclic G O₁) : isAcyclic G O₂

A single reversal move out of an acyclic orientation lands on an acyclic orientation. A cycle reversal of either kind is simply unavailable at an acyclic orientation: in the forward direction there is no directed cycle to turn, and in the backward direction the reversed cycle (DirectedCycle.reversed, DirectedCycle.reversedOne) would be a directed cycle of the acyclic orientation we started from. A cocycle reversal preserves acyclicity by isAcyclic_reverseCut, in either direction because reverseCut_reverseCut exhibits the inverse move as another cocycle reversal.

theorem Utilities.isAcyclic_of_reversalEquiv {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ReversalEquiv O₁ O₂) (hO₁ : isAcyclic G O₁) : isAcyclic G O₂

The reversal class of an acyclic orientation consists of acyclic orientations.

The signed difference of two orientations

Everything below reads the pair (O₁, O₂) through one object: the antisymmetric integer vector diffFlow O₁ O₂ on ordered vertex pairs, which is the "signed edge set on which the two orientations disagree" of Gioan's argument. Antisymmetry (diffFlow_antisymm) is the count_preserving field, and sum_diffFlow says its divergence is the in-degree difference.

def Utilities.diffFlow {G : CFGraph} (O₁ O₂ : CFOrientation G) (u v : G.V) : ℤ

The signed disagreement of two orientations on the parallel class (u, v): how many more edges O₁ sends from u to v than O₂ does.

Equations

• Utilities.diffFlow O₁ O₂ u v = ↑(flow O₁ u v) - ↑(flow O₂ u v)

theorem Utilities.diffFlow_antisymm {G : CFGraph} (O₁ O₂ : CFOrientation G) (u v : G.V) : diffFlow O₁ O₂ u v = -diffFlow O₁ O₂ v u

The signed disagreement is antisymmetric: both orientations saturate the same parallel class, so a surplus one way is a deficit the other.

theorem Utilities.sum_diffFlow {G : CFGraph} (O₁ O₂ : CFOrientation G) (v : G.V) : ∑ w : G.V, diffFlow O₁ O₂ w v = ↑(indeg G O₁ v) - ↑(indeg G O₂ v)

The divergence of the signed disagreement is the in-degree difference.

theorem Utilities.reversalEquiv_of_flow_eq {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ∀ (u v : G.V), flow O₁ u v = flow O₂ u v) : ReversalEquiv O₁ O₂

Two orientations with the same flow function are reversal equivalent, trivially.

Step 1 of Gioan's theorem: equal in-degrees

This is where the fine cycle move earns its place. If O₁ and O₂ have the same in-degree function then diffFlow O₁ O₂ is a nonzero circulation, so following the pairs where O₁ beats O₂ never gets stuck (nonempty_relCycle_of_forward_step). The resulting cycle is a directed cycle of O₁, and reversing it finely moves exactly one unit of flow off each of its steps: in-degrees are untouched (indeg_reverseCycleOne) and the disagreement strictly shrinks.

theorem Utilities.reversalEquiv_of_indeg_eq {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : ∀ (v : G.V), indeg G O₁ v = indeg G O₂ v) : ReversalEquiv O₁ O₂

Orientations with the same in-degree function are reversal equivalent, by fine cycle reversals alone.

This is the σ = 0 case of Gioan's theorem, and it is the exact analogue of eq_of_indeg_eq_of_isAcyclic without the acyclicity hypothesis: instead of forcing the two orientations to coincide, the disagreement is peeled off one directed cycle at a time.

Step 2 of Gioan's theorem: the cut part

Write d = indeg O₁ − indeg O₂. Linear equivalence of the two orientation divisors says d = ∂∂ᵀψ for an integer potential ψ, i.e. d v = ∑ u (ψ u − ψ v) · numEdges v u. The whole of the cut half of Gioan's argument is then the following observation, which needs no decomposition theory at all:

Let W be the set where ψ attains its minimum. Then every edge between W and its complement points into W under O₁.

Indeed for v ∈ W every summand of d v is non-negative and the ones at u ∉ W are at least numEdges v u, so ∑_{v ∈ W} d v ≥ e(W, Wᶜ). On the other hand the disagreement of O₁ and O₂ inside W cancels by antisymmetry, so ∑_{v ∈ W} d v is exactly (inflow into W under O₁) − (inflow into W under O₂), which is at most e(W, Wᶜ). The two bounds pin both quantities: the second inflow is 0 and the first is everything.

So Wᶜ is a directed cut of O₁ and may be reversed. The reversal replaces ψ by ψ + χ_W, which raises the minimum by one and leaves the maximum alone, so the spread of the potential strictly drops and the induction is on that.

theorem Utilities.gioan_reversalEquiv_of_linear_equiv {G : CFGraph} {O₁ O₂ : CFOrientation G} (h : linearEquiv G (ordiv G O₁) (ordiv G O₂)) : ReversalEquiv O₁ O₂

Gioan's theorem, one direction: orientations with linearly equivalent orientation divisors are connected by cycle and cocycle reversals.

Reference: E. Gioan, Enumerating degree sequences in digraphs and a cycle–cocycle reversing system, European J. Combin. 28 (2007) 1351–1366, where the cycle–cocycle reversing system is introduced and its classes are identified with the classes of D(𝒪) modulo linear equivalence. For the related existence of an orientation divisor in every degree-g-1 class, see An–Baker–Kuperberg–Shokrieh, Theorem 4.10 of arXiv:1304.4259v2.

The proof, in two halves. linearEquiv hands over a firing script σ with ordiv 𝒪₂ − ordiv 𝒪₁ = prin σ, i.e. a potential ψ = −σ with indeg 𝒪₁ − indeg 𝒪₂ = ∂∂ᵀψ pointwise. The induction is on the spread max ψ − min ψ, a natural number because G.V is finite.

• Spread 0 — ψ constant, so the two in-degree functions agree, and reversalEquiv_of_indeg_eq finishes with fine cycle reversals alone: the signed disagreement diffFlow is then a circulation, following its positive support never gets stuck, and each directed cycle so found can be reversed one edge at a time, preserving in-degrees (indeg_reverseCycleOne) and strictly shrinking the disagreement.
• Spread positive — isDirectedCut_compl_of_min shows that the complement of the minimum level set W of ψ is already a directed cut of 𝒪₁, so it may be reversed; indeg_reverseCut_compl identifies the effect on in-degrees as prin χ_W, which replaces ψ by ψ + χ_W and drops the spread by exactly one.

Notably no cycle/cut decomposition of ℤ^E is needed. It is replaced by the observation in isDirectedCut_compl_of_min, whose proof is two counting inequalities that squeeze each other. eq_of_indeg_eq_of_isAcyclic above is the degenerate case σ = 0 with 𝒪 acyclic.

Reference: E. Gioan, Enumerating degree sequences in digraphs and a cycle–cocycle reversing system, European J. Combin. 28 (2007) 1351–1366. The proof here is not Gioan's.

Model note (2026-08-20). This used to carry a caveat saying the classical proof does not transcribe, because a CFOrientation cycle reversal had to turn a whole parallel class. That caveat is gone: CFOrientation is now an arbitrary edge-level orientation, and ReversalStep includes the fine move reverseCycleOne, which turns a single edge at each step and is exactly the move Gioan's system is built from. So on an arbitrary multigraph this is now literally Gioan's theorem, hypothesis-free — in particular no simplicity and no connectivity.

The converse implication is not stated, and is false as long as the coarse move is a legal step: cocycle reversal preserves the class of ordiv (it changes it by the firing vector of W) and so does the fine cycle reversal (ordiv_reverseCycleOne), but the coarse one does not in general.

6. Winnability of divisors of cyclic orientations

theorem Utilities.winnable_ordiv_of_not_isAcyclic {G : CFGraph} (h_conn : graphConnected G) (O : CFOrientation G) (hO : ¬isAcyclic G O) : winnable G (ordiv G O)

An orientation with a directed cycle has winnable ordiv.

If ordiv G O were unwinnable then, having degree genus G - 1 (degree_ordiv), it would by unwinnable_iff_exists_acyclic_ordiv be linearly equivalent to ordiv G O' for some acyclic O'; Gioan then puts O and O' in one reversal class, and isAcyclic_of_reversalEquiv propagates acyclicity from O' to O, contradicting the hypothesis.

theorem Utilities.isAcyclic_of_not_winnable_ordiv {G : CFGraph} (h_conn : graphConnected G) (O : CFOrientation G) (hw : ¬winnable G (ordiv G O)) : isAcyclic G O

The contrapositive: an orientation whose divisor is unwinnable is acyclic. Together with ordiv_unwinnable (Orientation.lean) this makes isAcyclic G O ↔ ¬ winnable G (ordiv G O) — see isAcyclic_iff_not_winnable_ordiv.

theorem Utilities.isAcyclic_iff_not_winnable_ordiv {G : CFGraph} (h_conn : graphConnected G) (O : CFOrientation G) : isAcyclic G O ↔ ¬winnable G (ordiv G O)

Orientation criterion. An orientation is acyclic exactly when its divisor is unwinnable.