Freiman-Ruzsa bound from Bogolyubov and linear modelling (source code)

= Freiman-Ruzsa bound from Bogolyubov and linear modelling
{c}
{title2=$|\operatorname{span}A|\le C^4\,2^{1+\lceil C^5 2^{\lceil32C^{24}\rceil}\rceil}|A|$}

Let $A$ be a nonempty subset of $\mathbb F_2^N$ with <doubling constant> at most $C\ge1$. Translate to $B=A+a$ containing zero. The <Petridis minimal-growth lemma> and <Ruzsa triangle inequality> bound $|kB|\le C^k|B|$. In <injective linear modelling of a small sumset>, the image has density at least $1/(4C^{12})$. The <Finite-field Bogolyubov lemma> finds a subspace of codimension at most $\lceil32C^{24}\rceil$ in its fourfold sumset.

After <lifting a subspace through a Freiman model>, obtain $\widetilde W\subseteq4B$ with $|\widetilde W|\ge2^{-\lceil32C^{24}\rceil}|B|$. The set $B+\widetilde W\subseteq5B$ uses at most $C^5 2^{\lceil32C^{24}\rceil}$ cosets. Their representatives generate a quotient group of size at most two to this number. Since $|\widetilde W|\le C^4|B|$, adjoining those representatives and $a$ proves the displayed bound. Its constants are deliberately coarse, but depend only on $C$. The nonempty assumption is necessary: no vector subspace has cardinality at most a constant times the size of the empty set.