P60 sixteen lines in five dimensions: the grid optimum is proved

0. Setting

An answer is 16 nonzero vectors v₁, …, v₁₆ ∈ ℝ⁵ whose coordinates are decimals in [−1, 1] with at most nine places. A vector stands for the line it spans; sign and scaling do not change the answer. Write

q = μ² = max over i < j of (vᵢ·vⱼ)² / ((vᵢ·vᵢ)(vⱼ·vⱼ)), K = ceil(10¹⁸ q).

K is the integer score the site records, smaller being better; the page shows √(K/10¹⁸) rounded up at the ninth decimal. q is rational, and the verifier compares it exactly by cross-multiplication, with no normalisation and no square roots.

Let uᵢ = vᵢ/|vᵢ| be the unit representative and sᵢ = vᵢ·vᵢ. Lines i and j form an equality pair if (uᵢ·uⱼ)² = 1/5. Sections 2–6 use only that the coordinates of the vᵢ are rational, so (b) holds for rational coordinates with any denominator, not just 10⁹.

1. The lower bound and configurations attaining it

For each line put Qᵢ = uᵢuᵢᵀ − I₅/5. Each Qᵢ is a traceless real symmetric 5 × 5 matrix, a space of dimension 15 − 1 = 14. Their Gram matrix H under the Frobenius inner product ⟨A, B⟩ = tr(AB) is

Hᵢᵢ = 4/5, Hᵢⱼ = tr(QᵢQⱼ) = (uᵢ·uⱼ)² − 1/5 (i ≠ j).

H is a positive semidefinite 16 × 16 matrix of rank at most 14, so dim ker H ≥ 2. Also cᵀHc = ‖Σ cᵢQᵢ‖², so Hc = 0 exactly when Σ cᵢQᵢ = 0.

Lemma 1.1 (a Perron-type kernel lemma). Let H be positive semidefinite with every off-diagonal entry ≤ 0, and let the graph with an edge wherever Hᵢⱼ < 0 be connected. If H is singular, then ker H is one-dimensional and spanned by a vector with every coordinate strictly positive.

Proof: take z ∈ ker H nonzero and let |z| be its entrywise absolute value. Since the off-diagonal entries are nonpositive, |z|ᵀH|z| ≤ zᵀHz = 0; positive semidefiniteness then gives |z|ᵀH|z| = 0 and so H|z| = 0. If a nonnegative kernel vector y has yᵢ = 0, the i-th equation Σⱼ Hᵢⱼyⱼ = 0 has only nonpositive terms, forcing yⱼ = 0 at every negative-edge neighbour j of i; by connectivity y = 0. So every coordinate of |z| is strictly positive. Fix a positive kernel vector x; for any kernel vector z let c = maxᵢ zᵢ/xᵢ. Then cx − z is a nonnegative kernel vector with a zero coordinate, hence zero, and z = cx.

Proposition 1.2 (Rankin’s bound). Every 16 lines have q ≥ 1/5. If q < 1/5, every off-diagonal entry of H is strictly negative, the graph is complete, and Lemma 1.1 allows a kernel of dimension at most 1, contradicting dim ker H ≥ 2. This is Rankin’s orthoplex bound: N > d(d + 1)/2 lines have μ² ≥ 1/d, here with d = 5 and N = 16 > 15.

An attaining configuration (6 + 10). View ℝ⁵ as the hyperplane x₁ + … + x₆ = 0 in ℝ⁶, with j = (1, …, 1). The six simplex lines uᵢ = √(6/5)(eᵢ − j/6) are unit vectors with uᵢ·uⱼ = −1/5. For each 3-subset S of {1, …, 6} let v(S) be +1/√6 on S and −1/√6 off S; S and its complement give the same line, so there are 10 lines. The coordinates of v(S) sum to 0, so uᵢ·v(S) = ±1/√5, and v(S)·v(T) = ±1/3 when T is neither S nor its complement. Every squared overlap lies in {1/25, 1/9, 1/5}, and the largest is 1/5.

