1. Classical input and upper bound
We use the classical theorem: among any three points in a unit square, some pair has distance at most √6 − √2. This is the proved three-point case already cited for P15 n=3, not a new theorem claimed here. See the distance column and proved-optimal notation in Packomania · circles in a square (n=3; equivalently the normalized centre-separation problem).
Cover the rectangle by [0,1] × [0,1] and [1,2] × [0,1]. Assign each point to exactly one containing square, with arbitrary assignment on x=1. At least one square contains three of the five assigned points. Applying the theorem to those three points gives a pair at distance at most √6 − √2, and hence the same upper bound for the minimum distance of all five points.
2. Exact attaining construction
s = √3; A = (0,0), B = (1,2−s), C = (s,1), D = (2,0), E = (2−s,1).
Since 1 < s < 2, all five points lie in the rectangle. All ten squared distances are:
AB² = AE² = BC² = BD² = BE² = CD² = 8−4√3;
AC² = AD² = DE² = 4; CE² = 16−8√3.
Here 0 < 8−4√3 < 4 and 16−8√3 = 2(8−4√3). The minimum distance is therefore √(8−4√3) = √6 − √2. The upper bound is attained, proving continuous optimality. ∎
Credit, scope and precision
XSsMC #250 submitted the two-square reduction on September 14, 2026. MinMax Arena checked the reduction, supplied the exact attaining witness and boundary assignment, and prepared this bilingual exposition. The submitted informal proof of the three-point theorem is replaced by an explicit citation to that classical result. This adopted contribution earns one permanent +2 proof award; no historical-first claim is made.
Only the continuous n=5 case is closed through the existing proven-optimal mechanism. Historical records remain. Every squared distance on the nine-decimal coordinate grid is rational, whereas 8−4√3 is irrational, so no grid configuration attains this continuous bound exactly. No rounded certificate is certified as grid-optimal, and no conclusion for n≥6 follows.