# Uniformly bounded components of Gaussian-prime graphs

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Bounded-Step Walks on Gaussian Primes](../../preprints/Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026/paper.pdf)

## Scope

The Gaussian moat problem asks whether an infinite walk through distinct Gaussian primes can have bounded step lengths. The formalized result gives a negative answer for every real step bound $D$. More strongly, one finite bound depending only on $D$ limits the size of every connected component of the bounded-step graph and the length of every injective bounded-step walk. Axis primes and all associates are included. No explicit function of $D$ is supplied.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform bounds for bounded-step Gaussian-prime walks | [GaussianMoat.lean](../ComparatorChallenges/GaussianMoat.lean) |