n = 4 · Case Records · The Squares Project

n = 4 provedO=R

$s (4) = 2$

The best packing known for 4 squares, side

2

123

\sqrt{n}

\sqrt{n} + 1

Proven

$s (4) = 2$

optimal
exact
rigid

Bounds

Best known packing

$2$

Construction: —
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$2$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Kind: perfect square
Evidence: E-basic-area-lower

Verified lower bound

$2$

The reported value, verified here.

Evidence: E-basic-area-lower

Gap

Solved: the verified bounds meet.

Results in the register

T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows

Verification

upper: replayed here; lower: replayed here

—

Rigidity

locally rigid, verified, exact algebraic

Evidence: E-perfect-square-tiling-rigid

Scope

This record's side is verified above and below at exactly 2, so its 4 unit squares of total area 4 sit in a 2 by 2 container of area 4. The packing is a tiling with no slack anywhere, so no square admits any feasible motion. This is global rather than local, and holds for the exact configuration rather than for a materialized approximation of it. It says nothing about s(n) beyond what the tiling itself shows.

Evidence and sources

4 evidence entries

E-kingbird-upper-register, E-basic-area-lower, E-basic-grid-upper, E-nagamochi-lower

[Kingbird] record catalogue
[Friedman DS7] survey
[Alpert et al. 2023] context

In the frontier survey On GitHub

$s (4)$ — solved

$s (4) = 2$ . Established by triviality (a perfect square).

The packing

Found by an unrecorded author, via an unrecorded method.

The lower bound

$4$ is a perfect square, so the $2 \times 2$ grid is optimal and the area bound $\sqrt{n}$ is already tight.

Corrected 4 October 2026: the verified lower bound cites the area bound, E-basic-area-lower; until 2 October it cited Nagamochi 2005 (E-nagamochi-lower) at the same value, whose Lemma 1 is false (D-516).

The complete optimal configuration space

Exp-015 excludes genuinely rotated side-2 packings and exactly enumerates 24 isolated labelled grids. Relabelling, with or without the container’s D4 action, leaves one quotient point.

The rigid frontmatter field above is the historical catalogue flag defined by the frontier schema; it is not the repository’s now-proved moduli-space conclusion.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.

bound	evidence	run	code	programs
verified lower	`E-basic-area-lower`	replayed here	independent	`V-check-basic-bounds` (first-party)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)