n = 34 · Case Records · The Squares Project

n = 34 proved ★ corrects Nagamochi 2005O=

$s (34) = 6$

The best packing known for 34 squares, side

6

, Hiroshi Nagamochi 2005

567

5.8316.831

\sqrt{n}

\sqrt{n} + 1

Proven

$s (34) = 6$

new result
optimal
exact

Citation record n-034

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

Bounds

Best known packing

$6$

Found by: Hiroshi Nagamochi 2005
Construction: hand
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$6$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: Hiroshi Nagamochi 2005
Kind: Nagamochi
Note: General closed form: $s (N)$ >= min(ceil(sqrt(N)), sqrt(N - 2*floor(sqrt(N)) + 1) + 1).
Source: [Nagamochi 2005]
Evidence: E-nagamochi-lower

Verified lower bound

$6$

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 28 of the retained witness (witness id 29) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 3 of its 34 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-nagamochi-lower, E-basic-grid-upper, E-chelokot-square-minus-two-lean

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

In the frontier survey On GitHub

$s (34)$ — solved

$s (34) = 6$ , from Nagamochi’s infinite family $s (m^{2} - 1) = s (m^{2} - 2) = m$ at $m = 6$ . Corrected 3 October 2026: the verified lower bound here is 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; this record’s prose was missed by the correction of 2 October and is corrected here.

The packing

Found by Hiroshi Nagamochi in 2005, via a hand construction.

The lower bound

The strongest lower bound independently verified in this record is chelokot’s Lean theorem $s (n^{2} - 2) = n$ at $n = 6$ (T-086). Nagamochi’s general closed form, $s (N) \geq min (⌈ \sqrt{N} ⌉, \sqrt{N - 2 ⌊ \sqrt{N} ⌋ + 1} + 1)$ , is recorded as a reported bound: its published proof rests on his Lemma 1, which Karakuş showed false.

See the Frontier corpus summary for the current aggregate count; source-reported bounds are recorded separately.

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)