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√3-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 theorem, including this passage, is formalized in Lean with compiled evaluation. Proved in Lean, with compiler-trusted finite checks; not yet reviewed by experts. Produced by AI models under the author's direction.