Cyclic Bogolyubov lemma with explicit phase radius (source code)

= Cyclic Bogolyubov lemma with explicit phase radius
{title2=$B(R,1/6)\subseteq2A-2A,\quad |R|\leq4\alpha^{-2}$}

For a set of density $\alpha$ in a finite cyclic group, select frequencies whose normalized <Fourier coefficients on a finite abelian group> have magnitude at least $\alpha^{3/2}/2$. <Parseval identity> bounds their number by $4\alpha^{-2}$. <Fourier inversion> of the fourfold <convolution> shows it is positive on the <Bohr set in phase-distance convention> of radius $1/6$. This is an explicit form of the <Bogolyubov lemma>.