Cofinite Zeros of High Derivatives

We construct a nonzero transcendental entire function such that every nonempty open subset of the complex plane contains a zero of every sufficiently high derivative; equivalently, the union of the zero sets along every infinite increasing sequence of derivative orders is dense.

The construction is probabilistic and uses a bounded-coefficient Fock series.

A saddle estimate, a one-coordinate small-ball bound, and Jensen's formula give summable outer probabilities for zero-free disks.

The resulting function satisfies the explicit growth bound $|f(z)|\leq\sqrt2\exp(|z|^2)$ and therefore also supplies a counterexample to a 1973 theorem of Boas and Reddy as printed.

A machine-checked Lean 4 formalization verifies the existence theorem, the growth bound, and their supporting lemmas.