The current spherical-code table marks proved optima with an asterisk. Its 15-point row has no asterisk. Kottwitz's primary paper describes its solutions for 15 through 90 circles as conjectured solutions. Musin and Tarasov later proved the 14-point case by enumerating irreducible contact graphs, and their proof makes no claim for 15 points.

The strongest construction checked here and the elementary cap-area bound give \[ \arccos(\alpha)\leq\theta_{15}\leq2\arccos(13/15), \] or numerically \[ 53.65785012993268\ldots^\circ \leq\theta_{15}\leq 59.85286973322849\ldots^\circ. \] For the upper bound, place disjoint caps of angular radius \(\theta_{15}/2\) around the points. Each cap has area \(2\pi(1-\cos(\theta_{15}/2))\). Their total area is at most \(4\pi\), so \(15(1-\cos(\theta_{15}/2))\leq2\).

Let \(\alpha\) be the unique root in \[ 0.5926059029250737<\alpha<0.5926059029250738 \] of \[ 13x^5-x^4+6x^3+2x^2-3x-1=0. \] Henry Cohn's spherical-code table gives a 15-point code in \(\mathbb R^3\) whose largest pairwise inner product is exactly \(\alpha\). The table explains that a listed minimal polynomial means an exact code attaining that value has been checked to exist. Hence \[ \theta_{15}\geq\arccos(\alpha) =53.65785012993268\ldots^\circ. \] The corresponding minimum chordal distance is \[ \sqrt{2-2\alpha}=0.9026561882299664\ldots. \] The polynomial signs at the two rational endpoints have opposite signs. Its derivative is positive throughout \([0.59,0.60]\), which isolates the stated root. The accompanying artifact checks these facts with exact rational arithmetic.

Download the cited 15-point coordinate file lawfully from the Hardin-Sloane-Smith library and pass its local path to the checker. Number its vectors in file order and put \(u_i=v_i/\lVert v_i\rVert\). Every decimal token is treated as an exact rational number. The checker verifies the source-file and normalized-token hashes before using the coordinates. The source coordinates are not stored in this packet.

Exact squared comparisons prove \[ u_i\mathbin{\cdot}u_j<0.5926059032 \quad(i\ne j). \] Thus these published decimals alone certify a minimum angle greater than \(\arccos(0.5926059032)=53.6578501103\ldots^\circ\). This is a rigorous lower bound for the normalized decimal realization. The exact algebraic construction in the first claim has the slightly larger endpoint \(\arccos(\alpha)\).

The 30 pairs with normalized inner product above 0.5926059008 are ``` 1-4 1-9 1-10 1-13 2-3 2-7 2-11 2-12 3-8 3-9 3-10 4-5 4-9 4-11 5-6 5-7 5-15 6-7 6-12 6-14 6-15 7-11 7-12 8-10 8-14 9-10 10-13 12-14 13-14 13-15 ``` Every other normalized inner product is below 0.424696, leaving a gap larger than 0.1679 between contacts and noncontacts. This gap makes the contact graph insensitive to the source's rounding. The largest decimal-model inner product belongs to pair 13-14.