Machine-Verified Bounds for Chowla's Cosine Problem

Chowla's cosine problem (Erdős problem #510) asks: for a set \(A = \{a_1, \ldots, a_N\}\) of distinct positive integers, how negative can \(\min_\theta \sum_{i=1}^N \cos(a_i \theta)\) be? The Erdős conjecture asserts a bound of order \(-c\sqrt{N}\), which remains open. We present the first machine-verified treatment of this problem in Lean 4 with Mathlib, comprising 72 files and approximately 500 declarations. The main proof chain uses zero sorry; one sorry appears only in a counterexample computation (concrete trigonometric arithmetic in Lean). One documented axiom is used for the quantitative Bohr set size path, with a fully proved axiom-free alternative via Bohr set averaging.

We prove three tiers of bounds. Tier 1 (all sets): \(\min_\theta S_A(\theta) \leq -1\) via eigenvalue pigeonhole, strengthened by a few-negatives dichotomy yielding \(-N^{1/3}\) when at most \(N^{2/3}\) eigenvalues are negative. Tier 2 (symmetric sets): for \(A = -A\) in \(\mathbb{Z}/N\mathbb{Z}\), there exists \(k \neq 0\) with \(|\mathrm{Re}\,\hat{1}_A(k)| \geq \sqrt{|A|(N-|A|)/(N-1)}\), a magnitude bound of order \(\sqrt{N}\) (sign undetermined). Tier 3 (iteration framework): the logical skeleton of Bourgain's (1986) density increment iteration — spectral dichotomy, Bohr set concentration, bounded termination — is formalized end-to-end, with the specific analytic estimates as verified preconditions.

We develop from scratch a complete Fourier-analytic toolkit on \(\mathbb{Z}/N\mathbb{Z}\): Parseval identities, spectral pigeonhole, Bohr set concentration inequalities, restricted Fourier analysis, Riesz product machinery, and a density iteration engine. The formalization itself constitutes the proof.

Keywords: Chowla's cosine problem, Erdős problem #510, Lean 4, formal verification, additive combinatorics, Bohr sets, Bourgain iteration.