# The circulant Hadamard and Barker-sequence conjectures

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

- [The circulant Hadamard conjecture](../../preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf)

## Scope

The formalization proves the circulant Hadamard conjecture in exact form: a real circulant Hadamard matrix of positive order $n$ exists exactly when $n=1$ or $n=4$. Explicit witnesses are supplied for both orders, with no restriction on prime factors.

It also proves the even-length part of the Barker-sequence consequence. A positive even-length sign sequence whose nonzero aperiodic autocorrelations have absolute value at most one must have length $2$ or $4$. The paper's classification of odd Barker lengths is outside this selected additional statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Classification of circulant Hadamard orders | [CirculantHadamard.lean](../ComparatorChallenges/CirculantHadamard.lean) |
| Classification of positive even Barker lengths | [EvenBarker.lean](../ComparatorChallenges/EvenBarker.lean) |