Another attaining configuration (7 + 9). Take a unit vector e₀ and, in two mutually orthogonal planes orthogonal to e₀, equilateral unit triples t₁, t₂, t₃ and s₁, s₂, s₃ (pairwise inner products −1/2 within each triple). The seven lines e₀, −e₀/3 + (2√2/3)tᵢ, −e₀/3 + (2√2/3)sⱼ and the nine lines (e₀ + √2(tᵢ + sⱼ))/√5 have, by direct computation, every cross squared overlap equal to 1/5, overlaps 1/9 or 1/81 among the seven, and 4/25 or 1/25 among the nine. This proves (a). The known optimal 16-line configuration is listed in Henry Cohn’s archive of Grassmannian packings.

2. Equality structure: blocks, tight frames and odd cycles

From here to the end of Section 6, suppose v₁, …, v₁₆ are rational with q ≤ 1/5; we derive a contradiction. By Proposition 1.2, q = 1/5, so every off-diagonal entry of H is ≤ 0, and Lemma 1.1 applies to each connected component of the graph with edges Hᵢⱼ < 0. Call these components blocks.

Lemma 2.1 (no odd cycle of equality pairs). If i, j is an equality pair then sᵢsⱼ = 5(vᵢ·vⱼ)² with vᵢ·vⱼ ≠ 0. Multiply these equations around a cycle of odd length k: on the left each sᵢ appears twice, giving the square of a nonzero rational; on the right, 5ᵏ times a nonzero rational square. Then 5 would be a rational square, which it is not. In particular no three lines are pairwise equality pairs.

Lemma 2.2 (exactly two blocks). Between different blocks Hᵢⱼ = 0, so every cross-block pair is an equality pair. One line from each of three blocks would be an equality triangle, so by Lemma 2.1 there are at most two blocks. H is block diagonal, and ker H is the direct sum of the blocks’ kernels; by Lemma 1.1 each block contributes at most one dimension (a one-line block is the nonsingular 4/5). Since dim ker H ≥ 2, there are exactly two blocks, both singular, each with a strictly positive kernel vector, and rank H = 14.

Lemma 2.3 (positive tight frames). Let c > 0 be a kernel vector of a block. Then Σ cᵢQᵢ = 0, that is Σ cᵢuᵢuᵢᵀ = (Σ cᵢ/5)I₅. With wᵢ = 5cᵢ/Σ cⱼ,

Σ wᵢ uᵢuᵢᵀ = I₅, wᵢ > 0, Σ wᵢ = 5 (sum over one block).

(Σ wᵢ = 5 comes from taking traces.) So the lines of each block span ℝ⁵, and each block has at least 5 lines. No pair inside a block is an equality pair: it would form an equality triangle with any line of the other block.

Summary: two blocks A and B with |A| + |B| = 16, each a positive weighted tight frame; every cross pair has |a·b| = 1/√5 (unit representatives), and every pair inside a block has squared overlap strictly below 1/5.

3. Block sizes: excluding 5 + 11 and 6 + 10

The block sizes can only be (5, 11), (6, 10), (7, 9) or (8, 8). This section excludes the first two; 6 + 10 reduces to the regular simplex, which the arithmetic obstruction of Section 6 excludes.

3.1 A block of five lines

A positive tight frame of five lines: the 5 × 5 matrix W with columns √wᵢuᵢ has WWᵀ = I, hence WᵀW = I, that is √(wᵢwⱼ) uᵢ·uⱼ = δᵢⱼ. The five lines are an orthonormal basis with all weights 1. Every line of the other block has inner product ±1/√5 with each basis vector, so its coordinates in this basis are (±1, …, ±1)/√5. Two such lines have inner product equal to a sum of five ±1 over 5, an odd integer over 5, of absolute value 1/5, 3/5 or 1; the coherence bound leaves only 1/5.

Suppose there are N such lines. Their unit Gram matrix G has rank ≤ 5, trace N and squared off-diagonal entries 1/25. Cauchy–Schwarz on the eigenvalues of G gives (tr G)² ≤ 5 tr(G²):

N² ≤ 5(N + N(N − 1)/25) ⟹ 4N ≤ 24 ⟹ N ≤ 6.

(Exhaustive search shows the true maximum is 5.) The other block needs 11 lines, a contradiction.

3.2 A block of six lines

Let six lines satisfy Σ wᵢuᵢuᵢᵀ = I₅. The 5 × 6 matrix W with columns √wᵢuᵢ has orthonormal rows, so WᵀW = I₆ − zzᵀ with z a unit normal to the row space. Reading off the diagonal and Wz = 0:

