A certified lower bound for the first autocorrelation constant

Let C1 be the largest constant such that sup|t| ≤ 1/2 ∫ f(t−x) f(x) dx ≥ C1 (∫−1/41/4 f)2 for all nonnegative functions f on the real line. This constant governs the size of large generalized Sidon sets, and it is Problem 6.2 in the list of Georgiev, Gómez-Serrano, Tao and Wagner. The previous lower bounds include 1.28 by Cloninger and Steinerberger and 1.2937 by Kim and Pilanci. We prove C1 ≥ 1.32. Consequently, for all large g, the largest g-Sidon sets in {1, …, N} have fewer than 1.2310√(gN) elements once N is large. The proof starts from a reduction of Cloninger and Steinerberger: for each n, C1 is at least a finite min-max Vn of quadratic forms in the masses of f on n equal bins. We bound V30 from below by a spatial branch-and-bound over block masses. A linear relaxation with McCormick inequalities and square cuts closes the regions of the search, and every leaf carries an explicit dual vector. A checker written in Python evaluates the 24,935,952 leaf bounds in exact rational arithmetic. A second checker, written and proved sound in the Lean 4 proof assistant, accepts the same certificate by compiled evaluation. The bound C1 ≥ 1.31 also has a proof checked by the Lean kernel alone. The certificate, the programs and the Lean formalization are archived at doi:10.5281/zenodo.23480605 and available at github.com/tejasvi/autoconvolution-lower-bound.