Length nine: the exact optimum 10 · 2 · 846

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)

This is the proved global minimum over all five-row length-9 codebooks.

The attaining construction

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, with only two correlations reaching 10. The site verifier recomputes every correlation in exact Gaussian integers, establishing the upper bound.

Lower-bound search

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 — leaving 4⁸ = 65,536 candidate rows. A codebook keeps every scored q at or below a threshold B if and only if five candidate rows form a clique in the graph joining pairs of rows whose seventeen cross-correlations are all at most B. This reduces the feasibility check to a weighted five-clique search on a 65,536-vertex graph.

Three exhaustive searches rule out all lexicographically smaller triples:

• 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 search runs — the first is run twice, once without the strongest symmetry reduction — return INFEASIBLE after 5.8 billion pair checks in total. Each pruning step bounds the remaining contribution of the unchosen rows from below, so no feasible codebook is discarded.

Verification scope

This is a reproducible computer-assisted proof rather than an LRAT or VeriPB certificate or a formal proof-assistant development. Because the two weighted searches share one JavaScript core, rerunning them checks determinism and integrity rather than providing an independent second implementation.

The scoring is verified independently: both the proof bundle's exact scorer and the site verifier evaluate the construction above to the same 210 correlations, the same histogram, and the score 10 · 2 · 846.