wᵢ = 1 − zᵢ² > 0, Σ cᵢuᵢ = 0 with cᵢ = zᵢ√(1 − zᵢ²).

Flipping uᵢ (which flips the sign of zᵢ) we may take zᵢ ≥ 0, so cᵢ ≥ 0, with cᵢ = 0 exactly when zᵢ = 0. Each unit vector v of the other block gives signs εᵢ = √5 uᵢ·v ∈ {±1} with Σ cᵢεᵢ = √5 (Σ cᵢuᵢ)·v = 0; call ε balanced. The six uᵢ span ℝ⁵, so ε determines v, and −ε gives the same line. Ten lines therefore need at least 20 balanced sign vectors. Let m be the number of positive cᵢ.

m = 6. Identify ε with the subset S where it is +; balanced means the cᵢ over S sum to half the total. With every cᵢ positive, a proper subset of a balanced set has a strictly smaller sum, so the balanced sets form an antichain. Counting random maximal chains (the LYM inequality) gives Σ 1/C(6, |S|) ≤ 1; C(6, k) has the unique maximum C(6, 3) = 20, so there are at most 20, with equality only if every 3-subset is balanced. Comparing {a, b, c} with {d, b, c} shows all cᵢ are equal. Then zᵢ²(1 − zᵢ²) = c² has only the two roots t ≤ 1/2 and 1 − t. If some zᵢ² = 1 − t, either the other five equal t and 1 − t + 5t = 1 forces t = 0, or two equal 1 − t and the sum exceeds 1; both contradict zᵢ > 0 and Σ zᵢ² = 1. So zᵢ² = 1/6, wᵢ = 5/6, and the unit Gram is (6/5)(I₆ − J/6): diagonal 1, off-diagonal −1/5. These are the six central lines of the regular 5-simplex.

m = 5. The sign on the zero coordinate is free, so the balanced patterns are twice the balanced subsets of the positive coordinates, halved again by ±ε: the number of lines equals the number of balanced subsets. If a single cₐ is half the total, the only balanced subsets are {a} and its complement. Otherwise they are 2-subsets and their 3-element complements. Two balanced 2-subsets cannot be disjoint, or the fifth coefficient would be 0. Pairwise-intersecting 2-subsets form a star or a triangle, at most 4 of them on five points. So there are at most 8 balanced subsets and at most 8 lines.

m = 4. Lines = balanced subsets × 2² / 2, so ten lines need at least 5 balanced subsets. Balanced subsets are closed under complement and never equal their complement, so their number is even: at least 6. An antichain on four points has at most C(4, 2) = 6 members, with equality only if every 2-subset is balanced, which forces the four positive coefficients to be equal, and as above zᵢ² = 1/4. The block is then two axes orthogonal to everything else (zᵢ = 0, wᵢ = 1) and four regular-tetrahedron lines in the orthogonal ℝ³ (unit Gram off-diagonal −1/3). A line of the other block has components ±1/√5 on the two axes, and its ℝ³ part w has |w|² = 3/5 and inner product ±1/√5 with each tetrahedron direction; solving gives w = ±√(3/5)eⱼ for one of the three coordinate directions eⱼ aligned with the tetrahedron. Fixing the sign of the √3 term to be +, the candidates are

(ε₁, ε₂, √3 eⱼ)/√5, ε₁, ε₂ ∈ {±1}, j = 1, 2, 3.

For the same j two candidates have inner product (ε₁ε₁′ + ε₂ε₂′ + 3)/5: 3/5 when exactly one ε differs, above 1/√5, and 1/5 when both differ. So each j allows at most two lines; different j impose nothing further, and the total is at most 6, short of 10.

m = 3. With three positive coefficients a balanced subset exists only when one coefficient is the sum of the other two, and then only it and its complement: at most 2. That gives at most 2 × 2³ / 2 = 8 lines.

m ≤ 2. For m = 2, the four lines with zᵢ = 0 are orthogonal to each other and to the rest of the block (their rows of WᵀW are eᵢ) and span four dimensions; the remaining two lines lie in the one-dimensional complement and coincide, with squared overlap 1. For m = 1, zᵢ = 1 gives wᵢ = 0; m = 0 contradicts |z| = 1.

