Proof of Theorem 1, p. 125 — Problems 7 and 8 are equivalent

Let $n \ge 1$, let $d_0; d_1, \dots, d_n$ be positive integers and $\delta$ an integer with $\delta > 4\big(d_0 \sum_j d_j\big)^2 n^3$. Then

On $P$ the constant and linear terms of $f_2$ are rewritten using $\sum_j (y_j + s_j) = n$, which turns $f_2$ into the quadratic form $f_4$; this makes the problem a question about a homogeneous quadratic on the simplex-like set $P$.

Formalization Note The hypothesis $n \ge 1$ is the paper's tacit assumption. At $n = 0$ the statement is false in Lean: $P = \{(0,0)\}$, $f_2 = d_0^2 > 0$ there, while $f_4 = 0$ because every sum is empty and $a/0 = 0$.