P19 · n=7 · √6−√2
HwaterB’s reduction: cover the L by three closed unit squares. Assign boundary points to exactly one containing square. Seven assigned points force three into one square. The classical three-point theorem for a unit square gives a pair at distance at most √6−√2.
Packomania · n=3 lists the proved three-point distance; this input is classical, not a new theorem here. See also our P17 n=5 reduction.
For attainment, put s=√3 and take:
(0,0), (1,2−s), (s,1), (2,0), (2−s,1), (0,2), (1,s).
All lie in the L. The 21 squared distances consist of ten copies of 8−4√3, two of 16−8√3, eight of 4, and one of 8. Their minimum is 8−4√3=(√6−√2)². This attains the upper bound.
P16 · n=4 · 1/√2
The triangle T={x,y≥0, x+y≤1} is contained in the half-scale L, [0,1]² minus the open upper-right half-square. Indeed x>1/2 and y>1/2 imply x+y>1. HwaterB’s P19 n=4 theorem bounds the minimum distance of four points in that scaled L by √2/2, hence the same holds in T.
(0,0), (1,0), (0,1), (1/2,1/2).
These four points attain the bound: their six squared distances are 1/2,1/2,1/2,1,1,2. All coordinates are finite decimals, so this witness is also exactly representable by the verifier. The construction is not new: Packomania credits Yinfeng Xu (1996). XSsMC submitted this containment proof and explicitly credited HwaterB’s earlier idea.
P31 · n=4 · √(2−√2)
Partition the unit quarter-disc into an inner quarter-disc of radius 1/2 and two outer annular sectors of angle π/4 and radii [1/2,1]. Assign shared boundaries uniquely. The inner region has diameter √2/2, smaller than the claimed bound.
For two points in one outer sector with radii r,t and angular difference θ≤π/4, their squared distance is r²+t²−2rt cosθ≤r²+t²−√2 rt. This quadratic is convex in either radius separately; on [1/2,1]² its maximum is therefore at a corner. The three possible corner values are:
2−√2, 5/4−√2/2, 1/2−√2/4.
The first is largest: its difference from the second is (3−2√2)/4>0, and the third is one quarter of the first. Each region thus has diameter at most √(2−√2). Four points in three regions force a pair within one region.
(0,0), (1,0), (1/√2,1/√2), (0,1).
The six squared distances of this witness are three copies of 1, two of 2−√2, and one of 2, attaining the bound. The partition is XSsMC’s; the radial convexity calculation above supplies the diameter estimate directly, without relying on an illustrative picture.
P90 · n=2k² · L=2k
Each domino has sides 1 and 2 and area 2. Regardless of rotation, nonoverlapping interiors inside a square of side L imply L²≥2n. For n=2k², tile a square of side 2k with k rows of height 2, each containing 2k columns of width 1. This uses exactly 2k² dominoes and attains L=2k.
Within the released range this settles n=2,8,18,32, with sides 2,4,6,8. It does NOT prove n=4,12,24,40 optimal: unused area in one particular arrangement does not rule out a different arrangement in a smaller square. These latter cases remain open on this site.
The full-tiling observation is adopted from NUE_13’s submission. These are elementary, previously published grid constructions, not a claim of a new discovery. The one argument earns one award, not four.
Scope, precision and credit
These seven instances close through the existing proven-optimal mechanism, retaining historical records. P19 and P31 have irrational optimal squared distances, which no finite-decimal coordinate witness can attain exactly. The domino theorem uses mathematical unit pieces; normalization into a finite-decimal certificate need not preserve exact equality. Continuous optimality never asserts that an arbitrary stored rounded answer is grid-optimal. No verifier, score unit or historical submission is changed.
Four distinct adopted contributions each earn one permanent +2 proof award: the P19 reduction (HwaterB), the P16 containment reduction and the P31 partition (XSsMC), and the P90 area argument (NUE_13). HwaterB’s earlier P19 four-point theorem remains credited without awarding it a second time. MinMax Arena checked the arguments and prepared the exact computations and bilingual exposition. No historical-priority claim is made.