Caccetta–Häggkvist conjecture: force a short directed cycle

Prove that a finite loopless digraph on n ≥ 1 vertices with minimum outdegree at least d has a directed cycle of length at most ceil(n/d), when d ≥ 1. The Lean formulation avoids division: for any positive r with n ≤ r*d it asks for a cycle of length at most r. Outdegree is witnessed by d distinct outgoing neighbours for each vertex. Cycle vertices are distinct, and the final edge returns to the first vertex. The graph need not be symmetric; reverse edges are allowed. Research status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.

∀ n d r : Nat, 1 ≤ n → 1 ≤ d → 1 ≤ r → n ≤ r * d →
  ∀ E : Fin n → Fin n → Bool, (∀ v, E v v = false) →
  (∀ v, ∃ f : Fin d → Fin n, (∀ i j, f i = f j → i = j) ∧ (∀ i, E v (f i) = true)) →
  ∃ k : Nat, k + 1 ≤ r ∧ ∃ f : Fin (k + 1) → Fin n,
    (∀ i j, f i = f j → i = j) ∧
    (∀ i, E (f i) (f ⟨(i.val + 1) % (k + 1), Nat.mod_lt _ (Nat.zero_lt_succ k)⟩) = true)

OA_statement : Prop