A bijection is a Freiman s-isomorphism when, for every ,
holds if and only if
Because is finite, choose with and an integer . Define
An equality of -term sums in plainly gives equality after applying this linear map. Conversely, equality of the images gives
where . Therefore , and then . The same estimate with one term on each side shows that is injective on . Hence is a Freiman s-isomorphism from to the subset .
Consider the graph
The hypothesis says exactly that has at least additive quadruples. By the Balog-Szemerédi-Gowers theorem, it contains with and .
Part b gives a Freiman s-isomorphism from to a set , where it is enough to take any fixed . The set has bounded doubling, with a bound depending only on . Part c therefore provides a proper generalized arithmetic progression of rank such that
Write as a proper parameter box. Since , one of its side lengths tends to infinity with . Averaging over all lines parallel to that side gives a line on which has density bounded below in terms of . The Szemerédi theorem quoted in the question then gives, once is sufficiently large in terms of and , a nonconstant -term arithmetic progression in .
The inverse Freiman isomorphism sends it to a -term arithmetic progression in , because each relation between three consecutive terms is an additive-quadruple relation. Write this progression as
Its first-coordinate difference cannot be zero: the graph of a function has only one point above each . Hence . On the nonconstant progression
we have
Taking and , both in , proves the claim.