# Patterson's first moment for cubic Gauss sums

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

- [An unconditional first moment for cubic Gauss sums](../../preprints/An-unconditional-first-moment-for-cubic-Gauss-sums-September-25-2026/paper.pdf)

## Scope

Patterson's first-moment conjecture concerns the average of normalized cubic Gauss sums over primary Eisenstein primes. The formalization proves the sharp-cutoff asymptotic with main term $\frac65c_*X^{5/6}/\log X$, where $c_*=(2\pi)^{2/3}/(3\Gamma(2/3))$. It also proves the corresponding angular comparison for every integer Fourier mode and cancellation of order $o(X^{5/6}/\log X)$ for each fixed nonzero mode. All primary Eisenstein primes are included, without an extra conjectural premise.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Patterson first moment and angular cancellation | [PattersonFirstMoment.lean](../ComparatorChallenges/PattersonFirstMoment.lean) |