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

Let $n \ge 1$ and let $d_0; d_1, \dots, d_n$ be positive integers. Let $l$ be the total number of decimal digits of $d_0, d_1, \dots, d_n$, let $\delta$ be an integer with $\delta > 4\big(d_0 \sum_j d_j\big)^2 n^3$, and let $\varepsilon$ be a rational number with

Then

Since $f_5 = f_4 - \varepsilon$ on $P$, this says that when $f_4$ is positive on all of $P$, its minimum over $P$ is at least $\varepsilon$: the explicit, polynomially-sized precision is enough to turn the non-strict question into a strict one.

Formalization Note The bound $\varepsilon < 2^{-nl^2}$ is written multiplicatively, $\varepsilon \cdot 2^{n l^2} < 1$, in $\mathbb Q$. The hypothesis $n \ge 1$ is the paper's tacit assumption; at $n = 0$ both $f_4$ and $f_5$ vanish on $P = \{(0,0)\}$ in Lean, and the statement would be false.