# Ordinary two-point correlations and the corrected Elliott conjecture

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

- [Ordinary two-point correlations of multiplicative functions](../../preprints/Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026/final.pdf)

## Scope

The formalization proves ordinary two-point cancellation for multiplicative functions. For the Liouville function on every fixed pair of nonproportional affine forms, the correlation sum up to $X$ is $O(X/(\log X)^c)$ for an absolute $c>0$, with the implied constant depending on the forms.

For two one-bounded multiplicative functions, if at least one is uniformly nonpretentious against all Dirichlet-character twists with frequency $|t|\le N$, then their shifted and nonproportional affine correlation sums divided by $N$ tend to zero. These are ordinary averages, with no logarithmic averaging.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Ordinary Elliott cancellation under uniform nonpretentiousness | [OrdinaryElliott.lean](../ComparatorChallenges/OrdinaryElliott.lean) |
| Ordinary Liouville and multiplicative two-point correlations | [OrdinaryTwoPointCorrelations.lean](../ComparatorChallenges/OrdinaryTwoPointCorrelations.lean) |