The Turán density of the tight five-cycle

The tight five-cycle is the three-uniform hypergraph whose edges are the five cyclically consecutive triples on five distinct vertices. We prove that its Turán density is $2\sqrt3-3$. This answers the conjecture usually attributed to Mubayi and Rödl, explicitly stated by Mubayi, Pikhurko and Sudakov. Mubayi and Rödl's recursive construction gives the lower bound. The upper bound follows the reduction of Bodnár, León, Liu and Pikhurko, whose theorem concerns forbidding both the tight four-cycle and the tight five-cycle, or a tight cycle of length at least seven not divisible by three. We establish the two estimates needed for the five-cycle alone by exact rational certificates, using weighted link inequalities to include configurations containing a complete four-vertex hypergraph. We give the finite counting argument that turns the certificates into these estimates and then into the density bound. The whole proof, including this counting argument, is checked in Lean; its finite computations run as compiled code, so the check trusts Lean's compiler as well as its kernel. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Proved in Lean, with compiler-trusted finite checks; not yet reviewed by experts. Produced by AI models under the author's direction.