P61 five complex lines in three dimensions: the optimum is proved

0. Setting

An answer is five nonzero vectors z₁, …, z₅ in ℂ³ whose real and imaginary parts are decimals in [−1, 1]. The squared coherence μ² = max_{i<j} |⟨zᵢ, zⱼ⟩|²/(|zᵢ|²|zⱼ|²) is rational and computed exactly; the score is the integer ⌈10¹⁸·μ²⌉, smaller is better, and the page shows μ rounded up at the ninth decimal. Global phases, nonzero complex rescaling of each vector and a common unitary map leave μ unchanged, so an answer is five points of the complex projective plane ℂP², that is, five complex lines.

Let μ* be the continuous minimum (it exists: the fivefold product of unit spheres is compact). Put m₀ = (√13 − 1)/6 ≈ 0.434258546 and q₀ = m₀² = (7 − √13)/18. m₀ is the positive root of 3m² + m − 1, so for m ≥ 0, m < m₀ is equivalent to 3m² + m < 1; q₀ is the smaller root of 9q² − 7q + 1.

Let 𝒦 be the set of 5×5 Hermitian matrices with zero diagonal and off-diagonal entries |Sᵢⱼ| ≤ 1; it is compact and convex. Order eigenvalues as λ₁ ≥ λ₂ ≥ … ≥ λ₅ and put M = max_{S∈𝒦} λ₂(S).

1. The upper bound: the canonical code

Take e₁, e₂ and vⱼ = (√q₀ ωʲ, √q₀ ω⁻ʲ, √(1 − 2q₀)) for j = 0, 1, 2. Each vⱼ is a unit vector (q₀ + q₀ + 1 − 2q₀ = 1). The overlaps are:

• ⟨e₁, e₂⟩ = 0: one orthogonal pair.
• |⟨e₁, vⱼ⟩|² = |⟨e₂, vⱼ⟩|² = q₀: six pairs.
• For j ≠ k, ⟨vⱼ, vₖ⟩ = q₀(ω^{j−k} + ω^{k−j}) + 1 − 2q₀ = 1 − 3q₀, since ωᵃ + ω⁻ᵃ = −1 for a ≢ 0 (mod 3). Here 1 − 3q₀ = (√13 − 1)/6 = m₀ > 0 and (1 − 3q₀)² − q₀ = 9q₀² − 7q₀ + 1 = 0, so these three squared overlaps are q₀ as well.

So the code has one orthogonal pair and nine squared overlaps equal to q₀: μ = m₀, hence μ* ≤ m₀. It has two symmetries: the diagonal unitary diag(ω, ω⁻¹, 1) cycles v₀, v₁, v₂, and coordinate conjugation fixes e₁, e₂, v₀ and swaps v₁ and v₂. The construction and its status as conjecturally optimal come from the Game of Sloanes archive of Jasper, King and Mixon.

Decimal coordinates give rational squared overlaps while q₀ is irrational, so no site answer reaches μ = m₀ exactly; this is why the integer score needs its own corollary (§8).

2. Spectral and contact reduction

This section assumes no symmetry; it uses only compactness, the min-max principle and finite-dimensional convex separation.

Lemma 2.1 (M > 2). Let C be the real symmetric matrix with Cᵢⱼ = +1 when i − j ≡ ±1 (mod 5) and −1 on the other off-diagonal entries (+1 on the edges of the pentagon, −1 on its diagonals). Its characteristic polynomial is x(x² − 5)², so C ∈ 𝒦 has λ₂(C) = √5 and M ≥ √5 > 2.

Lemma 2.2 (no rank-one support). Let S ∈ 𝒦 and a unit vector v satisfy Sv = λv with λ > 2, and suppose S maximises the linear functional T ↦ v*Tv over 𝒦. Then λ is a simple top eigenvalue of S.

Proof. v*Tv = Σ_{i≠j} conj(vᵢ) Tᵢⱼ vⱼ, and each entry is maximised independently over its disk, so Sᵢⱼ = vᵢ conj(vⱼ)/(|vᵢ||vⱼ|) whenever vᵢvⱼ ≠ 0 (phase alignment). Then (Sv)ᵢ = λvᵢ gives λ|vᵢ| = Σ_{j≠i}|vⱼ|, i.e. (λ + 1)|vᵢ| = Σⱼ|vⱼ|: all moduli on the support are equal and λ = k − 1, where k is the support size. λ > 2 leaves k = 4 or 5. If k = 5, S is diagonal-unitarily similar to J₅ − I₅, with spectrum 4, −1, −1, −1, −1, and λ = 4 is simple. If k = 4, after rephasing the support block is J₄ − I₄ and the fifth coordinate is coupled by some b ∈ ℂ⁴ with |b|² ≤ 4; the fifth row of the eigen-equation makes b orthogonal to the constant vector. On the orthogonal complement of v, S acts as [−I₃, b; b*, 0], whose eigenvalues are −1 or roots of λ² + λ − |b|² = 0, all at most (−1 + √17)/2 < 3. So λ = 3 is simple. ∎

