n = 14 · Case Records · The Squares Project

n = 14 proved ★ corrects Nagamochi 2005O=

$s (14) = 4$

The best packing known for 14 squares, side

4

345

3.7424.742

\sqrt{n}

\sqrt{n} + 1

Proven

$s (14) = 4$

new result
optimal
exact

Citation record n-014

lowerchelokot 2026, GitHub corrects Nagamochi 2005 (confirmed T-086)

Bounds

Best known packing

$4$

Construction: grid
Tilt angles: $0^{\circ}$
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$4$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: Erich Friedman 2009
Kind: unavoidable points
Note: Friedman's DS7 Theorem 8 starts with twelve almost-unavoidable points; geometric cases and conditional covers complete the argument (archived PDF pp. 21–23).
Source: [Friedman DS7]
Evidence: E-migrated-lower-report

Verified lower bound

$4$

The reported value, verified here.

Corrects: Nagamochi 2005 (T-007)
Evidence: E-chelokot-square-minus-two-lean

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
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
T-085 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
T-086 V3 C3 chelokot · 2026-10-02 · 16 cases
$s (k^{2} - 2) = k$ for every integer $k \geq 2$ ; $k = 3 \dots 18$ are the cases held here

Verification

upper: replayed here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 10 of the retained witness (witness id 11) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 3 of its 14 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

5 evidence entries

E-kingbird-upper-register, E-migrated-lower-report, E-basic-grid-upper, E-chelokot-square-minus-two-lean, E-nagamochi-lower

[Kingbird] record catalogue
[Friedman DS7] lower bound proof
[chelokot Nagamochi counterexample 2026] formal certificate

In the frontier survey On GitHub

$s (14)$ — solved

$s (14) = 4$ . Friedman’s DS7 proof combines geometric case analysis with conditional point covers.

The packing

The record catalogue does not picture $n = 14$ : no arrangement has ever been found that beats the trivial $⌈ \sqrt{14} ⌉ = 4$ 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

Friedman’s DS7, Theorem 8, archived PDF pp. 21–23, starts with twelve almost-unavoidable points in a container of side $4 - ε$ . Two of the fourteen squares have interiors missing these points, which localizes their centers. Five configurations up to symmetry, with further subcases, use geometric exclusions and additional conditional point covers (Figures 31–33). The helper steps are part of the proof.

The verified lower-bound evidence recorded here remains the independent Nagamochi result, E-nagamochi-lower. Corrected 2 October 2026: the verified lower bound here is now chelokot’s Lean theorem $s (n^{2} - 2) = n$ , replayed here with its axiom receipt (T-086); Nagamochi’s result is a reported bound, his Lemma 1 being false (Karakuş 2026; review). This register had recorded that proof as verified, its own error, logged as defect D-516.

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-chelokot-square-minus-two-lean`	replayed here	producer’s code	`V-chelokot-lean` (external); `V-replay-chelokot-lean` (first-party, premises)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)