T-237: $s(2),s(3),s(4)=2$$s(2),s(3),s(4)=2$ and s(5)=2+1/2​=2.70710678…$s(5)=2+1/\sqrt{2}=2.70710678\dots$, the classical first cases

S3 V3 C3 Optimality confirmed

1979 published · Göbel; Friedman · $n=2,3,4,5$$n=2,3,4,5$

$s(2)$$s(2)$ = $s(3)$$s(3)$ = $s(4)=2$$s(4)=2$ and $s(5)=2$$s(5)=2$ + 1/√2 = 2.70710678118654752440…, the exact values at the first four counts above one square, which the case records n-002 to n-005 hold on the published proofs, the exact audit and the exact replays their verified bounds cite.

Göbel's 1979 survey of geometrical packing and covering problems, the first publication on the problem by Friedman's account, gives the exact value as known for $n=2$$n=2$, 3 and 5 and the squares of integers, and proves $s(5)$$s(5)$: its Proposition 1 says that a square of side 2 + √2/2 - ε holds no five unit squares for any ε > 0, since every unit square inside it covers one of four points at distance 1 - ε/3 from the sides, in an outline of three cases whose calculations are omitted. The packing at that side, Göbel's, puts four squares in the corners and the fifth, turned 45°, in the middle.

Friedman's survey proves $s(2)$$s(2)$ = $s(3)=2$$s(3)=2$ as its Theorem 1: by its Lemma 1 a unit square in [0, 2]^2 contains the point (1, 1) wherever its centre lies, so that one point is unavoidable. $s(4)=2$$s(4)=2$ is the area bound $s(n)$$s(n)$ ≥ √n met by the $2\times 2$$2\times 2$ grid, which also packs two and three squares at side 2. The survey's Theorem 2 proves $s(5)$$s(5)$ again, by the four unavoidable points (1, 1), (1, 1 + 1/√2), (1 + 1/√2, 1) and (1 + 1/√2, 1 + 1/√2) of [0, 2 + 1/√2]^2, the argument chelokot's Lean proof formalizes (T-238) and this repository audits exactly (E-n005-friedman-theorem2-audit).

Göbel, Geometrical Packing and Covering Problems, Math. Centre Tracts 106, 1979; Friedman, Packing Unit Squares in Squares: A Survey and New Results, Electron. J. Combin. Dynamic Survey DS7, cited in its 2009 revision.