Proposition 2.3 (double top eigenvalue). Every maximiser S of λ₂ on 𝒦 has λ₁(S) = λ₂(S) = M > λ₃(S).

Proof. Suppose λ₁(S) > M. Take a unit M-eigenvector v and a unit top eigenvector w orthogonal to it. If some T ∈ 𝒦 had v*Tv > M, put Sₜ = (1 − t)S + tT ∈ 𝒦. The compression of Sₜ − MI to the basis (w, v) is [[γ + ta, tb], [t·conj(b), tc]] with γ = λ₁ − M > 0 and c = v*Tv − M > 0. For small t > 0 its first diagonal entry is positive and its determinant tγc + t²(ac − |b|²) is positive, so it is positive definite and Courant–Fischer gives λ₂(Sₜ) > M, a contradiction. Hence S maximises v*Tv over 𝒦, and Lemma 2.2 makes M a simple top eigenvalue, contradicting λ₁ > M. So λ₁ = λ₂ = M. If λ₃ were also M: tr S = 0 forces λ₄ + λ₅ ≤ −3M, while tr S² = Σ|Sᵢⱼ|² ≤ 20, and Cauchy–Schwarz gives 20 ≥ 3M² + (3M)²/2 = 15M²/2 ≥ 75/2, a contradiction. ∎

Proposition 2.4 (μ* = 1/M). For any five unit vectors the Gram matrix G is positive semidefinite with unit diagonal and rank at most 3, and the coherence μ is positive (ℂ³ has no five pairwise orthogonal lines). S = (I − G)/μ lies in 𝒦, and G has at least two zero eigenvalues, so the top eigenvalue 1/μ of S has multiplicity at least two and M ≥ λ₂(S) = 1/μ. Conversely, for a maximiser S, Proposition 2.3 makes G = I − S/M positive semidefinite with unit diagonal and rank exactly 3: the Gram matrix of five unit vectors in ℂ³ with coherence at most 1/M. So μ* = 1/M, and every globally minimising Gram matrix G gives a maximiser S = M(I − G). By Lemma 2.1, μ* ≤ 1/√5 < 1/2.

Proposition 2.5 (rank-two support and matching). Let G be a globally minimising Gram matrix and S = M(I − G). There is a rank-two positive semidefinite Y = ZZ*, with Z of size 5×2, such that SZ = MZ; the five rows zᵢ ∈ ℂ² of Z are nonzero and pairwise linearly independent; S maximises tr(YT) over 𝒦; Sᵢⱼ = Yᵢⱼ/|Yᵢⱼ| whenever Yᵢⱼ ≠ 0, hence |Gᵢⱼ| = μ* there; and the off-diagonal zeros of Y form a matching.

Proof. Let U be 5×2 with orthonormal columns spanning the top eigenspace. The compact convex set {U*(T − S)U : T ∈ 𝒦} contains 0 and no positive definite matrix (otherwise the compression of T to range U exceeds MI and λ₂(T) > M). Finite-dimensional separation gives a nonzero 2×2 W with tr(W U*(T − S)U) ≤ 0 for all T ∈ 𝒦; testing against all positive multiples of positive definite matrices gives W ⪰ 0, and since 0 lies in the first set the separating constant is 0; normalise tr W = 1. Put Y = UWU*; then tr(YT) ≤ tr(YS). If W had rank one, Y = vv* for an M-eigenvector v, S would maximise v*Tv, and Lemma 2.2 would make M simple, contradicting Proposition 2.3. So W is positive definite, Y has rank 2 and range ker G. Put Z = UW^{1/2}.

tr(YT) = Σ_{i≠j} Yᵢⱼ conj(Tᵢⱼ), with each entry maximised independently over its disk, so Yᵢⱼ ≠ 0 forces Sᵢⱼ = Yᵢⱼ/|Yᵢⱼ|, |Sᵢⱼ| = 1 and |Gᵢⱼ| = 1/M = μ*. Any three code vectors are linearly independent: their 3×3 principal Gram block has unit diagonal and off-diagonal moduli at most μ* < 1/2, so its smallest eigenvalue is at least 1 − 2μ* > 0. If two rows zᵢ, zⱼ of Z were dependent, some c ≠ 0 would have (Zc)ᵢ = (Zc)ⱼ = 0, and Zc ≠ 0 would be a vector of ker G supported on the other three labels, contradicting that independence. Finally, a nonzero zᵢ ∈ ℂ² has a one-dimensional orthogonal complement, so it cannot be orthogonal to two non-collinear rows: the off-diagonal zeros of Y form a matching. ∎

So a globally optimal code has at most two pairs, and disjoint ones, with overlap below μ*; every other pair attains μ*.

3. The phase certificate (P)

Theorem 3.1 (P). Every 5×5 Hermitian matrix S with zero diagonal and all off-diagonal entries of modulus 1 has λ₂(S) < 23/10.