So 6 + 10 can only be the six regular-simplex lines with ten more, and Section 6 shows that has no rational coordinates. What remains is (7, 9) and (8, 8).

4. 7 + 9 and 8 + 8: the exhaustion down to six classes

Let A have p lines and B have q, with (p, q) = (7, 9) or (8, 8). Take five linearly independent unit vectors of A as the rows of U (A spans ℝ⁵); X = UUᵀ is their Gram matrix. Each unit vector b of B has Ubᵀ = ε/√5 with ε ∈ {±1}⁵. Flipping b we may take the first entry of ε to be +1, leaving 16 possible sign columns. U is invertible, so distinct B lines give distinct columns, and since B spans ℝ⁵ the q chosen columns have rank 5.

Every other line of A is a = λU for a row vector λ. The cross equality condition says λS ∈ {±1}^q, where S is the 5 × q sign matrix of the chosen columns. Take five independent columns of S as E; then λE ∈ {±1}⁵, so trying all 32 sign vectors, solving exactly for λ and checking that the whole row λS is ±1 finds every possible λ. Up to overall sign, the five basis lines give five rows, and p − 5 more are chosen from the remaining admissible rows. No numerical optimisation, sampling or heuristic pruning is involved.

Row and column permutations and sign flips only relabel lines and reverse their directions, leaving every absolute inner product unchanged. The six classes occur 480, 1,920, 400, 1,280, 1,160 and 2,160 times, 7,400 in all. Classes 0–2 are 7 + 9 and classes 3–5 are 8 + 8. The cross Gram matrix is S/√5, so the next section only has to treat the six representatives.

5. Each class has a unique metric

Fix a representative and let row λᵢ of Λ be the coefficients of the i-th A line in the basis U. The tight-frame identity Σ wᵢaᵢᵀaᵢ = I for A becomes UᵀCU = I, that is

C = X⁻¹ = Σ wᵢ λᵢᵀλᵢ, Σ wᵢ = 5, λᵢ C⁻¹ λᵢᵀ = |aᵢ|² = 1.

For each class the package gives an exact matrix C₀ = Σ wᵢ⁰ λᵢᵀλᵢ (entries in ℚ or ℚ(√5)) with C₀ positive definite, Σ wᵢ⁰ = 5 and every λᵢ C₀⁻¹ λᵢᵀ = 1. For any feasible C,

tr(C₀⁻¹C) = Σ wᵢ λᵢC₀⁻¹λᵢᵀ = Σ wᵢ = 5, tr(C⁻¹C₀) = Σ wᵢ⁰ λᵢC⁻¹λᵢᵀ = Σ wᵢ⁰ = 5.

Let μ₁, …, μ₅ > 0 be the eigenvalues of C₀^(−1/2) C C₀^(−1/2). Then Σ μₖ = 5 = Σ 1/μₖ. The AM–HM inequality (Σ μₖ)(Σ 1/μₖ) ≥ 25 holds with equality only when all μₖ are equal, so every μₖ = 1 and C = C₀. Hence X = C₀⁻¹ is determined; the A lines have Gram matrix ΛXΛᵀ and the B lines bⱼ = U⁻¹Sⱼ/√5 have Gram matrix SᵀC₀S/5. The whole 16-line Gram matrix is unique, and the configuration is unique up to an orthogonal map. Nothing here depends on a numerical optimiser.

Checking every within-block pair under the unique metric, in exact ℚ(√5) arithmetic:

Classes 0, 1, 3 and 4: the unique metric has a within-block pair at squared overlap 9/25 > 1/5, violating the bound, so not even a real configuration exists. Class 5: no within-block pair exceeds 1/5, but one pair inside A is exactly 1/5, and with any B line it forms an equality triangle, which Lemma 2.1 rules out for rational coordinates. Class 2: every within-block pair is strictly below 1/5 and every diagonal entry is 1, so it is a genuine real configuration (its weights 1/2 and 3/4 match the 7 + 9 configuration of Section 1); the arithmetic of Section 6 excludes it.

6. The rationality obstruction

Lemma 6.1. If ℚ⁵ contains five pairwise orthogonal rational vectors with squared norms (1, 2, 2, 2t, 2t), then t is a sum of two rational squares.

