143 Directed Graphs
143.1 Directed Graphs
The least number of edges one must cut to break \(G\) apart. "\(G\) is \(k\)-edge-connected" is spelled k \(\le \) edgeConnectivity G throughout this file — see robbins_orientation (\(k = 2\)) and exists_kArcConnected_orientation_of_eulerian.
Mathlib has no edge-connectivity, so this is the repo’s notion restated locally. sInf \(\emptyset \) = 0 in \(\mathbb {N}\) reproduces the book’s trivial-graph convention automatically — but it also means a graph with no edge cut (a one-vertex graph) gets \(\kappa ' = 0\), which is the source of the [Nontrivial V] gap in associatedDigraph_isKArcConnected_iff below.
A quiver is a vertex set together with, for each ordered pair, a type of arrows. Taking that type to be a Prop — arrow or no arrow — recovers exactly a digraph, and Mathlib’s Quiver.Path then supplies directed walks for free, which Digraph (a bare Adj with a lattice API) does not.
! Deliberately not an instance. The chapter routinely handles several digraphs on one vertex type at once — \(D\) and its converse \(\breve{D}\), \(D\) and a reorientation of one arc (exercise 10.2.1) — and a global instance would make Quiver.Path ambiguous between them. The cost is that every use site must write @Quiver.Path V D.toQuiver u v explicitly, which is why the statements below are visually heavy.
Follow the arrows, never against them; a directed path additionally never revisits a vertex. The book stresses (figure 10.3) that there is *no close relationship between the lengths of paths and directed paths in a digraph* — the digraph there has arbitrarily long paths but no directed path of length above one. Theorem 10.1 is remarkable precisely because it recovers control of directed-path length from the chromatic number.
! Quiver.Path is the directed walk, so a directed path is a Quiver.Path with Nodup vertices. Note the book’s directed walks are non-null, whereas Quiver.Path.nil is available here; that mismatch is harmless for paths but bites for Euler tours (see IsDirectedEulerTour).
Follow the arrows all the way round and return to where you started, never repeating a vertex en route. Directed cycles are the subject of §10.3: Moon (theorem 10.3) finds them of every length in a diconnected tournament, and Ghouila-Houri (theorem 10.4) finds a spanning one under a degree condition.
0 < length excludes nil; vertices.tail.Nodup allows the repeated basepoint at the two ends while forbidding any other repeat. Note a loop D.Adj v v counts as a directed cycle of length \(1\) under this definition, which is what makes the acyclicity hypotheses below (hacyc) automatically exclude loops — relied on by exists_topological_ordering.
You can get from \(u\) to \(v\) travelling only along arrows in their given direction. Reachability is not symmetric — that asymmetry is the whole point of directing a graph, and is what makes diconnection a strictly stronger condition than connection.
Relation.ReflTransGen D.Adj rather than an existential over Quiver.Path. The two agree (a path witnesses reachability and conversely), but ReflTransGen comes with induction principles and is reflexive, matching the book’s convention that every vertex reaches itself. Being defined directly from Adj, it needs no Quiver instance, so \(D\) and D.converse coexist freely — which converse_reachable relies on.
Wherever you start and wherever you want to go, some route respecting the arrows exists. In the road-network reading of §10.6 this is exactly the condition that a one-way system lets traffic flow freely — every junction remains reachable from every other, and Robbins’ theorem 10.5 says \(2\)-edge-connectivity is precisely what makes it achievable.
Stated directly as "every ordered pair is reachable" rather than via dicomponents, which avoids constructing the quotient. The two agree: one dicomponent means the equivalence relation is total. Note this is not symmetric by fiat — \(\forall \) u v, Reachable u v quantifies over ordered pairs, so both directions are demanded.
How many arrows point into \(v\). Exercise 10.1.2 gives the directed handshake lemma \(\sum d^{-}(v) = \varepsilon = \sum d^{+}(v)\) — each arc is counted once by its head and once by its tail, which is why the directed sum is \(\varepsilon \) and not \(2\varepsilon \).
! Missing from Mathlib (0 hits). Counts vertices \(u\) with D.Adj u v, not arcs — the same thing here, since Digraph is a bare relation and admits no parallel arcs. Needs [DecidableRel D.Adj] for the filter.
How many arrows point out of \(v\). Together with the indegree this refines the single degree of an undirected graph into two numbers, and their interplay drives most of the chapter: Euler tours need them equal (exercise 10.3.2), Ghouila-Houri’s theorem 10.4 needs both large, and exercise 10.1.10 asks for an orientation making them nearly equal everywhere.
! Missing from Mathlib. The exact mirror of indegree under converse, which is the content of exercise 10.1.5(a)(ii).
Count the ordered pairs \((u, v)\) for which an arc runs from \(u\) to \(v\). This is the \(\varepsilon \) of exercise 10.1.2’s handshake lemma and of exercise 10.1.1’s \(2^\varepsilon \) orientation count.
Since Digraph allows no parallel arcs in the same direction, \(\varepsilon \) is simply the size of the adjacency relation, counted as a Finset (V \(\times \) V). Note this differs from the book for multi-digraphs, which B&M permit — a point that also forces the restatement of adjMatrix below.
The least number of arrows pointing into any one vertex. Exercise 10.1.3(a) says an acyclic digraph must have \(\delta ^{-} = 0\), which is what makes topological ordering possible; exercises 10.1.6–10.1.7 turn a large \(\delta ^{-}\) into long directed paths and cycles.
! \(\bigsqcap \) over \(\mathbb {N}\) is Nat.sInf, and Nat.sInf \(\emptyset \) = 0, so on an empty carrier this silently returns \(0\) rather than being undefined. Every use site below carries [Nonempty V] for that reason. Only the minima are defined here; \(\Delta ^{-}\), \(\Delta ^{+}\) are never needed by a surviving statement.
The least number of arrows leaving any one vertex. By the converse symmetry of exercise 10.1.5, statements about \(\delta ^{-}\) transfer to \(\delta ^{+}\) and back — exactly how exercise 10.1.5(b) deduces \(\delta ^{+} = 0\) for acyclic digraphs from \(\delta ^{-} = 0\), without repeating the argument.
Same Nat.sInf \(\emptyset \) = 0 caveat as minIndegree.
Turn every arrow around. It is an involution (\(\breve{\breve{D}} = D\)), it swaps indegree with outdegree, and it reverses reachability — so every theorem about digraphs comes with a free dual, obtained by applying it to the converse. Exercise 10.1.5(a) records exactly these three facts and (b) puts them to work.
A one-line Digraph.mk with the arguments of Adj swapped, so converse_converse should be rfl-adjacent. Because Reachable is defined from Adj and not through a Quiver instance, \(D\) and D.converse can appear in the same statement without ambiguity — see converse_reachable.
The directed analogue of "simple". Note a strict digraph may have both \((u,v)\) and \((v,u)\) — forbidding that is what makes an orientation, which is a strictly stronger condition. Strictness is the standing hypothesis of exercises 10.1.6, 10.1.7 and theorem 10.4, where it guarantees that \(\delta ^{+}\) out-neighbours are \(\delta ^{+}\) genuinely distinct vertices.
Since Digraph is a bare relation it already forbids repeated arcs in the same direction, so the book’s second clause is automatic and strictness reduces to looplessness — Irreflexive D.Adj.
Make every edge one-way, choosing a direction for each. Orientations are the chapter’s central object: exercise 10.1.1 counts them (\(2^\varepsilon \)), the remark after theorem 10.1 builds one whose directed paths are short, exercise 10.1.10 one that is degree-balanced, and §10.6 asks which graphs admit diconnected ones — Robbins’ theorem 10.5.
Two clauses. The first, D.toSimpleGraphInclusive = G, says the underlying graph comes back out as \(G\). The second, \(\forall \) u v, \(\lnot \)(D.Adj u v \(\land \) D.Adj v u), forbids making an edge two-way — without it the associated digraph \(D(G)\) would count as an orientation of \(G\), which it is not. Taking \(u = v\) in the second clause also forces looplessness, so an orientation is automatically strict.
Every pair of players meets exactly once and the arrow points from winner to loser. Tournaments are remarkably well behaved: every one has a directed Hamilton path (Rédei, corollary 10.1) and a "king" reaching everyone in at most two steps (corollary 10.2); diconnected ones are vertex-pancyclic (Moon, theorem 10.3) and hence have directed Hamilton cycles (Camion). §10.7 uses them to rank players.
Unfolded rather than defined as "IsOrientationOf some complete graph": Irreflexive D.Adj plus, for distinct \(u\), \(v\), exactly one of D.Adj u v, D.Adj v u. The \(\leftrightarrow \lnot \) phrasing packs both "at least one" (from completeness of the underlying graph) and "at most one" (from being an orientation) into a single clause.
The arcs crossing from \(S\) into \(T\), counted with their direction. Unlike the undirected edge cut \([S, \bar{S}]\), the directed version splits into two generally unequal halves \((S, \bar{S})\) and \((\bar{S}, S)\) — which is precisely what \(k\)-arc-connectivity measures, and what theorem 10.6 has to balance.
A Finset (V \(\times \) V) obtained by filtering the product \(S \times ^{s} T\), so \(|(S, T)|\) is its card. Used in IsKArcConnected and in Moon’s theorem 10.3, where the book’s "\((S, T)\) must be nonempty" becomes a cardinality claim.
However you split the vertices in two, at least \(k\) arrows point from the first part to the second. Exercise 10.3.5 says \(1\)-arc-connected is the same as diconnected, and exercise 10.3.6(b) that \(D(G)\) is \(k\)-arc-connected exactly when \(G\) is \(k\)-edge-connected. Nash-Williams’ theorem — of which theorem 10.6 is the easy special case — says every \(2k\)-edge-connected graph has a \(k\)-arc-connected orientation.
! The book says nontrivial digraph, and this definition drops that. On a one-vertex carrier there is no nonempty proper \(S\), so the condition is vacuously true for every \(k\) — which is why statements consuming it must supply [Nontrivial V] themselves. diconnected_iff_isKArcConnected_one does; associatedDigraph_isKArcConnected_iff does not, and is false in consequence (see its docstring).
Keep only the vertices in \(S\) and the arcs with both ends there. The dicomponents of \(D\) are the induced subdigraphs \(D[V_{i}]\) on the diconnection classes, and theorem 10.2’s induction removes \({v} \cup N^{+}(v)\) this way.
Kept on the same carrier \(V\), with membership in \(S\) folded into Adj, rather than moving to a subtype. This avoids subtype juggling across the many statements that induce, at the cost that induce D S has isolated vertices outside \(S\) — harmless, since every consumer only asks about arcs.
Reading off the arrows a directed walk uses, in order. This is what a trail condition quantifies over — a directed trail repeats no arc — and what a directed Euler tour must exhaust.
! Defective: this definition has a sorry body. It is declared List (V \(\times \) V) := sorry, so arcsOf is an opaque, unspecified function, not the arc list of anything. This is the most damaging defect in the file, because the opacity propagates: IsDirectedTrail and IsDirectedEulerTour are defined from it, so both are meaningless as stated; and therefore exists_directedEulerTour_iff (exercise 10.3.2), deBruijnDigraph_exists_directedEulerTour and exists_arcDisjoint_directedPaths (exercise 10.3.3) say nothing — which is the entire §10.5 computer-drum application plus the flow precursor to chapter 11. It also violates the project convention (.claude/CLAUDE.md): never sorry in a def* — a sorry-ed proof is an honest debt, a sorry-ed definition is a silent change of meaning.
The repair is a routine structural recursion on Quiver.Path, whose two constructors are nil : Path a a and cons : Path a b \(\to \) (b ⟶ c) \(\to \) Path a c:
arcsOf nil = [] arcsOf (cons p e) = arcsOf p ++ [(b, c)]
with \(b\), \(c\) the source and target of the arrow \(e\). Nothing about it is delicate; the outline simply left it unspecified. This is a change of meaning, not of annotation, so it has been flagged rather than made here.
Follow the arrows, never using the same arrow twice, though you may revisit vertices. The directed analogue of §1.6’s trail, and the notion an Euler tour refines.
! Inherits the arcsOf defect: since arcsOf is sorry, this predicate is (opaque list).Nodup and means nothing. Repairing arcsOf repairs this automatically.
The directed version of Euler’s problem — traverse every one-way street exactly once and return to the start. Exercise 10.3.2 gives the criterion: possible exactly when \(D\) is connected and \(d^{+}(v) = d^{-}(v)\) everywhere, the directed analogue of theorem 4.1’s even-degree condition, because every visit uses one arrow in and one out. §10.5 uses it to design an efficient computer drum via the de Bruijn digraph.
! Defective on two counts. 1. Inherits the arcsOf defect — both conjuncts are stated in terms of an opaque function, so the predicate currently means nothing. 2. Admits the null walk. B&M’s directed walks are explicitly non-null (§10.1), so nil is not a directed tour for them; here Quiver.Path.nil satisfies both conjuncts vacuously ([].Nodup, and no arc to exhaust when \(D\) has none). This is not cosmetic: it makes exists_directedEulerTour_iff false outright — see the counterexample there.
The repair for (2) is to add 0 < Quiver.Path.length p, matching "non-null". Both repairs change meaning, so they are flagged rather than made here.
Weaker than diconnected — you need only get one way between any two vertices, not both. Exercise 10.2.2 characterises it: \(D\) is unilateral exactly when it has a spanning directed walk.
The disjunction is over Reachable, which is reflexive, so the case \(u = v\) is automatic. Note "unilateral" sits strictly between "connected" (underlying graph) and "diconnected".
Record a \(1\) where an arrow runs from \(v_{i}\) to \(v_{j}\) and \(0\) otherwise. Unlike the undirected case (§1.3) this matrix is not symmetric — its asymmetry encodes the orientations. Exercise 10.1.8 shows \(A^{k}\) counts directed walks of length \(k\), and §10.7 uses the powers of \(A\) to rank tournament players via the level score vectors \(s_{i} = A^{i}J\).
! Restated: Digraph has no arc multiplicities, so entries are \(0\) or \(1\) rather than a count. For strict digraphs — which every §10.7 statement is about, tournaments being orientations — the two agree, so nothing is lost where it is used. The value type \(\alpha \) is left generic so the same matrix serves the \(\mathbb {N}\)-valued counting of exercise 10.1.8 and any later numeric work.
Shrink each dicomponent to a single point and keep the arcs between them. Exercise 10.1.9 shows the condensation is acyclic — a directed cycle among dicomponents would merge them into one — so by exercise 10.1.3(b) the dicomponents can be topologically ordered, which is what §10.7 uses to rank the participants of a non-diconnected tournament, and what exercise 10.2.1 uses on tournaments.
! The \(a \ne b\) clause is a recorded correction, not a transcription. Taken literally the book’s condition puts an arc from \(w_{i}\) to \(w_{i}\) whenever \(D_{i}\) has any internal arc — a loop at every non-trivial dicomponent — which would make condensation_acyclic false, since a loop is a directed cycle of length \(1\). B&M plainly intend \(i \ne j\).
The vertex type is Quiver.StronglyConnectedComponent, Mathlib’s quotient by mutual reachability, which is exactly the set of dicomponents.
\(\vec{d}(u,v)\). ! Nat.sInf \(\emptyset \) = 0 when \(v\) is unreachable from \(u\).
The fewest arrows you must follow to get from \(u\) to \(v\). Unlike the undirected distance of §1.6 this is not symmetric — \(\vec{d}(u,v)\) and \(\vec{d}(v,u)\) may differ, which is the whole reason §10.7 needs \(d + 3\) rather than something symmetric.
! Nat.sInf \(\emptyset \) = 0, so an unreachable \(v\) gets distance \(0\) rather than \(\infty \). The definition is therefore faithful only on diconnected digraphs — which is exactly where the book defines it, and both consumers (tournament_adjMatrix_pow_pos, dirDiameter) carry hdicon. Minimising over Quiver.Path lengths rather than over Reachable witnesses, since the length is what is wanted.
The worst case of the directed distance — how far apart two vertices can be when you must respect the arrows. Theorem 10.7 shows that for a diconnected tournament on at least five vertices \(A^{d+3}\) is entrywise positive, where \(d\) is this diameter, and corollary 10.7 turns that into the primitivity that makes the §10.7 ranking method converge.
A Finset.sup over all ordered pairs, so the diagonal \(\vec{d}(v,v) = 0\) is included harmlessly. Inherits dirDist’s sInf \(\emptyset \) = 0 caveat: on a non-diconnected digraph the diameter is silently too small.
Make every street two-way. This embeds undirected graph theory inside directed graph theory: exercise 10.3.6 shows paths in \(G\) correspond exactly to directed paths in \(D(G)\), and \(D(G)\) is \(k\)-arc-connected exactly when \(G\) is \(k\)-edge-connected. Exercise 10.3.1 uses the embedding to derive Dirac’s theorem 4.3 from Ghouila-Houri’s 10.4.
One line: G.Adj is already symmetric and irreflexive, so it is the arc relation of \(D(G)\) — the "two oppositely oriented arcs" are the two directions of the symmetric relation. Note \(D(G)\) is emphatically not an orientation of \(G\) (IsOrientationOf’s second clause fails at every edge); the contrast between doubling and orienting is exactly what §10.6 is about.
For the adjacency matrix this says: however you pick a starting and finishing vertex, there is a directed walk of some common length \(k\) between them. Corollary 10.7 characterises when a tournament’s matrix is primitive — exactly when the tournament is diconnected with \(\nu \ge 4\). Primitivity is what licenses Perron–Frobenius, which gives the convergence of the iterated score vectors \(s_{i} = A^{i}J\) used to rank the players.
! Missing from Mathlib (0 hits). Stated for Matrix n n \(\mathbb {N}\) rather than the book’s real matrices, since the only instance needed is the adjacency matrix; \(0 \lt (R ^k) i j\) is then the entrywise positivity \(R^{k} \gt 0\). Note Mathlib’s Matrix order is not entrywise by default, which is why the positivity is spelled pointwise.
A vertex is a window of \(n-1\) bits; following an arc shifts the window one place, dropping the leading bit and appending a new one. Each arc therefore corresponds to an \(n\)-bit string — its label — and a directed Euler tour reads off every \(n\)-bit string exactly once, giving a cyclic binary sequence of length \(2^{n}\) in which all \(2^{n}\) windows are distinct.
The application (§10.5). A rotating drum’s surface is divided into \(2^{n}\) insulating or conducting sections, read by \(k\) consecutive contacts. *First note that \(k\) contacts yield a \(k\)-digit binary number, and there are \(2^{k}\) such numbers. Therefore, if all \(2^{n}\) positions are to give different readings, we must have \(2^{k} \ge 2^{n}\), that is, \(k \ge n\)* — and the de Bruijn sequence shows \(n\) contacts suffice. For \(n = 4\) the tour of figure 10.10 gives \(0000111100101101\). Due to Good (1946).
! Missing from Mathlib and the Archive (0 hits). A vertex is a function Fin (n-1) \(\to \) Bool rather than a list, so the shift condition is indexed: p ⟨i+1, _⟩ = q i for every \(i\) with \(i + 1 \lt n - 1\), which is the book’s \(1 \le i \le n-2\) in 0-indexed form. The last coordinate of \(q\) is unconstrained, giving the two out-arcs. \(D_n\) has loops (the all-zeros and all-ones vertices) but no parallel arcs — so it is not strict, which is fine, as no §10.5 statement needs strictness. Arc labels are not modelled: the label is recoverable from the arc, and exists_deBruijn_sequence states the conclusion about the sequence directly.
An orientation is a choice, independently for each edge, of one of its two directions; with \(\varepsilon \) edges and two choices each the product rule gives \(2^\varepsilon \). These are labelled objects: two orientations differing only by a symmetry of \(G\) still count separately.
Step 1 is the whole exercise and the Sym2 bookkeeping is the only fiddly part — the natural first move is to prove a helper turning IsOrientationOf into "for each edge, exactly one of the two directions".
The directed handshaking lemma. Every arc has exactly one head, so summing indegrees counts each arc once; likewise every arc has one tail. Contrast the undirected version (theorem 1.1), where the sum of degrees is \(2\varepsilon \): there each edge is counted twice, once from each end, whereas here the head-count and tail-count are kept separate and each totals \(\varepsilon \).
Stated as a conjunction because the book states both equalities at once; nothing forces them to share a proof, but step 4 notes they should.
If every vertex had an incoming arc one could walk backwards for ever; finiteness forces a repeat, and the portion between the two visits is a directed cycle. So an acyclic digraph always has a "source" with nothing pointing into it — the base of the topological-ordering induction in part (b).
[Nonempty V] is load-bearing: on an empty carrier there is no \(v\) to produce, while hacyc holds vacuously. Note hacyc also rules out loops, since a loop is a directed cycle of length \(1\) under IsDirectedCycle.
A topological ordering: line the vertices up so every arrow points forwards. Greedy construction via part (a) — take a source, delete it, repeat. These are the standard tool for scheduling tasks with prerequisites, and §10.7 uses the version for the condensation of a tournament to order its dicomponents in a way that preserves dominance.
The book’s "every arc with head \(v_{i}\) has its tail among the earlier vertices" is contraposed into the equivalent and more usable D.Adj u v \(\to \) f u < f v. Note no [Nonempty V] is needed here, unlike part (a) — the empty case is the induction’s base.
Reversing every arrow twice returns each to its original direction, so the converse is an involution. That is what makes it a genuine duality: any statement proved for all digraphs yields its mirror image for free, with in- and outdegrees and the direction of reachability exchanged — as parts (ii), (iii) and (b) then exploit.
The shortest item in the file; a good first fill to shake out the Digraph extensionality API.
An arc pointing into \(v\) in \(D\) points out of \(v\) in the converse, and vice versa. This is the workhorse of the duality: exercise 10.1.5(b) uses it to turn "acyclic \(\Longrightarrow \) \(\delta ^{-} = 0\)" into "acyclic \(\Longrightarrow \) \(\delta ^{+} = 0\)" without repeating the argument.
The open scoped Classical in on this declaration supplies decidability for D.converse.Adj; step 3 is where that shows up.
A directed path from \(u\) to \(v\) in the converse is exactly a directed path from \(v\) to \(u\) in \(D\), read backwards. A useful consequence: diconnection is self-dual — \(D\) is diconnected exactly when \(\breve{D}\) is — since diconnection demands reachability both ways.
This is the one place where defining Reachable as ReflTransGen rather than via Quiver.Path pays off directly: no Quiver instance is in play, so \(D\) and D.converse appear in the same statement without ambiguity.
An acyclic digraph has both a "source" (nothing in) and a "sink" (nothing out), which is what lets topological ordering be built from either end. The point of the exercise is methodological: the converse converts one statement into its dual with no new argument.
Step 1 needs a Quiver.Path reversal for D.converse versus \(D\); since toQuiver is not an instance, both quivers must be named explicitly. Worth extracting as a standalone lemma, as converse_reachable is the same fact one level down.
The directed analogue of exercise 1.6.3. Strictness is what makes the counting work: it guarantees the out-neighbours are \(\delta ^{+}\) genuinely distinct vertices.
! Step 5 is easy to get wrong. The statement asks for one path of length \(\ge \) max{\(\delta ^{-}\), \(\delta ^{+}\)}, not one path per bound; since max is one of the two, produce the two paths and pick the longer. minIndegree/minOutdegree are \(\bigsqcap \) over \(\mathbb {N}\), so [Nonempty V] is needed to keep them from collapsing to \(0\).
Sharpens exercise 10.1.6 from paths to cycles, exactly as exercise 1.7.3 sharpens 1.6.3 undirected. It is consumed inside Ghouila-Houri’s theorem 10.4, which opens by noting \(l \gt \nu /2\) for the longest directed cycle — that is this exercise with \(k \ge \nu /2\).
\(hk : 0 \lt k\) is load-bearing: with \(k = 0\) the conclusion would demand a directed cycle of length \(\ge 1\) in a digraph that may have no cycle at all. hdeg pins max \(\delta ^{-}\) \(\delta ^{+}\) to \(k\) as an equality, matching the book.
The \((i,j)\) entry of \(A\) counts arcs, i.e. walks of length one; matrix multiplication sums over an intermediate vertex, and every walk of length \(k\) decomposes uniquely as a shorter walk plus a final arc. This is the directed counterpart of exercise 1.6.2, and it is what makes §10.7’s ranking work: the \(i\)-th level score vector is \(A^{i}J\), counting directed walks of length \(i\) out of each player. Theorem 10.7 consumes it directly.
! Restated for a \(0/1\) matrix, Digraph having no arc multiplicities; for the strict digraphs of §10.7 this is no loss. The right-hand side is Nat.card of a subtype of Quiver.Path, which is finite because the length is pinned — but that finiteness may need to be supplied for Nat.card to behave.
A directed cycle among dicomponents would merge them into one, so contracting always produces an acyclic digraph — which by exercise 10.1.3(b) can be topologically ordered. §10.7 uses exactly this to rank the dicomponents of a non-diconnected tournament in a dominance-preserving order, and exercise 10.2.1 uses it on tournaments.
Step 3 is where Quiver.StronglyConnectedComponent’s defining property is consumed; the useful form is "same component \(\leftrightarrow \) mutually reachable", which should be extracted first. Note the statement quantifies over all base points \(c\), since IsDirectedCycle is stated for closed paths at a given vertex.
Every graph can be made one-way in a balanced way, with the traffic into and out of each junction differing by at most one. Contrast exercise 10.6.1, which shows the stronger set-wise balance — \(||(S, \bar{S})| - |(\bar{S}, S)|| \le 1\) for every vertex set \(S\) — is not always achievable, the Petersen graph being a counterexample.
The conclusion is stated as two \(\mathbb {Z}\) inequalities rather than \(|\cdot | \le 1\), avoiding Int.natAbs juggling. The open scoped Classical in supplies decidability of the existentially-bound D.Adj; the outline’s \(\exists \) _ : DecidableRel D.Adj does not register as an instance inside the body, which is why it was replaced.
(Roy, 1967; Gallai, 1968). *A digraph \(D\) contains a directed path of length \(\chi - 1\)*, where \(\chi \) is the chromatic number of the underlying graph.
Striking because, as figure 10.3 shows, there is otherwise *no close relationship between the lengths of paths and directed paths in a digraph* — yet the chromatic number of the underlying graph controls the latter exactly. The remark following shows the bound is best possible.
\(k - 1\) is \(\mathbb {N}\)-subtraction, harmless as the goal is a lower bound. \(hk\) pins \(\chi \) of toSimpleGraphInclusive — the underlying graph — to \(k\) in \(\mathbb {N}\infty \). Step 4 is the mathematical core; steps 1 and 2 are both "choose a maximum/minimum in a finite nonempty family" and should share a helper.
Orient every edge from the lower colour class to the higher. Along a directed path the colour index strictly increases, so the path has at most \(\chi \) vertices. Combined with theorem 10.1 this shows \(\chi - 1\) is exactly the right bound. Note the orientation is automatically acyclic, the colour index being a topological ordering — so this also witnesses exercise 10.1.3(b) in reverse.
Stated with an arbitrary \(k\)-colouring rather than an optimal one, which is the usable form: exercise 10.2.6(a) instantiates it at \(k = \Delta + 1\) via corollary 8.1.2, not at \(k = \chi \). Step 4’s injectivity is a cleaner invariant to carry than the book’s "no two vertices share a colour".
(Rédei, 1934). *Every tournament has a directed Hamilton path.*
B&M define the term just above: *A directed Hamilton path of \(D\) is a directed path that includes every vertex of \(D\).*
In any round-robin competition the players can be lined up so that each beat the next. The book cautions in §10.7 that this does not give a sensible ranking, since a tournament generally has many directed Hamilton paths — the six-player example has \((3,1,2,4,5,6)\), \((1,2,4,5,6,3)\), \((1,4,6,3,2,5)\) and others, declaring different winners. That is what motivates the eigenvector method.
"Includes every vertex" is \(\forall \) w, w \(\in \) p.vertices rather than a cardinality claim, which is what step 3 delivers most directly. Exercise 10.2.3 gives an independent route not passing through theorem 10.1.
(Chvátal and Lovász, 1974). *A loopless digraph \(D\) has an independent set \(S\) such that each vertex of \(D\) not in \(S\) is reachable from a vertex in \(S\) by a directed path of length at most two.*
Such a set is called a semi-kernel. The independence requirement is what makes it non-trivial — one wants mutually non-adjacent "dominators" from which everything else is within two steps. Corollary 10.2 is the tournament case, where independence forces \(|S| = 1\).
The \(u = v\) disjunct in the goal covers the reflexive case and is not in the book, which says "each vertex not in \(S\)"; it is harmless and makes the statement easier to instantiate. hloop : Irreflexive D.Adj is B&M’s "loopless". IsIndepSet is taken in toSimpleGraphInclusive, matching "independent set" for the underlying graph.
*A tournament contains a vertex from which every other vertex is reachable by a directed path of length at most two.*
Such a vertex is called a king: a player who, for every other player \(v\), either beat \(v\) directly or beat someone who beat \(v\). Exercise 10.2.4 gives a direct proof — take a vertex of maximum outdegree — which is dropped from this file as a second proof of the same statement. Note a king need not have won the most games, and a tournament may have several kings.
[Nonempty V] is load-bearing for step 3; without it \(S = \emptyset \) is a legitimate semi-kernel and no \(u\) exists.
Tournaments are never far from diconnected: a single reversed result suffices to make every player reachable from every other. Step 3 is the tournament speciality — in a general digraph the dicomponents form only a partial order, and one reversal would not do.
The reorientation is written inline as an \(if\)-cascade on Adj rather than via a helper: \((x,y)\) is removed, \((y,x)\) added, everything else kept. Note the if (u = y \(\land \) v = x) then True branch must come after the \((x,y)\) branch, which it does.
. \(D\) is unilateral if and only if \(D\) has a spanning directed walk.*
Unilateral means any two vertices are comparable — you can get from one to the other, though perhaps only one way round. It sits strictly between "connected" and "diconnected".
! The book genuinely means walk, not path: revisiting vertices is essential, since a spanning directed path would be a Hamilton path and is a far stronger requirement. The Lean statement accordingly asks only for a Quiver.Path (= directed walk) whose vertices cover \(V\), with no Nodup condition — do not be tempted to add IsDirectedPath.
*Let \(P = (v_{1}, \dots , v_k)\) be a maximal directed path in a tournament \(D\). Suppose \(P\) is not a directed Hamilton path and let \(v\) be any vertex not on \(P\). Then for some \(i\), both \((v_{i}, v)\) and \((v, v_{i+1})\) are arcs of \(D\).*
Because \(D\) is a tournament, \(v\) is joined to every vertex of \(P\) in one direction or the other; maximality forces \(v_{1} \to v\) at the start and \(v \to v_k\) at the end, so travelling along \(P\) the direction must switch somewhere. Part (b) — dropped here, being a re-derivation of corollary 10.1 — inserts \(v\) at that point to get a longer directed path and repeats until it spans.
The path is presented as a List V with IsChain D.Adj rather than as a Quiver.Path, since the statement indexes into it (\(l[i]\), \(l[i+1]\)) and lists index far more comfortably. [Inhabited V] supports head!/getLast! in hmax; hne : l \(\ne \) [] keeps those meaningful.
(Chvátal and Komlós). Let \(D\) be a digraph with \(\chi \gt mn\), and let \(f\) be a real-valued function on \(V\). Then \(D\) has either a directed path \((u_{0}, \dots , u_m)\) with \(f(u_{0}) \le f(u_{1}) \le \dots \le f(u_m)\), or a directed path \((v_{0}, \dots , v_n)\) with \(f(v_{0}) \gt f(v_{1}) \gt \dots \gt f(v_n)\).*
Theorem 10.1 says a high chromatic number forces a long directed path; this refines it by controlling how \(f\) behaves along that path. A large enough chromatic number forces a monotone directed path — weakly increasing of length \(m\), or strictly decreasing of length \(n\). Part (b) reads off Erdős–Szekeres.
Paths are List V with two IsChains — one for adjacency, one for the \(f\)-comparison — plus Nodup, rather than Quiver.Paths, so that the monotonicity condition can be stated alongside. Note the asymmetry \(\le \) versus \(\gt \) is the book’s and is essential: with two weak orders step 3 would fail on an arc where \(f u = f w\).
(Erdős and Szekeres). Deduce that any sequence of \(mn + 1\) distinct integers contains either an increasing subsequence of \(m\) terms or a decreasing subsequence of \(n\) terms.*
The classical Erdős–Szekeres theorem, obtained as a special case of a statement about digraphs — a good illustration of the chapter’s theme that chromatic number controls directed-path structure.
! Restated: Mathlib’s Archive version is not importable, so the statement is spelled out here and derived from (a) as the book intends. \(g\) is \(\mathbb {Z}\)-valued (the book’s "integers") while part (a) needs \(\mathbb {R}\), hence the cast in step 2. hN : m * n < N is the book’s "\(mn + 1\) terms", generalised to any longer sequence.
*Using theorem 10.1 and corollary 8.1.2, show that \(G\) has an orientation in which each directed path is of length at most \(\Delta \).*
Chaining two results already available: \(\chi \le \Delta + 1\) bounds the palette, and the colour-increasing orientation turns a palette bound into a path bound. Part (b) of the exercise — dropped here, being the same statement — asks for a constructive proof avoiding the chromatic detour.
! This rides chapter 8’s corollary 8.1.2, which is out of chapter; step 1 is therefore an import from TCSlib/GraphTheory/VertexColourings.lean (chromaticNumber_le_maxDegree_add_one) rather than something proved here. Note the shape of step 2: this is exactly why the theorem-10.1 remark was stated for an arbitrary \(k\)-colouring rather than an optimal one.
(Moon, 1966). *Each vertex of a diconnected tournament \(D\) with \(\nu \ge 3\) is contained in a directed \(k\)-cycle, \(3 \le k \le \nu \).*
A digraph with this property is vertex-pancyclic: every vertex lies on cycles of every possible length. Taking \(k = \nu \), every diconnected tournament has a directed Hamilton cycle — first proved by Camion (1959). Theorem 10.7 consumes the full strength, needing cycles of several specific lengths through a given vertex.
The cycle is based at \(u\) (p : Path u u), which is how "\(u\) is contained in" is expressed. ! The book’s final splice \((v_{0}, v, w, v_{2}, \dots , v_n)\) silently assumes \(v\) follows \(v_{0}\) and \(w\) precedes \(v_{2}\); check the index bookkeeping against \(n \ge 3\) before trusting it.
(a special case of Ghouila-Houri, 1960). *If \(D\) is strict and min{\(\delta ^{-}\), \(\delta ^{+}\)} \(\ge \) \(\nu \)/2 > 1, then \(D\) contains a directed Hamilton cycle.*
The directed extension of Dirac’s theorem 4.3 — a large minimum degree, now in both directions, forces a spanning cycle. Exercise 10.3.1 recovers Dirac from it by orienting a graph suitably.
hdeg states \(\nu \le 2 d^{-}(v)\) and \(\nu \le 2 d^{+}(v)\) rather than min{\(\delta ^{-}\),\(\delta ^{+}\)} \(\ge \) \(\nu \)/2, avoiding division; \(hv : 2 \lt \nu \) is the book’s \(\nu /2 \gt 1\). The result is only a special case of Ghouila-Houri’s theorem, as B&M note.
*\(D\) contains a directed Euler tour if and only if \(D\) is connected and \(d^{+}(v) = d^{-}(v)\) for all \(v \in V\).*
The directed analogue of Euler’s theorem 4.1. Every visit uses one arrow in and one out, so the two counts must balance. Why it is built early: §10.5 depends on it — the de Bruijn digraph \(D_n\) is connected with every indegree and outdegree \(2\), so it has a directed Euler tour, and that tour is exactly the binary sequence for the computer drum.
Connectivity is asked of toSimpleGraphInclusive, the underlying graph, matching B&M’s "\(D\) is connected" (a property of the underlying graph, per §10.1).
+ Statement repaired — connectivity moved from the right-hand side into a hypothesis. As previously written, (\(\exists \) Euler tour) \(\leftrightarrow \) (Connected \(\land \) balanced), the \(\leftrightarrow \) was false, for two compounding reasons.
Counterexample 1. Let \(D\) have no arcs and card V \(\ge \) 2. Then Quiver.Path.nil at any \(u\) satisfies IsDirectedEulerTour — its arc list is \([]\) (so Nodup), and the exhaustiveness clause \(\forall \) a b, D.Adj a b \(\to \) … is vacuous — so the left side holds, while the right side fails because \(D\) is disconnected.
Counterexample 2. Adding arcs does not rescue it: take one directed cycle plus an isolated vertex. A tour of the cycle exhausts every arc, so the left side holds, but the underlying graph is still disconnected.
So no strengthening of the left side repairs this; connectivity has to be assumed, not concluded. With hconn a hypothesis the equivalence is the honest directed Euler theorem, and it now matches the shape of this library’s undirected euler_tour_iff_no_odd_degree in EulerHamilton.lean.
! Note that unlike the undirected statement, no arc-nonemptiness hypothesis is needed: hconn already forces the arc-free case to be the one-vertex graph, where nil is an Euler tour and the balance condition holds vacuously, so the \(\leftrightarrow \) is true there.
*Let \(D\) be a digraph such that (i) \(d^{+}(x) - d^{-}(x) = l = d^{-}(y) - d^{+}(y)\) and (ii) \(d^{+}(v) = d^{-}(v)\) for \(v \in V \ {x, y}\). Show, using exercise 10.3.2, that there exist \(l\) arc-disjoint directed \((x, y)\)-paths in \(D\).*
The degree conditions say \(x\) has an excess of \(l\) outgoing arcs, \(y\) an excess of \(l\) incoming ones, and everything else is balanced — so \(l\) units of "flow" must run from \(x\) to \(y\). A small precursor of the max-flow min-cut machinery of chapter 11.
! Two obstructions to the intended route, both recorded rather than resolved. (i) Digraph admits no parallel arcs, so step 1’s "\(l\) copies of \((y,x)\)" is not expressible on \(D\); the construction has to move to Digraph (V \(\oplus \) Fin l), routing each extra arc through its own new vertex. The statement stays on \(D\) and is well-typed. (ii) The conclusion mentions arcsOf, which currently has a sorry body, so the arc-disjointness clause is presently meaningless — see that definition. Degrees are compared in \(\mathbb {Z}\) to let \(hx\), \(hy\) state genuine differences without \(\mathbb {N}\)-truncation.
. A diconnected digraph which contains an odd cycle also contains a directed odd cycle.*
The hypothesis gives an odd cycle in the underlying graph, whose arcs may point every which way; the conclusion upgrades it to a genuinely directed odd cycle. Diconnection is essential — without it the parity argument cannot be propagated across the whole digraph, and the statement is false.
The undirected cycle enters as a Walk in toSimpleGraphInclusive with IsCycle and Odd length; the directed conclusion is a Quiver.Path. Step 2’s "decompose a closed walk into directed cycles" has no Mathlib counterpart for Quiver.Path and will have to be built.
*A nontrivial digraph is diconnected if and only if it is 1-arc-connected.*
Diconnection is the \(k = 1\) case of arc-connectivity, exactly as connection is the \(k = 1\) case of edge-connectivity in §3.1.
[Nontrivial V] is the book’s "nontrivial digraph" and is load-bearing: on a one-vertex carrier there is no nonempty proper \(S\), so IsKArcConnected 1 is vacuously true while Diconnected — which is also true there — would make the \(\leftrightarrow \) hold only by accident. More importantly, its absence is what breaks associatedDigraph_isKArcConnected_iff below.
*\(D(G)\) is \(k\)-arc-connected if and only if \(G\) is \(k\)-edge-connected.*
The associated digraph faithfully preserves connectivity, so the directed notion generalises the undirected one. Contrast §10.6, where the question is which orientations — not the doubling — preserve it; there the answer is much more delicate (Robbins, Nash-Williams).
"\(G\) is \(k\)-edge-connected" is spelled k \(\le \) edgeConnectivity G, per §3.1. Step 2 needs that a minimal edge cut is \([S, S^{c}]\) for a component \(S\), which is the same fact the local IsEdgeCut docstring notes when reconciling the book’s shape-based definition with the deletion-based one used here.
+ Statement repaired — [Nontrivial V] added. The \(\leftrightarrow \) was false on a one-vertex carrier. Take card V = 1, so \(G = \bot \), and \(k = 1\). Left side: there is no nonempty proper S : Finset V, so IsKArcConnected 1 holds vacuously. *Right side:* \(\bot \) on one vertex is Connected, so nothing disconnects it, \(G\) has no edge cut at all, and edgeConnectivity G = 0; the claim \(1 \le 0\) fails.
[Nontrivial V] excludes exactly that carrier and is the hypothesis the book’s "nontrivial digraph" convention supplies implicitly (compare diconnected_iff_isKArcConnected_one above, which already carries it). ! Both Menger statements in Networks.lean consume this lemma, so their hypotheses must be checked against the added Nontrivial when they are proved.
A vertex is a window of \(n-1\) bits. Its out-neighbours drop the leading bit and append a new one — two choices; its in-neighbours drop the trailing bit and prepend a new one — again two. This is the balance condition exercise 10.3.2 needs, and is why \(D_n\) has a directed Euler tour.
\(hn : 2 \le n\) is load-bearing in step 3: for \(n = 1\) the carrier Fin 0 \(\to \) Bool is a singleton and the free coordinate does not exist, so the two neighbours coincide and the degree is \(1\), not \(2\).
From any binary string one can reach any other by shifting in the target’s bits one at a time; after \(n - 1\) shifts the window contains exactly the target. Together with the degree balance above, this is the second half of the Euler-tour criterion of exercise 10.3.2.
The explicit walk of step 1 is the whole content; a slick argument is unlikely to be shorter than just writing the \(n - 1\) intermediate vertices down as a function of the step index.
Each arc carries an \(n\)-bit label and the tour uses every arc exactly once, so reading off the first digit of each label in order produces a cyclic binary sequence of length \(2^{n}\) in which all \(2^{n}\) windows of length \(n\) are distinct.
The application. Divide a rotating drum’s surface into \(2^{n}\) sections according to that sequence; then \(n\) consecutive contacts read a different \(n\)-bit number at each of the \(2^{n}\) positions, so all positions are distinguishable — and \(n\) is optimal, since \(k\) contacts give only \(2^{k}\) readings. For \(n = 4\) the book’s tour gives \(0000111100101101\). Due to Good (1946).
! This is a three-line consequence of its two inputs, but it inherits both defects of exists_directedEulerTour_iff: that theorem is currently false as stated, and IsDirectedEulerTour is defined through the sorry-bodied arcsOf. Until those are repaired this statement is not the intended one. Note also that the labels are not modelled — the conclusion asserts a tour exists, and turning it into the binary sequence is left to exists_deBruijn_sequence.
(Robbins, 1939). *If \(G\) is 2-edge-connected, then \(G\) has a diconnected orientation.*
How to make a road system one-way so traffic can still flow everywhere. A graph with a cut edge clearly cannot manage it — whichever way that edge is directed, one side becomes unreachable — and Robbins showed 2-edge-connectivity is not merely necessary but sufficient. Intuitively, each new vertex is given both a way in and a way out.
! Step 2 rides chapter 3’s exercise 3.2.1, which this repo does not have; budget for it before starting. h2ec : 2 \(\le \) edgeConnectivity G is "\(2\)-edge-connected" per §3.1. Theorem 10.6 is the \(k = 1\) case of a different route to the same conclusion, so neither theorem subsumes the other.
*Let \(G\) be a \(2k\)-edge-connected graph with an Euler trail. Then \(G\) has a \(k\)-arc-connected orientation.*
The easy special case of a theorem of Nash-Williams (1960), that every \(2k\)-edge-connected graph has a \(k\)-arc-connected orientation; the general proof is difficult. Robbins’ theorem 10.5 is the case \(k = 1\) — proved there by a quite different, ear-decomposition route.
! Step 4’s \(\lfloor m/2\rfloor \) is stated as 2 * count + 1 \(\ge \) m to keep \(\mathbb {N}\) division out. Step 2 is where an Euler trail rather than a tour matters: an open trail is what allows the discrepancy of one, and a closed tour would give equality. Note t : G.Walk u v with \(u\), \(v\) unconstrained, so both cases are covered.
*Let \(D\) be a diconnected tournament with \(\nu \ge 5\), and let \(A\) be the adjacency matrix of \(D\). Then \(A^{d+3} \gt 0\) (every entry positive), where \(d\) is the directed diameter of \(D\).*
Why it matters (§10.7). The \(i\)-th level score vector of a tournament is \(s_{i} = A^{i}J\), each player’s score being the sum of the scores of those they beat. Primitivity of \(A\) is what lets Perron–Frobenius guarantee these vectors converge to a positive eigenvector, giving a well-defined ranking.
! The arithmetic \(d - d_{ij} + 3\) is \(\mathbb {N}\)-subtraction but never truncates, since \(d_{ij} \le d\); still, establish that inequality before the case split rather than relying on it implicitly. \(\nu \ge 5\) is load-bearing in step 4 only.
*The adjacency matrix \(A\) of a tournament \(D\) is primitive if and only if \(D\) is diconnected and \(\nu \ge 4\).*
The ranking method (§10.7). When \(A\) is primitive, Perron–Frobenius gives a largest real eigenvalue \(r\) with lim_i (A/r)\(^{i}\) J = s, a positive eigenvector; the normalised \(\bar{s}\) measures relative strengths. For the book’s six-player example \(r \approx 2.232\) and \(\bar{s} \approx (.238, .164, .231, .113, .150, .104)\), ranking the players \(1, 3, 2, 5, 4, 6\). Non-diconnected tournaments are handled by ranking within dicomponents and then ordering the dicomponents by dominance (exercises 10.1.9 and 10.1.3(b)). Due to Wei (1952) and Kendall (1955).
! Steps 2 and 4 are the awkward ones: B&M discharge them by pointing at a figure the source omits, so the two small tournaments have to be identified and checked from scratch. Everything else follows from theorem 10.7 and exercise 10.1.8.