OAI.GaussianMoat.fullMain

The theorem states that both of two Gaussian-moat endpoint propositions hold. The first, MainEndpoint, says that for every real step bound D there is no sequence z : ℕ → ℤ[i] of Gaussian integers such that every z(t) is irreducible (a Gaussian prime), z is injective, and consecutive terms satisfy |z(t+1) − z(t)| ≤ D in the complex plane; that is, no infinite walk through distinct Gaussian primes with steps of length at most D exists. The second, UniformEndpoint, says that for every real D there is a natural number B such that two things hold. First, in the graph whose vertices are the Gaussian primes and in which two distinct primes are adjacent when their complex distance is at most D, every connected component is finite and has at most B elements. Second, for every n and every injective list z₀, …, z_{n−1} of Gaussian primes whose consecutive entries are at distance at most D, the length n is at most B.