Proof. The rational Householder reflection I − 2wwᵀ/(wᵀw) (w = x − e₁, or the identity when x = e₁) sends a rational unit vector x to e₁ and keeps rationality and orthogonality; the other four vectors lie in the complement ℚ⁴ with squared norms (2, 2, 2t, 2t). Regard ℚ⁴ as the rational quaternions, where |pq| = |p||q|. For q of squared norm 2, left multiplication by q̄/2 is a rational linear map sending q to q̄q/2 = 1 and multiplying every inner product by 1/2, so orthogonality is kept. The squared norms become (1, 1, t, t); the first vector is the real unit 1 and the other three lie in the pure imaginary ℚ³. One more rational Householder reflection sends the unit vector of ℚ³ to a coordinate axis, and the remaining two vectors lie in a rational coordinate plane ℚ² with squared norm t: t = x² + y² with x, y rational.

Lemma 6.2. 3 and 15 are not sums of two rational squares. If a² + b² = 3c² or 15c², take (a, b, c) a primitive integer triple. Squares mod 3 are 0 and 1, so a² + b² ≡ 0 forces 3 | a and 3 | b; then 9 divides 3c² or 15c², so 3 | c, contradicting primitivity.

A common scale. Fix any B vector b. For two rational A representatives a and a′, dividing s_a s_b = 5(a·b)² by s_a′ s_b = 5(a′·b)² gives s_a/s_a′ = ((a·b)/(a′·b))², a rational square. So after rational rescaling all A representatives share one squared norm s, and the five basis lines (suitably oriented) have Gram matrix sX, rationally congruent to that. The Gram determinant of five rational vectors in ℚ⁵ is det(V)², a rational square, so s⁵ det X is a rational square.

Class 2. Exactly, det X = 256/729 = (16/27)², so s⁵ is a square, s is a rational square, and we may rescale to s = 1: there is a rational V with VVᵀ = X. The LDL factorisation X = LDLᵀ (L rational unit lower triangular) has diagonal (1, 8/9, 8/9, 2/3, 2/3); the rows of L⁻¹V are pairwise orthogonal rational vectors with these squared norms. Scaling by the rationals 3/2, 3/2, 3, 3 gives squared norms (1, 2, 2, 6, 6) = (1, 2, 2, 2t, 2t) with t = 3. Lemma 6.1 would make 3 a sum of two rational squares, contradicting Lemma 6.2.

The regular simplex (6 + 10). Orient the six lines to have pairwise inner products −1/5 and take five as the basis: X has diagonal 1 and off-diagonal −1/5, det X = (6/5)⁴ · (1/5) = 1296/3125 = 36²/5⁵, and the LDL diagonal is (1, 24/25, 9/10, 4/5, 3/5). s⁵ det X = 36²(s/5)⁵ is a square, so s/5 is a rational square and we may rescale to s = 5, with Gram 5X and LDL diagonal (5, 24/5, 9/2, 4, 3). Rescaling within square classes and reordering gives pairwise orthogonal rational vectors of squared norms (1, 2, 3, 5, 30). Replace the u, v of squared norms 3 and 5 by (u + v)/2 and (5u − 3v)/2: their squared norms are (3 + 5)/4 = 2 and (75 + 45)/4 = 30, and their inner product is (15 − 15)/4 = 0. This gives (1, 2, 2, 30, 30) = (1, 2, 2, 2t, 2t) with t = 15, contradicting Lemmas 6.1 and 6.2. (This is the five-dimensional case of the classical Schoenberg–Pelling criterion for rational regular simplices: 6 is not a sum of two rational squares.)

A Hasse–Minkowski cross-check. A rational V with VVᵀ = G exists exactly when the form G is rationally equivalent to I₅. Independently of Lemma 6.1, compare invariants: the class-2 X and the simplex 5X both have determinant in the square class 1 and are positive definite, but their Hasse invariants differ from those of I₅ at p = 2 and p = 3, so neither is rationally equivalent to I₅. Likewise the Hilbert symbols (−1, 3)ₚ = (−1, 15)ₚ = −1 at p = 2, 3 confirm independently that 3 and 15 are not sums of two rational squares.

7. Conclusion on the grid

