2 The Dictionary: every definition you need
HB.mixin Record HasArc V := { arc : rel V }.
Notation "u --> v" := (arc u v) (at level 30) : digraph_scope.
Source: theories/core/digraph.v:35
A digraph is a (finite, in this document) vertex type equipped with an arc relation. The library roots its own hierarchy on a bare relation:
rel V is the type of Boolean binary relations on V; u –> v is notation for arc u v, “there is an arc from \(u\) to \(v\)”. A diGraphType is a finite type bundled with such a relation, with no further axioms.
Why this is the right definition. No axioms at this level means nothing is smuggled in: loops and 2-cycles are not yet excluded. They are excluded exactly where the mathematics requires it — by the oriented/tournament axioms below. Isomorphism of digraphs is the evident notion (2.2).
Definition dgiso (D1 D2 : diGraphType) : Prop := exists f : D1 -> D2, bijective f /\ forall u v, (f u --> f v) = (u --> v).
Source: theories/core/digraph.v:97
A bijection between the vertex types that preserves and reflects arcs (\(f u \to f v\) iff \(u \to v\), as Booleans).
HB.mixin Record DiGraph_IsOriented V of DiGraph V := {
arc_irrefl : irreflexive (arc : rel V);
arc_asymm : forall u v : V, arc u v -> arc v u = false
}.
Source: theories/core/oriented.v:33
An oriented digraph (an “oriented graph” in the combinatorics literature) has no loops and no digons:
arc_irrefl forbids loops; arc_asymm says \(u \to v\) and \(v \to u\) cannot both hold. The bundled structure is orientedDigraph.
Definition outdeg v := #|[set w | v --> w]|.
Source: theories/core/oriented.v:47
The number of out-neighbours of \(v\): \(d^+(v) = |\{ w : v \to w\} |\). The path results state their hypothesis as “forall v, k <= outdeg v”, i.e. minimum out-degree \(\delta ^+ \ge k\).
HB.mixin Record Oriented_IsTournament V of Oriented V := {
arc_total : forall u v : V, (u != v) = (arc u v) (+) (arc v u)
}.
Source: theories/core/tournament.v:32
A tournament orients every pair: for distinct \(u,v\) exactly one of \(u \to v\), \(v \to u\) holds.
(+) is exclusive or, so the axiom reads: \(u \ne v\) iff exactly one of the two arcs is present. Together with irreflexivity (inherited from Oriented) this is precisely the textbook definition. The bundled structure is tournament.
Why this is the right definition. On the diagonal the axiom specialises to \(\mathrm{false} = (u \to u) \oplus (u \to u)\), which holds trivially — irreflexivity is genuinely carried by the Oriented layer, and totality by this one; no case is lost.
Definition transb := [forall u : T, [forall v : T, [forall w : T, (u --> v) ==> (v --> w) ==> (u --> w)]]].
Source: theories/core/tournament.v:112
The Boolean “the arc relation is transitive”. Transitive tournaments are exactly the linearly ordered ones; they are the tournaments with \(\bar\omega = 1\) (omegabar_transb, 6.7).
Definition C3 : Type := 'Z_3. Lemma arcC3E (u v : C3) : (u --> v) = (v == u + 1 :> 'Z_3).
Source: theories/core/tournament.v:183
Vertices \(\mathbb {Z}/3\), arcs \(u \to u+1\): the 3-cycle \(0 \to 1 \to 2 \to 0\), the smallest non-transitive tournament.
Definition ltp p u v := enum_rank (p u) < enum_rank (p v).
Definition realize : {perm V} := perm rfun_inj.
Lemma ltp_realizeE u v : ltp realize u v = r u v.
Source: theories/core/order.v:39
\(\bar\omega \) quantifies over orderings of the vertex set. The library represents an ordering by a permutation \(p\), compared through the position of the enumeration:
ltp p u v reads “\(u\) precedes \(v\) in the order named by \(p\)”.
Why this is the right definition. Two directions need checking. (i) Every ltp p is an irreflexive, transitive, total comparison — a strict linear order on the vertices. (ii) Conversely, every strict linear order arises this way: realize turns any irreflexive transitive total relation r into a permutation, and ltp_realizeE states ltp realize u v = r u v. So quantifying over {perm T} is quantifying over all \(|T|!\) vertex orders — no order is missed, which is what makes the minimum in \(\bar\omega \) honest.
Definition backedge_rel : rel T := [rel u v | ltp p u v && (v --> u) || ltp p v u && (u --> v)]. Definition backedge : sgraph := SGraph backedge_sym backedge_irrefl. Lemma backedgeE (u v : backedge) : (u -- v) = ltp p u v && (v --> u) || ltp p v u && (u --> v).
Source: theories/core/order.v:136
Fix a tournament \(T\) and an order \(p\). The backedge graph has an (undirected) edge between \(u\) and \(v\) when the arc between them points backwards with respect to \(p\):
sgraph is the simple-graph type of the coq-graph-theory library, whose clique machinery (cliques, omega) is reused unchanged; u – v is its edge relation.
Why this is the right definition. A set \(K\) is a clique of the backedge graph iff, listing \(K\) in \(p\)-increasing order, every later vertex beats every earlier one — i.e. \(K\) is a “reverse-ordered” subtournament under \(p\). This is the standard combinatorial reading of backedge cliques.
Definition omegab_at (T : tournament) (p : {perm T}) : nat :=
ω([set: backedge p]).
Definition omegabar (T : tournament) : nat :=
omegab_at [arg min_(p < (1%g : {perm T})) omegab_at p].
Source: theories/invariants/omegabar.v:29
omegab_at p is the clique number of the backedge graph of the order \(p\) (graph-theory’s omega of the full vertex set); omegabar takes the minimum over all \(p\) ([arg min_(...)] is MathComp’s minimiser over the finite type {perm T}). The display notation in the source is the omega-bar of the quoted statements.
Why this is the right definition. \(\bar\omega (T) = \min _{\prec } \omega (\mathrm{BE}(T,\prec ))\) over all \(|T|!\) linear orders \(\prec \), by the realization argument of 2.8. This matches Aboulker–Aubian–Charbit–Lopes (arXiv:2310.04265, where the invariant measures the distance of \(T\) from transitivity); \(\bar\omega (T) = 1\) iff \(T\) is transitive (6.7).
Definition kcritical (k : nat) (T : tournament) : bool := (ω̄(T) == k) && [forall v : T, ω̄(del_tournament v) == k.-1].
Source: theories/invariants/critical.v:21
\(T\) is \(k\)-critical when \(\bar\omega (T) = k\) and deleting any single vertex drops \(\bar\omega \) to \(k-1\). The [forall v : T, ...] ranges over all vertices; k.-1 is \(k - 1\).
Definition sub_tournament (T : tournament) (S : {set T}) : tournament :=
{x : T | x \in S} : tournament.
Definition del_tournament (T : tournament) (v : T) : tournament :=
sub_tournament [set~ v].
Lemma sub_arcE (u v : {x | P x}) : (u --> v) = (val u --> val v).
Source: theories/core/tournament.v:171
For \(S \subseteq V(T)\), sub_tournament S is the induced subtournament: its vertices are the elements of \(S\) (a dependent-pair type, whose first projection val is the underlying vertex) and its arcs are inherited verbatim (sub_arcE). Deleting \(v\) is the special case \(S = V \setminus \{ v\} \) ([set~ v]).
Definition dominatesb (X : {set T}) : bool :=
[forall v : T, (v \in X) || [exists x in X, x --> v]].
Definition domnum : nat := #|[arg min_(X < [set: T] | dominatesb X) #|X|]|.
Source: theories/invariants/domination.v:28
\(u\) dominates \(v\) if \(u = v\) or \(u \to v\); \(\mathrm{dom}(T)\) is the least size of a set dominating every vertex. Used in the general bound \(\mathrm{dom}(T) \le \bar\omega (T)\) (6.4).
Definition autb p : bool :=
[forall u : D, [forall v : D, arc (p u) (p v) == arc u v]].
Definition dgaut : {set {perm D}} := [set p | autb p].
Source: theories/constructions/automorphism.v:25
A permutation of the vertices preserving arcs in both directions; dgaut is the set of all of them (a group).
Definition vertex_transitiveb : bool :=
[forall u : D, [forall v : D,
[exists p : {perm D}, (p \in dgaut) && (p u == v)]]].
Source: theories/constructions/automorphism.v:55
For every pair of vertices some automorphism carries one to the other. All three critical families here are vertex-transitive — which is why checking one deletion suffices (6.2).
Definition lexprod : Type := (D1 * D2)%type. Lemma lexprod_arcE (u v : lexprod) : (u --> v) = (u.1 --> v.1) || (u.1 == v.1) && (u.2 --> v.2). Definition lexprod_tournament (T1 T2 : tournament) : tournament := lexprod T1 T2 : tournament.
Source: theories/constructions/product.v:25
Vertices are pairs \((s,h)\); between different \(S\)-blocks the arc follows the \(S\)-arc of the first coordinates, inside a block it follows \(H\) (lexprod_arcE is the characterising equation: the arc is (u.1 –> v.1) || (u.1 == v.1) && (u.2 –> v.2), and for tournaments the first disjunct can only fire when \(u.1 \neq v.1\)). This is the standard substitution/composition \(S[H]\): every block is a copy of \(H\), blocks are arranged as \(S\).
Definition cayley (gT : finGroupType) (A : {set gT}) : Type := gT.
Lemma cayley_arcE (x y : cayley A) : (x --> y) = ((x^-1 * y)%g \in A).
Source: theories/constructions/cayley.v:30
For a finite group \(G\) and connection set \(A \subseteq G\): vertices \(G\), arc \(x \to y\) iff \(x^{-1}y \in A\). Over \(\mathbb {Z}/n\) (written additively) this is the circulant: \(x \to y\) iff \(y - x \in A\).
Definition ACset : {set 'Z_n} :=
[set z : 'Z_n | ((0 < val z < m) || (val z == m.+1))%N].
Definition AC : tournament := cayley ACset : tournament.
Lemma AC_arcE (x y : AC) : (x --> y) = (y - x \in ACset).
Source: theories/constructions/circulant.v:63
The paper’s witness platform: for odd \(n = 2m+1\), the circulant with connection set \(g = \{ 1, \dots , m-1\} \cup \{ m+1\} \):
(val z is the representative of \(z \in \mathbb {Z}/n\) in \(\{ 0,\dots ,n{-}1\} \); the set comprehension says \(0 {\lt} \mathrm{val}\, z {\lt} m\) or \(\mathrm{val}\, z = m+1\).) Since \(g\) contains exactly one of \(\{ z, -z\} \) for each \(z \ne 0\), \(\mathrm{AC}_n\) is a tournament; as a Cayley digraph it is vertex-transitive. Throughout, \(m\) is m’.+1 and \(n\) is m.*2.+1 (??). In statements quoted from section contexts, the local abbreviations ACm, m, n denote AC m’, m’.+1, m.*2.+1.
T5 abbreviates lexprod_tournament ACm ACm: \(\mathrm{AC}_n\) substituted into itself, a vertex-transitive tournament on \(n^2\) vertices.
Definition dipath x s := path arc x s && uniq (x :: s).
Source: theories/core/dipath.v:36
path arc x s (MathComp) says consecutive elements of x :: s are joined by arcs; uniq makes the path simple. Its length (number of arcs) is size s.
Definition has_dipath k := [exists x : D, exists t : k.-tuple D, dipath x t]. Definition ell := \max_(k < #|D| | has_dipath k) (k : nat).
Source: theories/core/dipath.v:144
\(\ell (D)\) is the largest \(k\) for which a directed simple path with \(k\) arcs exists (_(...) over the finite range; a simple path has at most \(|D| - 1 {\lt} |D|\) arcs, so the bounded maximum is the true maximum). The display notation in the source is the script ell of the quoted statements.
Definition strongb := [forall x : D, forall y : D, connect arc x y].
Source: theories/invariants/strong.v:37
Every vertex reaches every other by a directed walk (connect is MathComp’s reflexive-transitive closure).