n = 2 · Case Records · The Squares Project

n = 2 provedO=

$s (2) = 2$

The best packing known for 2 squares, side

2

123

1.4142.414

\sqrt{n}

\sqrt{n} + 1

Proven

$s (2) = 2$

optimal
exact

Bounds

Best known packing

$2$

Construction: grid
Tilt angles: $0^{\circ}$
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: counting
Source: [Friedman DS7]
Evidence: E-side2-center-lower

Verified lower bound

$2$

The reported value, verified here.

Evidence: E-side2-center-lower

Gap

Solved: the verified bounds meet.

Results in the register

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

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 0 of the retained witness (witness id 1) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 2 of its 2 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.

Evidence and sources

4 evidence entries

E-kingbird-upper-register, E-basic-grid-upper, E-basic-area-lower, E-side2-center-lower

[Kingbird] record catalogue
[Friedman DS7] lower bound proof

In the frontier survey On GitHub

$s (2)$ — solved

$s (2) = 2$ . Established by an elementary counting argument.

The packing

The record catalogue does not picture $n = 2$ : no arrangement has ever been found that beats the trivial $⌈ \sqrt{2} ⌉ = 2$ grid, so the grid is still the best known packing. That is a statement about what has been searched, not a proof.

The lower bound

Established by an elementary counting argument.

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-side2-center-lower`	replayed here	producer’s code	`V-optimal-moduli` (first-party)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)