Clunie [Cl67] proved that there exists an infinite sequence $\{z_\nu\}$ on the unit circle with $A_\nu \le \nu$ for all $\nu \ge 1$. Translating $z_\nu = e(x_\nu)$, the natural domain of $x_\nu$ is the half-open unit interval $\mathrm{Ico}\,0\,1$, matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including $z = 1$, i.e. $x = 0$).

Linear upper bound (tight via Clunie phase tracking). Tighter than linear_upper_bound_weak: there exists a sequence $x \in (0,1)$ with $A_k \le k + 1$ for all $k \ge 1$, via the (shifted) van der Corput sequence. Whether the $+1$ can be eliminated to recover Clunie's exact $A_k \le k$ under the strict $\mathrm{Ioo}\,0\,1$ hypothesis is open in this formalization (see linear_upper_bound).