[proofplan]
This entry is an outline-level record of the Green-Tao-Ziegler inverse theorem for finite-interval Gowers norms, not an independent proof of that deep theorem. The proof fixes the finite-interval $U^s([N])$ convention, states the precise external Green-Tao-Ziegler input with its nilsequence-complexity convention, and checks that the hypotheses of the present statement are exactly the hypotheses of that input. The conclusion then follows by translating the theorem's $(s-1)$-step nilsequence output into the displayed correlation estimate.
[/proofplan]
[step:Fix the finite-interval Gowers norm convention]
Let $[N] := \{1,\dots,N\}$. For $s \ge 2$ and $N \in \mathbb N$, define the parallelepiped index set
\begin{align*}
\mathcal P_s(N) := \{(n,h_1,\dots,h_s) \in \mathbb Z^{s+1} : n + \omega_1 h_1 + \cdots + \omega_s h_s \in [N] \text{ for every } \omega \in \{0,1\}^s\}.
\end{align*}
For each $\omega \in \{0,1\}^s$, define $|\omega| := \omega_1 + \cdots + \omega_s$, and define the map $\kappa_\omega: \mathbb C \to \mathbb C$ by $\kappa_\omega(z) = z$ when $|\omega|$ is even and $\kappa_\omega(z) = \overline z$ when $|\omega|$ is odd. The normalized finite-interval Gowers norm used here is
\begin{align*}
\|f\|_{U^s([N])}^{2^s}
:= \frac{1}{|\mathcal P_s(N)|}
\sum_{(n,h_1,\dots,h_s) \in \mathcal P_s(N)}
\prod_{\omega \in \{0,1\}^s}
\kappa_\omega\bigl(f(n + \omega_1h_1 + \cdots + \omega_s h_s)\bigr),
\end{align*}
for every function $f: [N] \to \mathbb C$ for which the right-hand side is defined. Fix $\delta > 0$, $N \in \mathbb N$, and a function
\begin{align*}
f: [N] &\to \mathbb C
\end{align*}
such that $|f(n)| \le 1$ for every $n \in [N]$ and $\|f\|_{U^s([N])} \ge \delta$. These are the boundedness and lower Gowers-norm hypotheses that will be supplied to the Green-Tao-Ziegler theorem under this normalization.
[/step]
[step:Apply the external Green-Tao-Ziegler theorem with matching conventions]
We use the Green-Tao-Ziegler inverse theorem for the $U^{s}([N])$ norm, in the finite-interval normalization fixed above. In the notation of Green-Tao-Ziegler, an $(s-1)$-step nilsequence of complexity at most $M$ is a function
\begin{align*}
\psi: [N] &\to \mathbb C \\
n &\mapsto F(g^n x)
\end{align*}
where $G/\Gamma$ is a filtered nilmanifold of degree at most $s-1$, $g \in G$, $x \in G/\Gamma$, and $F: G/\Gamma \to \mathbb C$ is a Lipschitz function; the dimension, filtration data, rationality constants, and Lipschitz norm are all bounded by $M$ in the Green-Tao-Ziegler complexity convention.
The external theorem states that, for each $s \ge 2$ and $\delta > 0$, there exist constants $C = C(s,\delta) > 0$ and $c = c(s,\delta) > 0$ such that every function $f: [N] \to \mathbb C$ with $|f(n)| \le 1$ for all $n \in [N]$ and $\|f\|_{U^s([N])} \ge \delta$ admits an $(s-1)$-step nilsequence
\begin{align*}
\psi: [N] &\to \mathbb C
\end{align*}
of complexity at most $C$, satisfying $\|\psi\|_\infty \le 1$, for which
\begin{align*}
\left|\frac{1}{N}\sum_{n=1}^{N} f(n)\overline{\psi(n)}\right| \ge c.
\end{align*}
The function fixed in the preceding step satisfies precisely these two hypotheses, so the theorem applies with the same parameters $s$ and $\delta$.
[/step]
[step:Translate the nilsequence output into the stated structured correlation]
The function $\psi: [N] \to \mathbb C$ obtained from the Green-Tao-Ziegler theorem is an $(s-1)$-step nilsequence, hence it is a structured object of degree less than $s$ under the nilsequence hierarchy fixed in the preceding step. The estimate
\begin{align*}
\left|\frac{1}{N}\sum_{n=1}^{N} f(n)\overline{\psi(n)}\right| \ge c(s,\delta)
\end{align*}
is the asserted correlation lower bound. The complexity bound $C(s,\delta)$ and the correlation bound $c(s,\delta)$ depend only on $s$ and $\delta$ because those are the only parameters in the external Green-Tao-Ziegler theorem; they do not depend on $N$ or on the particular function $f$. This completes the outline-level derivation from the Green-Tao-Ziegler inverse theorem.
[/step]
