§4, proof of Theorem 4.1, p. 1722 — $\delta_{k+1}\le\delta_k\le\delta_0$ and $\|\Delta y^k\|_k\le(\delta_0)^k\|\Delta y^0\|_0$

Let $\kappa\in\mathbb R$, $\omega\ge0$, and let $(a_k)_{k\ge0}$ be nonnegative reals (the step norms $\|\Delta y^k\|_k$). Put $\delta_k:=\kappa+\frac{\omega}{2}a_k$. If $\delta_0<1$ and $a_{k+1}\le\delta_k a_k$ for every $k$, then for every $k$

This is the inductive step that turns the one-step contraction into the geometric decay of the real-time steps used for (4.3), (4.2) and (4.4).

Formalization Note. Stated for an abstract sequence. The hypothesis $\omega\ge0$ is added: for $\omega<0$ the abstract statement is false, while in Theorem 4.1 a negative $\omega$ makes (4.1b) unsatisfiable on any domain with two points. The paper's intermediate product bound $\|\Delta y^k\|_k\le\delta_{k-1}\cdots\delta_0\|\Delta y^0\|_0$ is not stated separately.