3.1 The inertia criterion. Let s = 23/10 and H = sI − S. λ₂(S) < s is equivalent to H having at least four positive eigenvalues. Every principal minor of H of order at most 3 is positive: order one gives s, order two s² − 1 = 429/100, and order three s³ − 3s − 2Re(z) with |z| = 1 (z the product of the three edge phases, one conjugated), at least s³ − 3s − 2 = 3267/1000. By Sylvester every principal block of order ≤ 3 is positive definite, and by interlacing H has at least three positive eigenvalues. Let d = det H and let e₄ be the sum of the five principal 4-minors of H.

• (a) If d < 0: H is nonsingular with an odd number of negative eigenvalues, and at most two eigenvalues are non-positive, so exactly one is negative and four are positive.
• (b) If e₄ > 0: some principal 4-minor is positive; that 4×4 block has positive leading minors of orders 1 to 3 (true for every principal block, as above), so by Sylvester it is positive definite and by interlacing H has at least four positive eigenvalues.

In (b) it matters that every small principal block is positive definite; knowing only that H has three positive eigenvalues would not suffice. Conversely, if H has four positive eigenvalues, the fifth is either negative ((a) holds) or nonnegative (e₄ > 0). So the two strict sign tests together are exactly equivalent to (P).

3.2 Gauge and phase domain. Label the indices 0, …, 4. A diagonal unitary similarity preserves the spectrum and makes the first row S₀ⱼ = 1 (j = 1, …, 4). Write the other six edges (1,2), (1,3), (1,4), (2,3), (2,4), (3,4) as zₖ = εₖ(1 − tₖ² + 2itₖ)/(1 + tₖ²) with εₖ = ±1 and tₖ ∈ [−1, 1]: as tₖ runs over [−1, 1], (1 − t² + 2it)/(1 + t²) = e^{iθ} with θ = 2 arctan t covering [−π/2, π/2], and the sign ±1 covers the rest of the circle. This gives 64 sign patterns, each with the closed box [−1, 1]⁶.

Two symmetries shrink the domain. (i) Relabelling 1, …, 4 (a permutation similarity fixing 0) preserves the spectrum and permutes the edges; when an edge reverses orientation its entry is conjugated, i.e. t → −t with the sign unchanged, so the box still maps onto [−1, 1]⁶. Hence the 64 sign patterns fall into 11 orbits under S₄ (the 11 graphs on 4 vertices), and one representative per orbit suffices. (ii) S → conj(S) preserves the spectrum and sends every tₖ to −tₖ with the signs unchanged, so we may take t₁ ≥ 0. Each root box is therefore [0, 1] × [−1, 1]⁵, eleven in all.

3.3 Integer multiquadratic numerators. Let D(t) = Πₖ(1 + tₖ²) > 0 and define P_det(t) = 10⁵·D(t)·det H and P_e4(t) = 10⁴·D(t)·e₄(H). Expand by permutations: each edge occurs 0, 1 or 2 times in a permutation, and twice only as a transposition, contributing zₖ·conj(zₖ) = 1. So after multiplying by D(t) every tₖ has degree at most 2, the coefficients are integers, and each polynomial has 3⁶ = 729 coefficients (exponent index Σₖ eₖ3ᵏ); all imaginary parts cancel. Eleven roots give 22 polynomials.

3.4 Tensor Bernstein enclosure. On an interval [l, h] the three Bernstein coefficients of a + bt + ct² are a + bl + cl², a + b(l + h)/2 + clh and a + bh + ch². The tensor product over six coordinates gives 729 coefficients; the Bernstein basis is nonnegative and sums to 1 on the closed box, so the polynomial lies between its smallest and largest coefficient on the whole box. If every coefficient of P_det is negative, d < 0 on the whole box; if every coefficient of P_e4 is positive, e₄ > 0 on the whole box. Splitting at the midpoint, the one-dimensional coefficients (A, B, C) give the children (with a common positive factor 4)

left: (4A, 2(A + B), A + 2B + C), right: (A + 2B + C, 2(B + C), 4C).

This is de Casteljau subdivision, in integers throughout.

3.5 The binary forest. The certificate is a one-byte preorder stream of 11 trees: a digit 0–5 splits that coordinate at its midpoint (left child first), D marks a leaf where every Bernstein coefficient of P_det is negative, and E one where every coefficient of P_e4 is positive. The two closed children of each split cover their parent, so the leaves cover the 11 root boxes. The forest has 2,008,363 nodes, 1,004,176 splits and 1,004,187 leaves (636,388 D and 367,799 E), maximum depth 41; nodes = 2 × leaves − 11, with no pending node and no bytes left over.

Each D leaf proves d < 0 on its box and each E leaf proves e₄ > 0; by 3.1 either gives λ₂(S) < 23/10. The gauge and symmetries of 3.2 bring every unimodular S into some leaf box, so (P) holds on the whole continuous phase domain, not on a finite sample. ∎

Corollary 3.2. For any globally optimal code, the matrix Y of Proposition 2.5 has an off-diagonal zero. By §1, μ* ≤ m₀, so M = 1/μ* ≥ 1/m₀ = (1 + √13)/2; and 13 > (18/5)² gives √13 > 18/5, so 1/m₀ > 23/10. If Y had no zero, every |Sᵢⱼ| = 1 and (P) would give M = λ₂(S) < 23/10, a contradiction. ∎

