Tournaments, \(\bar\omega \)-criticality, and directed paths
The formal statements of the digraph-theory library, for mathematicians

1 How to use this site

This site lets a mathematician audit, without reading any proof or learning any proof assistant, what exactly has been machine-checked in the digraph-theory library:

  • for every \(k \in \{ 3,4,5\} \) there are infinitely many \(k\)-\(\bar\omega \)-critical tournaments (Conjecture 5.10 of Aboulker–Aubian–Charbit–Lopes, arXiv:2310.04265, at every value of \(k\) for which it is humanly known) — 3.1;

  • Question 5.9 of the same paper fails at each such \(k\) — 3.3, 3.5, 3.7;

  • the \(\delta = 3\) case of the Cheng–Keevash path conjecture: every oriented digraph with minimum out-degree \(\ge 3\) contains a directed path of length 6 — 5.1;

  • the general tournament theory behind them (substitution bound, vertex-transitive criticality, domination, uniqueness of the 2-critical tournament).

The division of labour.

The Rocq kernel has checked every proof; each result here reports axiom-free status (Print Assumptions: closed under the global context). Proofs are therefore not shown. What a human must check is that the statements say what the informal mathematics means — so every result page shows the verbatim formal statement, a plain-mathematics decoding, and machine-generated uses links to every definition the statement depends on (the Dictionary, 2). Use the dependency graph to explore: a result’s ancestors are exactly the definitions you must read to trust it.

Generated, not curated.

The dependency edges are computed from the compiled library by scripts/statement_closure.py; continuous integration fails if a statement’s closure ever contains a definition without a Dictionary entry, or if a quoted text drifts from the source.

Conventions.

Statements are quoted verbatim. Boolean connectives (==, &&, [forall ...]) are MathComp’s decidable counterparts of the usual logical ones — equivalent to them on the finite structures used here. The circulant families use the index convention \(m =\) m’.+1, \(n =\) m.*2.+1 with hypothesis 3 <= m’.+1: \(n\) ranges exactly over the odd numbers \(\ge 7\). A statement quoted from inside a Section is implicitly universally quantified over the section’s parameters. A companion PDF with the same content plus a notation primer and the full declaration catalog is available as digraph_formal.pdf; the per-file API documentation (coqdoc) is under /doc.