A New Upper Bound for the Tur\'an Density of the Tetrahedron

1 Introduction

• 312372062889819/560000000000000 < 0.557808 is the new upper bound, improving Baber’s 0.5615 bound.The bound closes about 62% of the gap to the conjectured value 5/9.Source: §1 · p. 2
• The certificate combines flag-algebra inequalities with degree-stationarity from Razborov’s differential method [19, §4.3].It is an exact seven-vertex certificate; the new bound reduces the gap to 5/9 from approximately 0.00594444 to 0.00225170.Source: §1 · p. 2
• Searching over all 23 tetrahedron-free five-vertex types and selected smaller types creates an SDP with matrices up to 1024 × 1024 and over a million inequalities.The scale of this computation is identified as the main computational challenge.Source: §1 · p. 2
• Cutting planes and column generation make the search tractable by iteratively adding rank-one PSD matrices and violated coefficient inequalities to smaller linear programs.Positive combinations of rank-one matrices ensure positive semidefiniteness while their weights are optimized by linear programming.Source: §1 · p. 2
• The numerical candidate is converted to rational data and checked with exact arithmetic, and the complete bound is formally proved in Lean 4.The exact checks verify the bound, positive semidefiniteness, and all coefficient inequalities.Source: §1 · p. 2

2.1 Types, flags and densities

• A type is a tetrahedron-free 3-graph on labeled vertices, and a flag adds labeled roots; flag densities are probabilities of seeing induced flags.Pair densities use two disjoint sets of non-root vertices sharing the same roots.Source: §2.1 · p. 3

2.2 The flag algebra

• The flag algebra is a quotient that identifies expansion relations, and its product models the asymptotic joint density of flags sharing roots.The probability that independently sampled non-root sets overlap is O(1/n), so conditioning on disjointness changes probabilities by a vanishing amount.Source: §2.2 · p. 4

2.3 Positive homomorphisms

• Positive homomorphisms encode limits of convergent flag sequences, allowing the extremal density to be expressed as an optimization over them.They are linear, multiplicative, normalized maps that are nonnegative on every flag.Source: §2.3 · pp. 4–5

2.4 The downward operator

• The downward operator averages over root labelings while forgetting the labels, and it maps nonnegative flag-algebra elements to nonnegative unrooted elements.The averaging accounts for the probability of a root placement as well as removing its label.Source: §2.4 · p. 5

2.5 Stationarity constraint

• Every maximizer of edge density is degree-stationary: the normalized degree of a uniformly random vertex has vanishing variance in a representing convergent sequence.The stationarity constraint follows from Razborov’s criterion applied at an edge-density maximizer.Source: §2.5 · p. 6

3.1 Certificate criterion

• Proposition 3.1 certifies an upper bound when every block matrix is positive semidefinite and every coefficient c_G is at most B.Source: §3.1 · p. 7

3.2 The seven-vertex certificate

• The seven-vertex certificate uses rational factorizations to ensure positive semidefiniteness and integer evaluations to verify its coefficient bound.The proof establishes that C7(G) is an integer for every G in F0^7.Source: §3.2 · p. 8
• The exact certificate proves Theorem 1.1 with B = 312372062889819/560000000000000.The maximum coefficient divided by L gives this bound, and rational factorizations complete the certificate verification.Source: §3.2 · p. 9
• Lean 4 formalizes the full proof without omitted proofs or extra user-declared axioms, though compiled finite checks require trusting Lean’s compiler.Source: §3.2 · p. 9

4.1 Semidefinite program

• The search minimizes B over positive semidefinite block matrices and a stationarity multiplier, requiring c_G(Q, τ) ≤ B for every tetrahedron-free seven-vertex 3-graph.Any feasible solution gives an upper bound; optimality is not required.Source: §4 · p. 9, §4.1 · p. 9
• The search uses 32 blocks, but only 23 have nonzero matrices in the final certificate; block dimensions count flags and give PSD matrix side lengths.The blocks use flag products on six or seven vertices.Source: §4.1 · p. 9, Table 2 · p. 10