4. A zero dual pair forces an antiunitary involution

Proposition 4.1. If the Y of a globally optimal code has an off-diagonal zero, the code is preserved by an antiunitary involution J (antilinear, norm-preserving, J² = I); after relabelling, J either fixes all five lines (type 1⁵) or fixes three and exchanges the other two (type 1³·2).

4.1 Normalisation. Relabel so that Y₁₂ = 0. A common unitary on the two columns of Z and phases on its rows (a consistent monomial similarity of S, Y and G, which affects no conclusion) give

z₁ = r₁(1, 0), z₂ = r₂(0, 1), zⱼ = rⱼ(cⱼ, sⱼe^{iφⱼ}) (j = 3, 4, 5),

with every rᵢ, cⱼ, sⱼ strictly positive and cⱼ² + sⱼ² = 1; strict positivity comes from zⱼ being independent of both z₁ and z₂, so no zero-coordinate boundary case is dropped. Phase alignment gives S₁ⱼ = 1 and S₂ⱼ = e^{−iφⱼ}; write a = S₁₂ (unconstrained, since Y₁₂ = 0). The first two rows of SZ = MZ give

M r₁ = Σⱼ rⱼcⱼ, M r₂ = Σⱼ rⱼsⱼ, a r₂ = −Σⱼ rⱼsⱼe^{iφⱼ}, conj(a) r₁ = −Σⱼ rⱼcⱼe^{−iφⱼ}.

Hence the three real numbers αⱼ = rⱼ(r₁sⱼ − r₂cⱼ) satisfy

Σⱼ αⱼ = 0, Σⱼ αⱼ e^{iφⱼ} = 0. (A)

4.2 Three distinct azimuths. Three distinct points of the unit circle are affinely independent in the real plane (a line meets a circle at most twice), so (A) forces every αⱼ = 0. Then sⱼ/cⱼ = r₂/r₁ is constant: cⱼ = c, sⱼ = s and r₁s = r₂c. If two of the last three rows are orthogonal, c² + s²e^{i(φⱼ−φₖ)} = 0 gives c = s = 1/√2 at once (this covers a possible second edge of the matching). Otherwise all three inner products are nonzero. Project row j of SZ = MZ on the unit direction (−s, c·e^{iφⱼ}) perpendicular to zⱼ: the contributions of the first two rows cancel because r₁s = r₂c, and the right side vanishes. With δ = φₖ − φⱼ and fⱼₖ = |c² + s²e^{−iδ}| > 0, the k-term divided by rₖ is exactly

(cs/fⱼₖ)·[(c² − s²)(cos δ − 1) + i·sin δ]. (B)

Both δ are nonzero, so cos δ − 1 < 0, and rₖ, cs, fⱼₖ are positive: the real part forces c² = s². So c = s = 1/√2 and r₁ = r₂. The antiunitary map J(x, y) = (conj(y), conj(x)) on the row space exchanges z₁ and z₂ and takes zⱼ to e^{−iφⱼ}zⱼ (j = 3, 4, 5), so Y has an antiunitary monomial symmetry exchanging labels 1, 2 and fixing the other three; r₃, r₄, r₅ need not be equal.

4.3 At most two azimuths. If the three azimuths coincide, one phase on the second column makes every zᵢ real. If there are exactly two, one occurs once, at label j say, and the other two rows share azimuth φ₀. If φ₀ − φⱼ is not 0 or π (mod 2π), neither Yⱼₖ vanishes (with positive c, s, orthogonality needs opposite azimuths). Project row j on (−sⱼ, cⱼe^{iφⱼ}): the first two rows contribute real numbers, and the imaginary part of the k-term is exactly

rₖcₖsₖ·sin(φₖ − φⱼ) / |cⱼcₖ + sⱼsₖe^{−i(φₖ−φⱼ)}|, (C)

The two terms have the same nonzero sign, a contradiction; so the two azimuths are opposite. A diagonal unitary rotates the second column to azimuths 0 or π, and a phase on the axis row z₂ makes its coordinate positive real again (both permitted gauges); then all five rows are real, and Y is real and fixed by plain conjugation.

4.4 Transfer to the original code. This step is needed because zeros of Y do not determine the corresponding entries of S. Take the monomial unitary Q with Y = Q·conj(Y)·Q* (Q = I in the real case; in the case of 4.2 it exchanges 1, 2 and carries the phases of the last three rows), with Q·conj(Q) = I. Put S′ = Q·conj(S)·Q* ∈ 𝒦. Then

S′Y = Q·conj(SY)·Q* = M·Q·conj(Y)·Q* = MY, tr(YS′) = tr(conj(Y)·conj(S)) = conj(tr(YS)) = tr(YS).

