At length nine, 10 · 2 · 846 is the end of it

What is being minimised

Five sequences of length 9 over the four phases 1, i, −1, −i are scored on 210 correlations: each row's eight nonzero autocorrelation shifts, and all seventeen shifts of each of the ten row pairs. Write q for the squared modulus of a correlation, and minimise, in order, the peak P = max q, then the number C of correlations attaining it, then the total T = Σq.

(P, C, T) = (10, 2, 846)

That is the global optimum, not the best anybody has found.

The construction that reaches it

Digits are phases: p stands for i to the power p.

000212332
020030132
022010310
002232110
010101210

Its 210 correlations, by squared modulus:

The counts sum to 210 and the energies to 846, and only two correlations reach 10. This site's own verifier recomputes all of it in exact Gaussian integers, which is what makes the upper bound checkable rather than asserted.

Why nothing is lower

Multiplying a row by a unit phase rotates every correlation it appears in without changing any modulus, so every row may be taken to start at phase 0 — which leaves 4⁸ = 65,536 candidate rows. A codebook keeps every scored q at or below a threshold B exactly when five candidate rows form a clique in the graph that joins two rows whose seventeen cross-correlations all sit at or below B. So the question becomes a weighted five-clique search, over a graph small enough to hold.

Three exhaustive searches then rule out everything lexicographically smaller, and between them they cover every case:

• no codebook keeps every scored q at 9 or below;
• with a peak of 10, no codebook attains it only once;
• with a peak of 10 attained twice, no codebook totals 845 or less.

All four searches — the first is run twice, once without the strongest symmetry reduction — return INFEASIBLE, over 5.8 billion pair checks in total. Every pruning rule they use compares against a lower bound on what the unchosen rows can still contribute, so nothing that could have satisfied the limits was ever discarded.

What kind of proof this is

A reproducible computer-assisted proof, and not more than that. It is not an LRAT or VeriPB certificate and it has not been through a proof assistant; the two weighted searches share one JavaScript core, so rerunning them checks determinism and integrity rather than providing an independent second implementation.

What is independent is the scoring. The proof bundle carries its own exact scorer, this site has its own, and both were run on the construction above: 210 correlations, the same histogram, the same 10 · 2 · 846. The searches all rest on that arithmetic, and two unrelated implementations of it agree.