Sections 2–6 exclude every way rational coordinates could reach q = 1/5: exactly two blocks (§2), not 5 + 11, and 6 + 10 only as the regular simplex (§3), six classes for 7 + 9 and 8 + 8 (§4), five of them excluded by the unique metric (§5), and class 2 and the simplex by arithmetic (§6). With Proposition 1.2, every 16 lines with rational coordinates have q > 1/5 strictly, so 10¹⁸q > 2 · 10¹⁷ and

K = ceil(10¹⁸ q) ≥ 200000000000000001.

The bound is attained. Computing all 120 squared overlaps of the package’s nine-decimal answer exactly, the largest is

q = 31903962418344681393274995137809561 / 159519812091723406674694957320312413,

which exceeds 1/5 by about 3.66 × 10⁻¹⁹, so K = 200000000000000001, displayed as μ = 0.447213596. This equals the current site record, so the record is the grid optimum. That rational points cannot reach 1/5 while the integer score reaches its minimum is no contradiction: rounding up gives every q in (1/5, 1/5 + 10⁻¹⁸] the same score.

Our verification

zzzcy #308 emailed the proof package on 6 October 2026, stating that it was generated with AI assistance. Under the site’s rules we ran none of its scripts and read only its data files. We checked the hand arguments of Sections 1–3 and 5–7 line by line; the finite computations were replayed by the site’s own program tools/p60-certificates.py, in exact rationals and our own ℚ(√5) arithmetic, in about 2 minutes:

• Our own exhaustion of Section 4: 24,310 column subsets, 24,290 of rank 5, 6,210 with enough admissible rows, 7,400 raw matrices, exactly the set in the package’s witness file.
• All 7,400 switching witnesses (row and column permutations with sign flips) applied entry by entry, each landing on one of the six representatives, with multiplicities 480, 1,920, 400, 1,280, 1,160 and 2,160.
• For each class, Λ rebuilt in exact ℚ(√5), C₀ = Σ w⁰λᵀλ, Σ w⁰ = 5, positive definiteness and unit diagonals checked, and both blocks’ Gram matrices rebuilt from the unique metric: classes 0, 1, 3, 4 have a within-block pair at 9/25, class 5 an A-internal pair at exactly 1/5, and class 2 is feasible over ℝ.
• The obstructions for class 2 (det 256/729, LDL 1, 8/9, 8/9, 2/3, 2/3) and the simplex (det 1296/3125, scaled to 5X) rechecked by LDL and determinant, and independently by Hasse–Minkowski invariants (different from I₅ at p = 2 and 3); (−1, 3)ₚ = (−1, 15)ₚ = −1 at p = 2, 3.
• Brute force for the finite claims of Section 3: the largest family of (±1, …, ±1)/√5 lines with pairwise inner products ±1/5 has 5 lines; at most 6 of the m = 4 candidates are compatible; and the maximal balanced-subset counts 2, 6, 8, 20 were sanity-checked over integer weights.
• The package’s answer scored exactly: q = 31903962418344681393274995137809561/159519812091723406674694957320312413, score 200000000000000001.

To rerun: python tools/p60-certificates.py <package dir>; the result is PASS.

Two corrections to the text. Neither affects validity, and this page states the corrected versions. (1) Section 7 of the package’s proof gives 9/25 as the violation for classes 0, 1 and 4, whereas the certificates for those classes name a pair at 1/4; both exceed 1/5, and 9/25 is indeed the largest under the unique metric. (2) The m = 4 case in Section 5 of the package says lines differing in one sign have inner product 3/5; that holds only once the sign of the √3 term is fixed to be + (flipping that sign gives −1/5). The conclusion, at most two lines per j and six in all, is correct, and we confirmed it by brute force. Also, the counting bound in the 5 + 11 case gives at most 6 lines where the true maximum is 5; both are far below 11.

Credit and scope

μ² ≥ 1/5 is R. A. Rankin’s orthoplex bound (1955), and the projection-matrix formulation follows Conway, Hardin and Sloane (1996); 16 lines attaining 1/√5 were known, and are listed in Henry Cohn’s archive of Grassmannian packings. What this proof adds is (b): rational coordinates cannot reach 1/5, so the current site record 200000000000000001 is the optimum on the nine-decimal grid, and the record holder is unchanged. The adopted contribution earns zzzcy #308 one permanent +2 proof award.

Cohn · Conway–Hardin–Sloane · Open P60