Asymmetric Balog–Szemerédi–Gowers theorem (qualitative)

Let $G$ be an arbitrary additive commutative group and $\eta > 0$. There exist constants $c > 0$ and $C > 0$, depending only on $\eta$, such that the following holds. Let $X, Y \subseteq G$ be nonempty finite sets with $|X| = |Y|$ whose additive energy satisfies

Then there exist subsets $X' \subseteq X$ and $Y' \subseteq Y$ with

Here $E(X,Y)$ counts the additive quadruples $x_1 + y_1 = x_2 + y_2$ with $x_i \in X$ and $y_i \in Y$, and $X' - Y' = \{x - y : x \in X', y \in Y'\}$ is the pointwise difference set. The cardinality bounds $c|X| \le |X'|$ and $c|Y| \le |Y'|$ already force $X'$ and $Y'$ to be nonempty, so no separate nonemptiness clause is needed.

This is the qualitative asymmetric form of the Balog-Szemeredi-Gowers theorem: large additive energy forces large subsets whose difference set is linear in $|X|$. The conclusion bounds the difference set $|X' - Y'|$, and this is not a restatement of a sumset bound. The graph step of the proof delivers a bound on the sumset, $|X' + Y'| \le C_0|X|$; converting that into the difference-set bound is a separate Ruzsa argument (Finset.ruzsa_sumset_to_difference) which costs a factor, replacing the sumset constant $C_0/c_0$ by $(C_0/c_0)^3/c_0 + 1$.

It is the top-level asymmetric conclusion of the project, deduced from the popular-sum graph construction, the graph (restricted-sumset) Balog-Szemeredi-Gowers theorem, and that Ruzsa conversion.