The second identity says that S′ also maximises tr(YT) over 𝒦, so the phase alignment of Proposition 2.5 applies to S′ as well: at every nonzero off-diagonal entry of Y, S′ᵢⱼ = Yᵢⱼ/|Yᵢⱼ| = Sᵢⱼ. Both diagonals vanish, so D = S − S′ is supported on the zero matching of Y, and DY = 0. Each row of D has at most one possibly nonzero entry Dᵢⱼ, and (DY)ᵢⱼ = Dᵢⱼ·Yⱼⱼ with Yⱼⱼ = |zⱼ|² > 0, so D = 0: S = Q·conj(S)·Q*, and G = I − S/M satisfies G = Q·conj(G)·Q* as well.

This relation preserves every conjugated Gram product, so the antilinear map defined by Q’s label permutation and phases is well defined and norm-preserving on the span of the code vectors; the five vectors span ℂ³, so it is an antiunitary J of ℂ³, and Q·conj(Q) = I gives J² = I. Its label permutation is the identity (the real case, type 1⁵) or one transposition (the case of 4.2, type 1³·2). This is a symmetry of the original code, not of an auxiliary matrix, and it was not assumed. ∎

5. Type 1⁵: five real lines

Reduction to real vectors. If the antiunitary involution J fixes every line, take a unit vector v on a line with Jv = αv (|α| = 1) and choose β with β/conj(β) = α; then J(βv) = βv. The J-fixed vectors form a real subspace with real inner products; since v = (v + Jv)/2 + i·(v − Jv)/(2i), its complexification is all of ℂ³, and real Gram–Schmidt gives a J-fixed orthonormal basis. In that basis the five representatives are real unit vectors of ℝ³, with every overlap unchanged.

Proposition 5.1. Any five unit vectors in ℝ³ have coherence μ ≥ (5 − √17)/2 > 7/16 > m₀.

Proof. The real Gram matrix G is positive semidefinite with unit diagonal and rank at most 3, so its kernel has dimension at least 2. Let P be the real orthogonal projection onto a two-dimensional subspace of the kernel: GP = 0 and tr P = 2. Then 0 = tr(GP) = 2 + Σ_{i≠j} Gᵢⱼ Pᵢⱼ ≥ 2 − μL with L = Σ_{i≠j}|Pᵢⱼ|, so μL ≥ 2. Put Sᵢᵢ = 1 and Sᵢⱼ = sign(Pᵢⱼ) (sign(0) = +1); then L = tr(PS) − 2. In an eigenbasis of S the diagonal entries αᵢ of P lie in [0, 1] and sum to 2, so tr(PS) = Σλᵢαᵢ ≤ λ₁ + λ₂ (Ky Fan; P and S need not commute). Conjugating by diag(1, S₁₂, …, S₁₅) makes the first row of S all +1, leaving six free signs: exactly 64 matrices, whose characteristic polynomials fall into seven types:

The counts sum to 64, and the largest λ₁ + λ₂ is (9 + √17)/2. So L ≤ (9 + √17)/2 − 2 = (5 + √17)/2 and μ ≥ 2/L ≥ 4/(5 + √17) = (5 − √17)/2 ≈ 0.43845. 17 < (33/8)² gives (5 − √17)/2 > 7/16, and 13 < (29/8)² gives m₀ < 7/16. ∎

So a code of type 1⁵ has coherence strictly above m₀.

6. Type 1³·2: the three-fixed barrier

Proposition 6.1. If five distinct lines in ℂ³ are preserved by an antiunitary involution that fixes three of them and exchanges the other two, their coherence satisfies m ≥ m₀.

6.1 Reduction to a spherical elliptic cap. m > 0 (ℂ³ has no five pairwise orthogonal lines). Suppose 0 < m < m₀ and put q = m², so 3q + m < 1. Take J to be coordinate conjugation in a real orthonormal basis; the three fixed lines have real unit representatives u₁, u₂, u₃. The exchanged pair is z and conj(z); rephase z so that its real and imaginary parts are orthogonal, swap them if needed, and write z = √λ·eₓ + i√(1 − λ)·e_y with 1/2 ≤ λ ≤ 1 and orthogonal real unit vectors eₓ, e_y, completed by e_z. The pair’s own overlap is s = |⟨z, conj(z)⟩| = 2λ − 1 ≤ m. A fixed line’s squared overlap with z is λuₓ² + (1 − λ)u_y² ≤ q.

If some u had u_z = 0, the left side would be at least 1 − λ ≥ (1 − m)/2 > q; so u_z > 0 after orienting. Put a² = q/λ = 2q/(1 + s) and b² = q/(1 − λ) = 2q/(1 − s), so 0 < a ≤ b < 1. The feasible set is the positive-height elliptic cap K: (uₓ/a)² + (u_y/b)² ≤ 1 with u_z = √(1 − uₓ² − u_y²) > 0. Among the fixed lines we keep only uᵢ·uⱼ ≤ m (dropping the lower bound is a relaxation). It is enough to show that no three points of K have every pairwise dot product at most m.

3q + m < 1 gives b² ≤ 2q/(1 − m) < 2/3, so every point of K has height u_z ≥ √(1 − b²) > 1/√3, and for any triple 3 + 2Σ_{i<j} uᵢ·uⱼ = |Σuᵢ|² > 3: the largest dot product is positive. Minimise the largest of the three dot products over the compact K³ and call the minimum t; a feasible triple gives 0 < t ≤ m < 1, so the minimising points are distinct. Call a pair active if its dot product equals t.

