A New Upper Bound for the Tur\'an Density of the Tetrahedron
En palabras de los autores
We prove that the Tur\'an density of the tetrahedron satisfies , improving Baber's upper bound of and closing about of the gap to the conjectured value . The proof uses an exact seven-vertex flag-algebra certificate incorporating degree-stationarity from Razborov's differential method. To find the certificate, we combine the established techniques of cutting planes and column generation to optimize jointly over flag families whose types have at most five vertices. We give a complete formal proof of this Tur\'an density bound in Lean 4.
Apareció: jueves, 24 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: 28 pages, 5 figures, 8 tables. Lean 4 formalization, exact certificate and code: https://github.com/taeyool/tetrahedron-turan