4.2 Cutting planes and column generation

• Restricting each PSD matrix to nonnegative combinations of selected rank-one matrices makes positive semidefiniteness automatic and turns weight optimization into a linear program.The search also enforces coefficient inequalities on a subset of tetrahedron-free seven-vertex graphs, gradually enlarging it.Source: §4.2 · p. 10
• Cutting planes add violated coefficient constraints, while column generation adds matrix terms that may permit a smaller B after reoptimization.The search tracks the smallest feasible upper bound seen and converts the associated matrices and multiplier into an exact certificate.Source: §4.2 · pp. 10–11
• Dual multipliers identify candidate new vectors: negative eigenvalues signal terms that may allow a smaller B after reoptimization.The procedure selects up to 80 vectors associated with the most negative eigenvalues, requiring each selected eigenvalue to be below −10^-7.Source: §4.2 · p. 11

4.3 Efficient coefficient evaluation

• Coefficient evaluation reuses six-vertex computations across seven-vertex graphs, reducing the combined edge-density, stationarity, and six-block contribution to seven table lookups per graph.There are 964 six-vertex 3-graphs in the stated expansion.Source: §4.3 · p. 11
• For five-root blocks, a precomputed matrix incorporates type automorphisms, so each graph’s contribution can be evaluated over 21 five-vertex subsets instead of up to 2520 injections.The same precomputed matrix is reused across the seven-vertex graphs.Source: §4.3 · pp. 11–13

5 Computational experiments

• The experiments assess which optimization techniques work well for these tetrahedron SDPs and which additional flag types improve the bounds.The tested formulations vary in included flag types, flag sizes, and expansion size.Source: §5 · p. 13, §5.3 · p. 15

5.3.2 Effect of five-root blocks

• 312372062889819/560000000000000 < 0.557808 is the exact bound established by the six-hour certificate search.The experiments report that the search used all 23 five-root types.Source: §5 · p. 13

5.1 Experimental design

• The study compares four optimization methods on four flag-algebra SDPs, all using the edge-density objective and degree-stationarity condition.Each of 13 SDP–method combinations was run three times with a one-hour search budget; initialization and exact verification were excluded.Source: §5.1 · pp. 13–14

5.2.1 Expansion size m = 6

• On M6, column-generation methods obtained bounds near 0.56167 and met stopping criteria before one hour, while LP-CG was faster than LP-CUT-CG.LP-CG took a median 5.16 seconds versus 6.91 seconds; cutting planes reduced retained 3-graphs from 964 to 305 but increased LP iterations from 58 to 139.Source: Table 3 · p. 14, §5.2.1 · p. 15

5.2.2 Expansion size m = 7

• On both tested m = 7 SDPs, LP-CUT-CG gave the strongest bound within the one-hour budget among the four methods.The comparison covered M7-no5 and M7-all5.Source: §5.2.2 · p. 15, Table 4 · p. 15, Figure 2 · p. 16
• On M7-all5, LP-CUT-CG used less than 1/7 the peak memory of LP-CG and improved the verified bound from approximately 0.560454 to 0.558581.It completed about 253 iterations in one hour, compared with 32 for LP-CG.Source: §5.2.2 · p. 15, Table 4 · p. 15, Figure 2 · p. 16

5.3.1 Expansion size and flag blocks

• Increasing m from 6 to 7 with blocks fixed brought no observed improvement, whereas adding one- and three-root blocks and then five-root blocks improved the bounds.The reported sequence was approximately 0.561671 to 0.559210, then to 0.558581.Source: §5.3.1 · p. 16, Figure 3 · p. 17

5.3.2 Effect of five-root blocks

• Jointly optimizing over all 23 five-root types improved the verified bound from approximately 0.559210 to 0.558581 in the one-hour comparison.Neither SDP was solved to optimality, so the experiments do not establish a strict difference between their optima.Source: Table 5 · p. 16, §5.3.2 · p. 17

