Motivation

Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.

Setting

Work in an arbitrary abelian group $G$ (Lean: AddCommGroup G). For finite $X, Y \subseteq G$, the additive energy $E(X,Y)$ counts quadruples $(x,x',y,y')$ with $x + y = x' + y'$; the trivial maximum is $|X|^3$ when $|X| = |Y|$. The sumset $X + Y$ is $\{x + y\}$, and the difference set $X - Y$ is defined pointwise. A set has small doubling when $|X + X|$ is linear in $|X|$. The Lean development uses Finset.addEnergy and Finset.addConvolution from Mathlib.

A bipartite graph here is an edge set $E$ of type Finset (G × G) with $E \subseteq A \times^s B$, not a Mathlib SimpleGraph; solvers should state graph hypotheses that way. Given such an $E$, the partial sumset $A +_E B$ is $\{a + b : (a,b) \in E\}$, following Tao–Vu Definition 2.28.

Target

The mission goal is the two-set (equal-cardinality) form:

$$E(X,Y) \ge \eta |X|^3 \implies \exists X' \subseteq X, Y' \subseteq Y,\ |X'|,|Y'| \ge c|X|,\ |X' - Y'| \le C|X|.$$

This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps $c$ and $C$ existential; the explicit-constant variant is proved separately in the mission with $c = \eta/16$.

The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.

Significance

The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.

Formalizing it matters because the constants are the content: the development tracks explicit constants through dependent random choice (graph level $c = \delta/8$ and $C = 2^{13}K^3/\delta^5 + 2^{12}/\delta^5$; energy level $c_0 = \eta/16$ and $C_0 = 2^{13}(4/\eta)^3/(\eta/2)^5 + 2^{12}/(\eta/2)^5$), which paper proofs often leave implicit. Fox–Sudakov state the application for sets of integers; the formalization is over an arbitrary AddCommGroup, with no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1) contains no BSG statement, so this fills a genuine upstream gap.

Difficulty

The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.

Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's $a' \ne a$ and $b' \ne b$ terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.

Formalization scope

Sets are Finset G in an AddCommGroup G with DecidableEq; energy is Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise sumset and difference operations from open scoped Pointwise. Density hypotheses are stated with explicit real constants. The counting lemmas at the bottom of the development (sum_addConvolution_eq_card_product, path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are unconditional; the statements that need them carry the nonemptiness, equal-cardinality and density hypotheses that exclude degenerate zero-energy configurations. Welcome contributions: the single-set polynomial Freiman–Ruzsa consequences, and non-abelian variants.

Selected references

• A. Balog and E. Szemerédi, A statistical theorem of set addition, Combinatorica 14 (1994), 263–268.
• W. T. Gowers, A new proof of Szemerédi's theorem for arithmetic progressions of length four, Geom. Funct. Anal. 8 (1998), 529–551.
• J. Fox and B. Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011), 68–99 (Lemmas 5.1/5.2 and §5.1 BSG application).
• T. Tao and V. Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Definition 2.28 (partial sumsets), Theorem 2.29 (BSG, p. 79) and Lemma 2.30 (energy to partial sumset, p. 80).
• C. Reiher and T. Schoen, Note on the theorem of Balog, Szemerédi, and Gowers, Combinatorica 44 (2024), no. 3, 691–698 (arXiv:2308.10245).
• I. Ruzsa's inequalities via Mathlib's Finset.pluennecke_ruzsa_inequality_nsmul_add; see G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, Combinatorica 32 (2012), 721–733 (arXiv:1101.3507).
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, modules Combinatorics/Additive/BalogSzemerediGowers and BSGEnergyToGraph.