6.2 The local-minimum lemma. Fix v ∈ K. For u in the interior of K, the only stationary points of u·v on the sphere are ±v: −v has negative height and lies outside the cap, and v is a strict maximum. So the relevant local minima lie on the elliptic boundary. Assume a < b. Every local minimum of u·v on K × K with u ≠ v is the global wide-axis diameter pair (0, b, √(1 − b²)), (0, −b, √(1 − b²)). Reason: both points are on the boundary; with R = diag(λ, 1 − λ, 0), the Lagrange conditions give v = (αI + βR)u and u = (α′I + β′R)v (the constraint gradients are independent since u_z, v_z > 0 and Ru, Rv ≠ 0). If all coordinates of u are nonzero, so are those of v, and (α + βr)(α′ + β′r) = 1 holds at the three distinct eigenvalues r of R; the quadratic is identically 1, forcing β = β′ = 0 and u ∥ v, impossible for distinct points of positive height. If a coordinate vanishes, the stationarity equations make the same coordinate of the other point vanish (z never does): zero x gives the wide-axis pair; zero y gives the short-axis endpoints, and moving them to opposite nearby boundary angles lowers their dot product 1 − 2(a²cos²θ + b²sin²θ), so they are not a local minimum. The wide-axis pair is a global minimum because every point has height at least √(1 − b²), so K lies in the spherical cap of that angular radius, whose diameter is this pair. In the circular case a = b every local two-point minimum is an antipodal boundary pair, again a global diameter.

Hence an optimal triple cannot have exactly one active pair: the inactive pairs have strict slack, so the active pair would be a local minimum of the dot product on K × K, hence a global one, and then the two inactive pairs would be strictly smaller still, a contradiction.

6.3 Three active pairs. The real Gram matrix has unit diagonal and constant off-diagonal t ≥ 0, so its smallest eigenvalue is 1 − t. F = Σuᵢuᵢᵀ has the same nonzero eigenvalues, and R is positive semidefinite with trace 1, so 3q ≥ Σuᵢᵀ R uᵢ = tr(RF) ≥ 1 − t ≥ 1 − m, contradicting 3q + m < 1.

6.4 Exactly two active pairs: the centre is a short-axis endpoint. The two active pairs share a centre v; call the other points u and w, with u·w < t. Both u and w must be local minima of h_v(x) = v·x on K: otherwise a small move of one reduces its active product while keeping the slack of u·w, giving an optimal triple with one active pair, already excluded. So they are two distinct local minima of h_v with equal value.

Equal-minima lemma (a < b). Put C = 1 − b² > 0 and k = b² − a² > 0 and write boundary points with x ∈ [−a, a] as (x, ±b√(1 − x²/a²), √(C + kx²/a²)). If v_y ≠ 0, on the half where y has the sign opposite to v_y the objective is f₋(x) = vₓx − |v_y|b√(1 − x²/a²) + v_z√(C + kx²/a²), strictly convex with exactly one interior minimum. On the other half f₊ has a plus sign instead, and a²f₊″ = −|v_y|b/(1 − r²)^{3/2} + v_z kC/(C + kr²)^{3/2} with r = x/a; the ratio of the second term to the first is a constant times ((1 − r²)/(C + kr²))^{3/2}, strictly decreasing in |r|, so f₊″ is positive only on one central interval, f₊ has at most one local minimum, and its value is strictly above the minimum of f₋ (f₊ > f₋ in the interior). At x = ±a, moving into the favourable half decreases the objective to first order, so these are not local minima. Hence v_y ≠ 0 admits no two equal local minima, and v_y = 0.

With v_y = 0 both halves carry the same strictly convex g(x) = vₓx + v_z√(C + kx²/a²), so two distinct minima must be the reflected pair (x*, ±Y, Z) at the unique interior minimiser x*. Reflect so that vₓ ≥ 0; if vₓ > 0 then g′(0) = vₓ > 0 gives x* < 0, and if vₓ = 0 then x* = 0. The centre lies on the short meridian (c, 0, √(1 − c²)) with 0 ≤ c ≤ a. If c < a, increase c slightly with the leaves fixed: both active products c·x* + √(1 − c²)·Z strictly decrease (to second order when c = x* = 0) while u·w keeps its slack, lowering the objective, a contradiction. So v is the short-axis endpoint (a, 0, √(1 − a²)). In the circular case a = b, h_v has a unique boundary minimum unless v is the north pole, where every boundary value is √(1 − a²) > m, so this case is impossible too.

6.5 The exact short-axis bound. Take v = (a, 0, √(1 − a²)). Its boundary objective at abscissa x = −ap (0 ≤ p ≤ 1) is

D(p) = −a²p + √(1 − a²)·√(C + kp²).

Two distinct leaves need an interior minimum 0 < p* < 1. D′(0) = −a² < 0 and D′(1) = k − a² = b² − 2a², so b² > 2a² is needed, that is s > 1/3; the case can occur only for 1/3 < s ≤ m. Solving D′(p*) = 0 gives

