The region and five squares
Let C be [0,3] x [0,3] with its four open corner unit squares removed. Equivalently, C is the union of the central unit square and the four unit-square arms B, R, T and L. For a finite set S in C, let d(S) be its smallest pairwise Euclidean distance. The verifier stores d(S) squared.
The attaining constructions
For four points choose
(1,0), (3,1), (2,3), (0,2).
In cyclic order these are the vertices of a square: its four side lengths are sqrt(5), while its diagonals have length sqrt(10). Thus d(S) = sqrt(5).
For five points add the centre (3/2,3/2). Its squared distance to every outer point is 5/2, while all outer-pair squared distances are at least 5. Hence d(S) = sqrt(5/2).
Four points: the four arms force a short side
Assume for contradiction that four points are pairwise farther apart than sqrt(5). A unit square has diameter sqrt(2), so no two points can lie in the same one of the five unit squares covering C. If one point lies in the central square, its union with any arm is a 1 by 2 rectangle of diameter sqrt(5), already a contradiction. The only remaining case has one point in every arm.
Call them B, R, T and L in cyclic order. Write X for the sum of the squared horizontal differences along BR, RT, TL and LB. The two middle horizontal coordinates x_B,x_T lie in [1,2], the right coordinate x_R in [2,3], and the left coordinate x_L in [0,1]. For fixed x_R and x_L,
X = f(xB) + f(xT),
f(m) = (xR−m)² + (m−xL)².
The function f is convex, so its maximum on [1,2] is at an endpoint. The same endpoint argument puts x_R and x_L at endpoints too. The four possibilities (x_R,x_L) = (2,0),(2,1),(3,0),(3,1) give X at most 8, 2, 10 and 8 respectively; hence X <= 10. Rotating the argument by 90 degrees gives the analogous vertical sum Y <= 10. Therefore
|BR|² + |RT|² + |TL|² + |LB|² = X + Y ≤ 20.
At least one of the four adjacent squared distances is therefore at most 5. This contradicts the assumption and proves d(S) <= sqrt(5).
Five points: one entire arm is close to the centre point
Now suppose five points were pairwise farther apart than sqrt(5/2). Since sqrt(5/2) > sqrt(2), each of the five unit squares can contain at most one point. Because they cover C, there must be exactly one assigned point in the central square and one in each arm. Write the central point as
c = (3/2 + σ, 3/2 + τ),
a = |σ|, b = |τ|, 0 ≤ a,b ≤ 1/2.
Of the top and bottom arms, choose the one nearer to c. The largest squared distance from c to any point of that whole arm is
Mv = 5/2 + a − 3b + a² + b².
Indeed, the largest horizontal displacement is 1/2+a and the largest vertical displacement to the nearer arm is 3/2-b. Likewise, for the nearer of the left and right arms,
Mh = 5/2 + b − 3a + a² + b².
At least one of M_v and M_h is at most 5/2. Otherwise, adding the two strict inequalities would give a²+b² > a+b. But 0 <= a,b <= 1/2 implies a²+b² <= (a+b)/2, an impossibility (and at a=b=0 both maxima equal 5/2). Thus one entire arm lies within distance sqrt(5/2) of c. Its assigned point contradicts the supposed separation. Therefore d(S) <= sqrt(5/2).
Both upper bounds meet the constructions, proving the theorem. Equivalently, P21's exact stored optima are 5 and 5/2. ∎
Why n = 9 is not closed
The submitted nine-point arrangement is valid and attains sqrt(5)/2: add the centre and the four side midpoints of the outer four-point square. But exhibiting a value is only a lower bound. The symmetry sentence does not show that every nine-point arrangement has a pair this close, and no independent upper bound is presently known. P21 n=9 therefore remains open.
What came from the submission
NUE_13 #31 supplied the four-, five- and nine-point constructions and proposed their optimal values. The arena verified all three constructions, rejected symmetry as an upper-bound argument, and supplied the rigorous inequalities that settle n=4 and n=5. The conjecture and the completed proof are credited separately.