n = 7 · Case Records · The Squares Project

n = 7 proved ★ corrects Nagamochi 2005O=

$s (7) = 3$

The best packing known for 7 squares, side

3

234

2.6463.646

\sqrt{n}

\sqrt{n} + 1

Proven

$s (7) = 3$

new result
optimal
exact

Citation record n-007

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

Bounds

Best known packing

$3$

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

Verified upper bound

$3$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: Said El Moumni 1999
Kind: counting
Note: El Moumni's intended proof uses four marker points, geometric localization, and intersection-length budgets (printed pp. 282–288). D-344–D-347 retain limitations in the printed route; E-nagamochi-lower supplies independent verified evidence.
Source: [El Moumni 1999]
Evidence: E-migrated-lower-report

Verified lower bound

$3$

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

Open questions

Priority: s(7) determined (Bajmoczy (via Schrijver, via Gobel))

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
[El Moumni 1999] lower bound proof
[Friedman DS7] survey
[chelokot Nagamochi counterexample 2026] formal certificate

In the frontier survey On GitHub

$s (7)$ — solved

$s (7) = 3$ . El Moumni (1999) presents a geometric counting route with the limitations in the printed source noted below. The verified lower bound has independent support from Nagamochi. 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.

The packing

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

El Moumni’s Theorem 1, printed pp. 282–288 (volume PDF pp. 288–294), begins with four marker points. At least three of seven squares have interiors that avoid the marks. Localization then restricts their centers, and case analysis uses convexity and intersection-length budgets to seek a contradiction.

D-344–D-347 record limitations in this printed route: a negative segment length, a dropped minimum branch, an incorrect center label, and an undefined point. The recorded repairs are distinguished from the source and do not complete a faithful replay of the printed proof. The independent Nagamochi evidence E-nagamochi-lower continues to support the verified bound in this record. (Corrected 2 October 2026: that evidence is now reported; see the correction above.)

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)