t² = D(p*)² = (1 − b²)(1 − a²b²/(b² − a²)) = (1 − 2q/(1 − s))(1 − q/s) = H(s).

(Here q < 1/3 < s and b² < 2/3, so every root and denominator is positive.) H′(s) has the sign of B(s) = 1 − 2s − s² − 2q + 4qs; precisely, H′(s)·s²(1 − s)²/q = B(s). On [1/3, m], B′(s) = −2 − 2s + 4q < 0, so H can only rise and then fall, and its minimum is at an endpoint: H(1/3) = (1 − 3q)² and H(m) = 1 − m − 2q. (1 − 3q)² > q is 9q² − 7q + 1 > 0, true since q < q₀; 1 − m − 2q > q is 3q + m < 1. So t² > q = m², contradicting t ≤ m. Every active-pair case is excluded, and m ≥ m₀. ∎

The canonical code belongs to this class (conjugation fixes e₁, e₂, v₀ and swaps v₁, v₂), so the bound m₀ is attained within the class.

7. Type 1·2²: dependency C

§4 produces only types 1⁵ and 1³·2, so this section is not on the path to the value or the integer score. The package includes it to complete its full symmetry theorem (every code with a nonscalar unitary symmetry or any antiunitary symmetry has μ ≥ m₀); we report it faithfully and say how far we checked it.

Reduction of a general antiunitary T: T² is a unitary preserving the code; if it is nonscalar, branch A (unitary symmetry) applies; if T² = λI, T(T²) = (T²)T makes λ real, ±1, and writing T = UK (K coordinate conjugation) gives det(T²) = |det U|² = 1 while det(λI) = λ³, excluding λ = −1. So T is an involution, of permutation type 1⁵, 1³·2 or 1·2².

Type 1·2²: a fixed real unit vector u and exchanged pairs z, conj(z) and w, conj(w). Put A = xxᵀ + yyᵀ for z = x + iy, and B likewise: real positive semidefinite, trace 1, rank at most 2. At threshold m, feasibility becomes: A and B have spectrum (h, l, 0) with h = (1 + m)/2, l = (1 − m)/2, uᵀAu ≤ q, uᵀBu ≤ q, and root fidelity F(A, B)² ≤ q. (This step uses two prerequisites: joint concavity of fidelity, and that every extreme point of the capped trace set has spectrum (h, l, 0), so both within-pair overlaps can be saturated together.) Parametrise A = a₁eeᵀ + b₁(evᵀ + veᵀ) + c₁vvᵀ and B likewise, with aᵢ ∈ [l, h], bᵢ = √(aᵢ(1 − aᵢ) − p), p = hl and d = vᵀw ∈ [−1, 1]; then

t = tr(AB) = a₁a₂ + c₁c₂d² + 2b₁b₂d, F² = t + 2p|d|, e₂(M) = p + θ(1 − θ)(1 − 2p − t), det M = pθ(1 − θ)(1 − d²)[θc₂ + (1 − θ)c₁],

where M = θA + (1 − θ)B. If both e₂ and det of N = M − qI are positive (tr N = 1 − 3q > 0), N is positive definite, contradicting uᵀMu ≤ q. At m = 4343/10000 (3m² + m − 1 > 0, so m > m₀), a rational interval bisection of [l, h]² × [−1, 1] closes every leaf by a₁ > a₂ (symmetry), a lower bound on F² above q, or a listed θ making both lower bounds of e₂(N) and det N positive. The certificate has 10,794 leaves, so a code of type 1·2² has coherence above 0.4343 > m₀.

8. Conclusion and the integer corollary

Take any global minimiser (it exists, §0); its coherence is μ*. By §1, μ* ≤ m₀. Proposition 2.5 gives a support matrix Y; Corollary 3.2 gives it an off-diagonal zero; Proposition 4.1 gives the code an antiunitary involution of type 1⁵ or 1³·2. Type 1⁵ has μ* > m₀ by Proposition 5.1, contradicting μ* ≤ m₀; so the type is 1³·2, and Proposition 6.1 gives μ* ≥ m₀. Hence μ* = m₀: every five lines in ℂ³ have μ ≥ (√13 − 1)/6 and μ² ≥ (7 − √13)/18, with equality for the canonical code. Nowhere is a symmetry, orbit, coordinate form or contact pattern assumed for the optimum; the symmetry is derived from optimality.

Integer corollary. Every legal answer is five nonzero vectors, so μ² ≥ q₀ and the score ⌈10¹⁸μ²⌉ ≥ ⌈10¹⁸q₀⌉. Put K = 188580484696445040. q₀ = 0.188580484696445039271…, and exactly (K − 1)/10¹⁸ < q₀ < K/10¹⁸: for rational x, q₀ < x is equivalent to 7 − 18x < 0 or (7 − 18x)² < 13, an integer comparison. So every answer scores at least K. The current record’s nine-decimal answer has largest squared overlap exactly 6279168879955444015132457236080625 / 33297023761832624111414575863183801 and scores exactly K (displayed μ = 0.434258546). Hence K is the smallest integer score, and the current record is optimal and cannot be beaten.