A Certificate data and exact verification

• The appendix describes the five-root block data used by the certificate.It also derives integer formulas for the certificate coefficients and explains exhaustive verification of the coefficient bound.Source: A Certificate data and exact… · p. 20
• Integer formulas for the certificate coefficients are derived from the block data.Source: A Certificate data and exact… · p. 20
• The coefficient bound in Proposition 3.2 is verified exhaustively.Source: A Certificate data and exact… · p. 20

A.1 Five-root block data

• The five-root types are the 23 tetrahedron-free 3-graphs on five vertices up to isomorphism, and the certificate has nonzero matrices for 18 of them.For each listed type, the appendix gives the six-vertex flag dimension and factor count.Source: §A.1 · p. 20

A.2 Integer coefficient formulas

• The verification clears the common denominator L = 5040M^2 and computes the integer numerator C7(G) = L cG.It evaluates six-vertex terms once per six-vertex graph and the remaining blocks directly on each seven-vertex graph.Source: §A.2 · pp. 20–21
• For four-root blocks, the six-vertex count matrix averages over 720 root assignments and weights flag pairs using factor vectors.Summing over the factor vectors gives the coefficient of the block at H.Source: §A.2 · p. 21
• For the stationarity coefficient, counts of disjoint-edge pairs and pairs of edges intersecting in one vertex give coefficients n1(H)/60 and n2(H)/180.The verification code computes 3n1(H) − n2(H) directly.Source: §A.2 · p. 21
• The edge-density coefficient at H is |E(H)|/20, and combining it with block and stationarity coefficients yields an integer comparison equivalent to cG ≤ B.The appendix gives the resulting block terms and sums over the 18 five-root types used in the certificate.Source: §A.2 · pp. 21–22
• For one-, three-, and five-root blocks, the formulas use count matrices or grouped counts, with denominators determined by the number of choices.The five-root contribution is expressed as 2Tσ(G; Qσ) after clearing the common denominator.Source: §A.2 · pp. 21–22

A.3 Exhaustive verification

• The coefficient evaluation checks factor-vector dimensions and bounds intermediate and final integer values to prevent overflow.Source: §A.3 · p. 22
• The exhaustive scan extends each of 964 tetrahedron-free six-vertex representatives and retains 13,051,375 tetrahedron-free extensions.Every tetrahedron-free seven-vertex 3-graph occurs among these extensions up to isomorphism.Source: §A.3 · p. 22
• Two implementations agree on the maximizing 3-graph and the exact maximum in Proposition 3.2’s coefficient bound.They cross-check the seven-vertex terms, while a Python script additionally confirms selected component values.Source: §A.3 · p. 22
• The Lean formalization independently proves the six-vertex catalog and seven-vertex extension coverage, then checks coefficient inequalities by exhaustive computation.For five-root blocks, it proves the grouped sum equals the sum over root labelings.Source: §A.3 · p. 22

B.1 Optimization procedure

• Each iteration solves a restricted LP, scans for violated coefficient constraints, and adds new constraints or eigenvector directions from negative eigenvalues.If selected constraints are already present, selected vectors are added instead; convergence tests remain unchanged.Source: §B.1 · p. 23

B.2 The dual SDP and LP

• The dual LP uses weights supported on the current constraint set and tests matrix positivity only along selected vectors, whose negative-eigenvalue directions guide column generation.Its multipliers also recover the certificate variables, so one LP solve supplies both the coefficient-scan inputs and eigenvalue-calculation inputs.Source: §B.2 · pp. 23–24

B.3 Constructing the exact certificate

• To construct the exact certificate, the search factors are reduced by SVD, small singular directions are discarded, and retained coordinates are rounded to rational multiples of 1/M.The rounded factor representations preserve positive semidefiniteness; the stationarity multiplier is also rounded before exact coefficient verification.Source: §B.3 · pp. 24–25
• Exact coefficient checks establish cG ≤ B for every tetrahedron-free seven-vertex 3-graph, and the rational matrices are positive semidefinite, completing the certificate.The selected floating-point solution is converted to rational matrices and its coefficient maximum is recomputed exactly.Source: §B.3 · p. 25

