Small grids with no five points on a sphere

A grid can hold surprisingly few points if every five must avoid a common sphere or plane. On the cubic grids of side length three and four, the exact maxima are 8 and 11. Larger constructions reach 14 points on the next grid and 18 points on the one after that. Finding those sets is much easier than proving that no larger set exists.

Let $C(n)$ be the largest admissible subset of $\{0,\ldots,n-1\}^3$ . A plane counts alongside a sphere in this definition. Each horizontal layer therefore holds at most four points, giving the immediate bound $C(n)\le 4n$ .

Grid side $n$	Verified range for $C(n)$	Evidence for the upper endpoint
3	$C(3)=8$	SAT exclusion, with a recorded checked LRAT proof
4	$C(4)=11$	SAT exclusion, with a recorded checked LRAT proof
5	$14 \le C(5) \le 20$	Four points per layer
6	$18 \le C(6) \le 24$	Four points per layer

The larger grids also have completed computational searches reporting no sets of size 15 and 19, respectively. Those results support the candidate equalities $C(5)=14$ and $C(6)=18$ . They remain single-program exclusion evidence: the independent exclusion check has not succeeded. The table keeps that distinction visible.

An exact test for every five points

Replace each point $(x,y,z)$ by the row $(x,y,z,x^2+y^2+z^2,1)$ . Five points lie on a common sphere or plane precisely when

\det\begin{pmatrix} x_1&y_1&z_1&x_1^2+y_1^2+z_1^2&1\\ \vdots&\vdots&\vdots&\vdots&\vdots\\ x_5&y_5&z_5&x_5^2+y_5^2+z_5^2&1 \end{pmatrix}=0.

A zero determinant supplies coefficients for an equation of the form

a(x^2+y^2+z^2)+bx+cy+dz+e=0.

If $a$ vanishes, the equation describes a plane. Otherwise, completing the square gives a sphere. Integer coordinates allow the determinant to be evaluated exactly, without a tolerance for points that are almost on a sphere.

This makes a construction easy to verify: enumerate every five-point subset and check that its determinant is nonzero. The larger constructions have been checked with separately implemented determinant calculations. An exclusion result has a different burden: every possible larger set must be ruled out, including every branch removed by a pruning rule.

Reducing the search to layers

The search fills the grid one horizontal layer at a time. Within a layer, a four-point subset must avoid a common circle or line. Such a degenerate quadruple would make the lifted determinant vanish after any fifth point was added.

For a square layer of side length five, there are 12,650 four-point subsets. Exactly 826 are excluded by this rule, leaving 11,824. Rotations and reflections reduce the allowed first-layer choices further: the enumeration uses 1,905 symmetry classes for the grid of side length five and 8,133 for side length six. The first inventory includes nonempty subsets of up to four points; the second starts with two-point subsets, since a target-sized set can be reflected to have at least two points in its first layer.

As points are added, the program records which unused points would complete a forbidden five-set. These masks allow it to discard impossible extensions quickly. A capacity bound stops a branch when even the largest permitted choices in all remaining layers cannot reach the target.

The corrected search on the smaller of these grids visited about 591 million nodes. The larger run completed all 8,133 first-layer classes and recorded 448,735,206,762 nodes, counting each class once. Both reported no target-sized set. A completed run is meaningful evidence, but the completeness of the algorithm and the validity of its pruning rules still need scrutiny.

Why the checker matters

The first search used a capacity bound that overlooked some unfilled layers. It could discard a branch that still had enough room to reach the target. After the correction, the search visited more nodes and reached the same negative result. On the grid of side length five, the corrected program also found a valid set of 14 points.

That positive control checks whether the program can find a solution; it cannot establish that every excluded branch was impossible. A separate implementation was intended to test the exclusion. Review found defects in its combination iterator and cache handling, so its unfinished runs provide no corroboration.

For the two smallest grids, the SAT approach leaves an LRAT certificate, a sequence of logical deductions that a separate checker can validate. For the larger grids, the retained evidence is the enumerator source, completed run records and valid constructions. The reported candidate equalities should be assessed at that level of evidence until a separate exclusion succeeds or a checkable proof is produced.

What the small cases establish

The exact values and constructions already rule out one tempting extrapolation. The first three proposed maxima follow $3n-1$ , but an admissible set of size 18 on the sixth grid exceeds the value 17 predicted by that expression. A short sequence of small cases does not determine the general answer.

The general upper bound used here remains $4n$ . Improving it requires an argument that connects different layers, or a search result whose coverage can be checked independently.

Sources and verification

The research manuscript contains the constructions, proof records, search method and limitations. The small-grid source and records and sixth-grid enumerator allow the computational claims to be inspected.

The unlisted precursor reported the larger searches too strongly and included an incorrect formula comparison. This version separates checked proof records, independently verified constructions and single-program exclusion evidence.