Our verification

We read only the package’s data files (phase_polynomials.json, all_roots.data, full.tree, answer.json, leaf_certificate.json) and decided every step with our own code, tools/p61-certificates.py and tools/p61-forest-replay.cpp. Every check passed, in about 94 seconds.

Composition. The complete composition is in the package’s top-level THEOREM.txt; the phase archive README’s “composition pending” and BERNSTEIN_CERTIFICATE_PROOF’s “no traversal” are older frozen files and are stale.

Reasoning checked by hand (every step on the path to the lower bound).

• §2 contact reduction: the top-eigenvalue multiplicity, μ* = 1/M, separation giving a rank-two Y, and the matching structure of Y’s zeros; the pentagon sign matrix’s characteristic polynomial x(x² − 5)² is checked exactly by our code.
• §3 the logic of (P): every principal minor of H = 23/10·I − S up to order 3 is positive (minimum 3267/1000), so det < 0 or e₄ > 0 each give four positive eigenvalues; 13 > (18/5)² gives 1/m₀ > 23/10.
• §4 zero-dual-pair reduction: the α-system, the three-azimuth case, projections (B) and (C), and the transfer S′ = S with D = 0. The package applies phase alignment to S′ directly; that needs S′ to maximise tr(YT) as well, which holds because tr(YS′) = tr(YS). We supplied that line; the conclusion stands.
• §5 real five lines: the characteristic polynomials of all 64 sign matrices computed exactly, 7 types with multiplicities 15, 15, 12, 10, 10, 1, 1, largest λ₁ + λ₂ = (9 + √17)/2; (5 − √17)/2 > 7/16 > m₀ compared exactly.
• §6 three-fixed barrier: the elliptic cap, the local-minimum lemma, the short-axis endpoint and H(s). The identities for H(s), B(s) and the endpoint values are verified exactly over the rationals; the closed form of D(p*)² we rederived by hand and checked numerically on random instances.

Replay of the phase certificate.

• The 22 numerator polynomials: rebuilt by exact Gaussian-rational determinants on the grid {−1, 0, 1}⁶ followed by interpolation (a different route from the package’s permutation expansion), confirmed at random rational points; the coefficients are identical to the submitted ones.
• The 11 sign roots are exactly one per S₄-orbit of the 64 edge-sign patterns; the first-row gauge, the conjugation half-box and the t-parametrisation cover the whole phase domain.
• The root-box Bernstein coefficients are computed by us and match all_roots.data up to positive factors.
• The forest is replayed by our own C++ (__int128, with every coefficient checked below 2¹²⁴ before each split, so nothing can overflow): 2,008,363 nodes, 1,004,176 splits, 1,004,187 leaves (636,388 D and 367,799 E), maximum depth 41, no bytes left over, about 37 seconds.
• Every 997th leaf, 1,007 in all, is rechecked in Python big integers by a direct Bernstein transform of the monomial polynomial on the leaf box, independent of the de Casteljau chain.
• Extra (not on the score path): all 10,794 leaves of the 1·2² branch (dependency C, m > 0.4343) pass with our own exact interval arithmetic, and the leaf volumes tile the whole box with pairwise disjoint interiors.
• Numerical sanity (not proof): local search over unimodular S found λ₂ at most about 2.2843 < 2.3, and SLSQP found best coherence 0.434258546.
• Values: q₀ and K = ⌈10¹⁸q₀⌉ compared exactly; the canonical code’s identity 9q₀² − 7q₀ + 1 = 0; answer.json scores exactly K.

To rerun: put the five data files above in a directory <dir>, then

E:/math/research/toolshim/g++.exe -O2 -std=c++17 tools/p61-forest-replay.cpp -o replay.exe
python tools/p61-certificates.py <dir> replay.exe

Not refereed.

• The equality and uniqueness classification: the three_fixed_equality module and the equality case of the unitary barrier A (the classification of codes with an orthogonal pair at μ = m₀). So the statement that the optimal configuration is unique (up to unitaries, permutations and row scalings) is not verified by us. The value and the integer score do not depend on it; attainment is checked directly: the canonical code has one orthogonal pair and nine squared overlaps equal to q₀.
• The prerequisites of dependency C: the extreme-point spectrum lemma and the fidelity reduction (the two steps in parentheses in §7). We replayed its interval certificate but did not referee these prerequisites; §7 is not on the path to this page’s conclusions.
• The lower-bound part of the unitary-symmetry branch A is likewise off the path and was not refereed.

Credit and scope

The canonical code and the conjecture that it is optimal come from the Game of Sloanes of Jasper, King and Mixon (arXiv:1907.07848 and its GitHub archive, which credits the listed numerical packing to Dustin G. Mixon). This proof shows it is optimal and settles the smallest integer score on the site. The adopted contribution earns zzzcy #308 one permanent +2 proof award.

Game of Sloanes · Jasper–King–Mixon · Open P61