Lines of Gaussian integers far from every Gaussian prime

Every straight line through two distinct Gaussian integers z ≠ w contains Gaussian integers at arbitrarily large distance from every Gaussian prime: for every R there is t : ℤ such that z + t (w - z) has squared distance > R from all Gaussian primes (Gethner–Wagon–Wick, 1998); so no walk to infinity with bounded steps stays on a line. The point is built by the Chinese remainder theorem: for each offset u in the box of radius R, a prime p ≡ 1 (mod 4) larger than everything relevant splits in ℤ[i] and one of its Gaussian factors is made to divide z + t (w - z) + u, with a norm too large for that Gaussian integer to be prime.

Main results

• GaussianMoat.exists_far_from_primes_on_line: every line through two Gaussian integers has points far from all Gaussian primes
• GaussianMoat.norm_eq_of_dvd_prime: a Gaussian prime divisible by a Gaussian integer of prime norm has that norm

References

• E. Gethner, S. Wagon and B. Wick, A stroll through the Gaussian primes, Amer. Math. Monthly 105 (1998), 327–337.
• The general moat question (Gordon 1962; Erdős problem 952) is settled in OpenAI, Bounded-Step Walks on Gaussian Primes (2026), with a Lean proof in openai/math; that is a different statement and is not used here.

theorem GaussianMoat.exists_int_dvd_sub {π : GaussianInt} {p : ℕ} (hp : Nat.Prime p) (hπ : Zsqrtd.norm π = ↑p) (g : GaussianInt) : ∃ (n : ℤ), π ∣ g - ↑n

If π has prime norm p then every integer-coefficient Gaussian integer is congruent modulo π to a rational integer (ℤ → ℤ[i]/(π) is onto).

theorem GaussianMoat.norm_eq_of_dvd_prime {π g : GaussianInt} {p : ℕ} (hp : Nat.Prime p) (hπ : Zsqrtd.norm π = ↑p) (hg : Prime g) (hd : π ∣ g) : Zsqrtd.norm g = ↑p

A Gaussian prime divisible by an element of prime norm p has norm p.

theorem GaussianMoat.exists_norm_gt (a e : GaussianInt) (he : e ≠ 0) (L : ℤ) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → L < Zsqrtd.norm (a + ↑k * e)

Norm growth along an arithmetic progression of Gaussian integers.

theorem GaussianMoat.exists_modulus (z d : GaussianInt) (hd : d ≠ 0) (S : Finset GaussianInt) : ∃ (t : ℤ) (M : ℤ), 0 < M ∧ ∀ u ∈ S, ∃ (π : GaussianInt) (q : ℕ), Nat.Prime q ∧ Zsqrtd.norm π = ↑q ∧ ↑q ≤ M ∧ ∀ (k : ℤ), π ∣ z + ↑(t + k * M) * d + u

Inductive CRT construction: for every finite set S of offsets there is a progression t + k M along which, for each u ∈ S, the point z + (t + k M) d + u is divisible by a Gaussian integer of prime norm q ≤ M.

theorem GaussianMoat.exists_far_from_primes_on_line (z w : GaussianInt) (hzw : z ≠ w) (R : ℕ) : ∃ (t : ℤ), ∀ (π : GaussianInt), Prime π → ↑R < Zsqrtd.norm (z + ↑t * (w - z) - π)

Gethner–Wagon–Wick (1998). Every straight line through two distinct Gaussian integers z ≠ w contains Gaussian integers at arbitrarily large distance from every Gaussian prime: for every R there is t : ℤ such that z + t (w - z) has squared distance > R from every Gaussian prime.