A certified upper bound for the beat the average game

Let C be the supremum of P[X_1 + X_2 + X_3 < 2X_4] over all probability measures on [0, ∞), where X_1, ..., X_4 are independent with the given law. This is Problem 6.39 in the list of Georgiev, Gómez-Serrano, Tao and Wagner. Bellec and Fritz proved 0.4006953 ≤ C ≤ 673/1615 < 0.41672 and conjectured that the lower bound is the exact value. We prove C ≤ 4006983/10000000 = 0.4006983, which is within 3·10^-6 of the conjectured value. The proof applies the flag algebra method of Razborov to samples of eight points. After sorting, such a sample determines which of the 280 inequalities 2x_d > x_a + x_b + x_c among its coordinates hold, and the probability in question is the expected fraction of these inequalities that hold. Independence of the sample imposes positive semidefinite constraints on the distribution of these sign patterns, and since they hold for every measure, no limit argument is needed. We combine them in a semidefinite program, round its solution to an exact sum of squares, and evaluate the bound in exact rational arithmetic on all 45,319,744 patterns of eight points whose restrictions to seven points are realizable. Gordan certificates exclude the two of these patterns that exceed the bound, and trees of Gordan certificates show that the list of realizable patterns of seven points is complete. A checker that uses only the Python standard library verifies the certificate. The certificates and the programs are archived at doi:10.5281/zenodo.23506055. The programs and the certificates for 6 and 7 points are also available at github.com/tejasvi/beat-the-average-bound.