Case record

The best packing known for 23 squares, side

5

, Nagamochi 2005

$n = 23$

O= corrects Nagamochi 2005proved

$s (23) = 5$

456

4.7965.796

\sqrt{n}

\sqrt{n} + 1

Proven

$s (23) =$ $5$

optimal
exact

Citation record n-023

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

Bounds

Best known packing

$5$

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

Verified upper bound

$5$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: 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

$5$

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 Hosono 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ş; Vlasenko · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
T-086 V3 C3 Vlasenko · 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
T-124 V0 C0 Daniel after Couzo · 2026-10-07 · 178 cases
Reported non-strict local minima for 178 source configurations

Verification

upper: replayed here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

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

$s (23) = 5$ , from Nagamochi’s infinite family $s (m^{2} - 1) = s (m^{2} - 2) = m$ at $m = 5$ . 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.

A cautionary case about enumerations

$n = 23$ is a good test of whether a source’s list of solved cases is complete. Wikipedia’s list — $2, 3, 5, 6, 7, 8, 10, 13, 14, 15, 24, 34, 35, 46, 47, 48$ — omits 23, along with 22 and 33, and truncates Nagamochi’s infinite family to a few of its members. Other enumerations include it.

The union across sources, plus Nagamochi’s theorem stated in general form, is the safe reading: $n = 23$ is covered, and the omission is an incomplete enumeration rather than a mathematical subtlety. The general theorem subsumes a large slice of the table — $2, 3, 7, 8, 14, 15, 23, 24, 34, 35, 47, 48, 62, 63, 79, 80, 98, 99, \dots$ — and any list that enumerates members instead of stating the family will keep springing leaks.

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)

Bounds

Results in the register

s(23)s(23) — solved

A cautionary case about enumerations

Verification Code

$s (23)$ — solved