Add Caccetta–Häggkvist conjecture (directed cycles vs minimum out-degree)

[henrykmichalewski]

This PR adds the Caccetta–Häggkvist conjecture (1978) as FormalConjectures/Wikipedia/CaccettaHaggkvistConjecture.lean.

Statement. Every simple digraph on $n \ge 1$ vertices in which every vertex has out-degree at least $n/r$ contains a directed cycle of length at most $r$. The degree hypothesis is stated in the integer form $n \le r \cdot \operatorname{outdeg}(v)$.

Encoding.

• Uses Mathlib's Digraph V; "simple" is captured by an Irreflexive G.Adj hypothesis (loops forbidden, digons allowed, matching the standard statement).
• A directed cycle of length $k$ is an injective map $f : \mathbb{Z}/k\mathbb{Z} \to V$ with $f(i) \to f(i+1)$ an arc for all $i$ (HasDirectedCycleOfLength, defined locally with a docstring since Mathlib has no digraph cycle API).
• Out-degree is defined locally (outDegree) as a filtered-univ cardinality, since Mathlib's Digraph has no degree API.
• A 1 ≤ n hypothesis excludes the empty digraph, for which the degree hypothesis is vacuous but the conclusion fails.

Contents.

• caccetta_haggkvist — the conjecture, @[category research open, AMS 5] (open since 1978).
• variants.caccetta_haggkvist_triangle — the famous $r = 3$ special case (minimum out-degree $\ge n/3$ forces a directed cycle of length $\le 3$), also research open.
• Two @[category test] sanity checks, both closed by decide without sorry: the complete loopless digraph on 3 vertices has a directed 3-cycle, and each of its vertices has out-degree 2.

Sorry count: 2 (the two open conjecture statements only).

🤖 Generated with Claude Code

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

Thanks, lgtm, except for the hallucinated link and one of the defintions, see comments...

[mo271]

this link is hallucinated. Let's instead use https://www.openproblemgarden.org/op/caccetta_haggkvist_conjecture and move this file to a new directory "OpenProblemGarden"!

[mo271]

This should be either inlined (my preference) or moved to FormalConjecturesForMathlib.
Surprising how much stuff is missing for digraphs...