• The appendix section collects settings, verification procedures, and additional measurements for the experiments in Section 5.Source: C Experimental settings and additional… · p. 25

• The six blocks with 2ℓ−s = 6 have dimensions 2, 11, 64, 56, 50, and 45; the added smaller blocks yield 9, 12, or 35 blocks across the listed seven-vertex methods.The three smaller blocks are retained for optimization availability, but their matrices are zero in the final certificate.Source: §C.1 · p. 25
• All four optimization methods tested the global coefficient maximum against the solver objective and each block’s minimum eigenvalue (at least −10^-7); successful termination also required normalization, stationarity, and nonnegativity tests to meet 10^-7 tolerances.Source: §C.1 · p. 25
• Trials ran sequentially on Windows 11 with an Intel Core i7-14700K, 63.72 GiB RAM, and a 40 GiB process-memory cap.HiGHS and SCS were the LP and SDP solvers; solver and linear-algebra calculations used one thread.Source: §C.1 · p. 25
• For the seven-vertex LP-CG and SDP-FULL runs, precomputed coefficient and deletion-probability data occupied 17.93 GB for M7-no5 and 20.42 GB for M7-all5.Constructing those data took 110.20 and 132.33 seconds, respectively, and setup costs were excluded from search timings.Source: §C.1 · pp. 25–26
• HiGHS used 10^-9 feasibility tolerances and SCS used 10^-8 tolerances, distinct from the 10^-7 overall-search convergence tests.Generated SDP runs used a 300-second limit per restricted solve; settings were fixed within each group of three repetitions.Source: §C.1 · p. 26
• Exact verification selected only fully evaluated candidate pairs, converted them to rational certificates, and recomputed the largest coefficient over the full graph set.For SDP methods, negative eigenvalues of exported matrices were replaced by zero before rounding; this supports valid bounds even when the solver had not reached dual feasibility.Source: §C.1 · p. 26

• 2,859 and 5,078 inequalities were retained by LP-CUT-CG on M7-no5 and M7-all5, versus 1,295,600 for methods without cutting planes.Table 7 compares computational costs and final retained inequality and vector counts across four methods on two seven-vertex SDPs.Source: §C.2 · p. 27
• SDP-FULL and SDP-CUT spent most of their running time in solver calls, whereas LP-CUT-CG’s dominant cost was coefficient evaluation.Source: §C.2 · p. 27
• 77% and 81% of LP-CUT-CG recorded runtime went to evaluating cG(Q, τ) across seven-vertex graphs on M7-no5 and M7-all5, respectively.This evaluation computes U and identifies violated constraints, even with the reductions described in Section 4.3.Source: §C.2 · p. 27

C.3 Longer searches

• Both six-hour LP-CUT-CG searches improved on their one-hour bounds; M7-no5 reached approximately 0.558917, while M7-all5 reached approximately 0.557807255.The M7-all5 run used the Appendix B.1 procedure, which allows column generation whenever no new constraint is added; one-hour runs did so only when U − B ≤ 10^-7.Source: §C.3 · p. 27
• 312372062889819/560000000000000 (approximately 0.557807255) is the M7-all5 bound stated in Theorem 1.1.The corresponding certificate is presented in Section 3.Source: §C.3 · p. 27
• Approximately 0.561653 was the six-hour SDP-FULL bound on M6, only a small improvement over its one-hour bound; all three searches exhausted their time budgets without establishing the SDP optimum.For M6, the solver iteration limit was raised from one million to 20 million.Source: §C.3 · p. 27
• Figure 5 tracks the smallest floating-point U found during the fresh six-hour searches on common logarithmic axes, with crosses marking exact certificate bounds.Open circles mark the first available SDP-FULL candidate; the M6 square is a separate one-hour reference run with a 20-million iteration limit.Source: Figure 5 · p. 28