TejasviTomar
October 2026 · Preprint

A certified lower bound for the first autocorrelation constant

Tejasvi Singh Tomar

In plain words

Spread sand along a stretch of the number line and add the positions of every pair of grains: the totals always crowd somewhere, and the first autocorrelation constant measures how little they can. Schinzel and Schmidt studied it in 2002; it is on a 2025 problem list by Georgiev, Gómez-Serrano, Tao and Wagner. Earlier proven lower bounds include 1.28 and 1.2937; the new one, 1.32, lowers the cap on how many whole numbers below a large limit can be chosen with no sum of two occurring more than a fixed, large number of times.

Abstract

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.

Twenty-two black bars of uneven heights, with gaps where eight of the thirty bins are empty, stand in a row above a wide inverted triangle of small teal bricks shaded from pale to deep; 112 of the bricks are yellow with black outlines, most of them in slanted diamond-shaped clusters.
Illustration of the reduction for 30 bins. Top: an explicit mass vector on 30 equal bins of [−1/4, 1/4], found by local search, which gives the paper's upper bound V₃₀ ≤ 1.331221; bar heights are proportional to the masses, and eight bins are empty. Below: one brick for each of the 1,770 windows of [−1/2, 1/2], placed by the window's centre (left to right) and its length (growing downwards), and shaded darker teal the larger its averaged mass. The 112 yellow bricks are the windows whose averaged mass equals the largest, 1.33122…, to within 10⁻¹¹. The paper proves that for every mass vector of total mass 1 on 30 bins some window has averaged mass at least 1.32, which gives C₁ ≥ 1.32.