n = 24 proved ★ corrects Nagamochi 2005O=

s(24)=5

The best packing known for 24 squares, side 5, Erich Friedman 1999
5
456
4.8995.899
nn+1

Proven

s(24)=5

  • new result
  • optimal
  • exact

Citation record n-024

lowerKarakuş 2026 corrects Nagamochi 2005 (confirmed T-083, T-084)

Bounds

Best known packing

5

Found by
Erich Friedman 1999
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

5

Proved by
Erich Friedman 1999
Kind
unavoidable points
Source
[Friedman DS7]
Evidence
E-migrated-lower-report
Verified lower bound

5

The reported value, verified here.

Corrects
Nagamochi 2005 (T-007)
Evidence
E-karakus-strip-lower, E-karakus-strip-measure-interval
Gap

0

Solved: the verified bounds meet.

Results in the register

Verification

upper: replayed here; lower: external proof (read here), audited here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

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

s(24) — solved

s(24)=5. Established by an unavoidable point set, Erich Friedman (1999).

The packing

Found by Erich Friedman in 1999, via a hand construction.

The lower bound

Proved by exhibiting an unavoidable set: a set of points in the container that every unit square placed inside must contain. With n−1 such points, n disjoint squares are impossible by pigeonhole.

The verified lower-bound evidence recorded here is Karakuş’s rectangle bound, E-karakus-strip-lower, which gives exactly s(k2−1)=k (T-084). Corrected 4 October 2026: until 2 October it was the Nagamochi result, E-nagamochi-lower, whose published proof rests on Nagamochi’s Lemma 1, which Karakuş showed false; its value here is the same, and it is now a reported bound (review of 2 October 2026). 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.

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-karakus-strip-lower a published proof no code no verification code
verified lower E-karakus-strip-measure-interval audited here independent V-check-karakus-strip-measure (first-party)
verified upper E-basic-grid-upper replayed here independent V-check-basic-bounds (first-party)