Case record
The best packing known for 21 squares, side 5,

n=21

O=proved

s(21)=5

5
456
4.5835.583
nn+1

Proven

s(21)=5

  • optimal
  • exact

Citation record n-021

lowerDaniel after Burns, Massaccesi 2026, GitHub (confirmed T-052)

Bounds

Best known packing

5

Construction
grid
Tilt angles
0∘
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
Daniel 2026
Kind
counting
Scope
Unrestricted independent rotations with disjoint interiors; boundary contact allowed.
Note
evand/square-packing (28 September 2026) states s(21)=5 from a mixed cover of [0,5]^2, 7,536 weighted points plus mass spread uniformly along 1,872 interior grid-line segments of length 1/50, total 522368729933/(25*10^9) = 20.894749197 < 21, exactly D4-invariant and certified at margin zero by two separately written checkers, zm_mixed.py (exact rational) and zmx2 (binary64 enclosures widened outward), with a Lean theorem minSide 21 = 5 from that one computational hypothesis. Its CREDITS.md says the work was produced with an AI agent under human direction. It supersedes the same author's 5000/1001 of 23 September 2026, which stays as evidence.
Source
[evand square-packing 2026-09-28]
Evidence
E-n021-evand-mixed-cover-report
Verified lower bound

5

The reported value, verified here.

Evidence
E-n021-evand-mixed-cover-zmx2-replay
Gap

0

Solved: the verified bounds meet.

Results in the register

  • T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases

    s(n)≥min(⌈n⌉,n−2⌊n⌋+1+1) for 4≤n≤324

  • T-020 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 19–21

    s(n)≥24/5=4.80 for n=19,20,21

    Claim and records
    Claim
    s(19)≥24/5, s(20)≥24/5 and s(21)≥24/5, from this project's weighted fractional unavoidable-set certificate at container side 24/5 = 4.80.

    Two of the three cases previously held Nagamochi's 2005 general closed form in this register's independently verified lower fields -- min(ceil(sqrt(N)), sqrt(N - 2*floor(sqrt(N)) + 1) + 1), which gives 1 + sqrt(13) = 4.6055... at n=20 and 1 + sqrt(14) = 4.7416... at n=21 -- and the third held the 459/100 = 4.59 this project certified earlier the same day as T-019. The movement is +0.21 at n=19, +0.194449 at n=20 and +0.058343 at n=21, relative to those verified fields.

    The September 2026 DS7 audit records stronger external reports below 4.80 separately, with missing source proofs and table discrepancies explicit; no claim of historical priority follows from the earlier source omissions.

    The three sizes take no monotonicity step. Only Condition 2 mentions n among the five conditions, so an atom set of mass 946131/50000 certifies the side for every integer strictly above that mass, which is 19 and upward. From n=22 on the register already holds 5, so the certificate is true there and weaker; these three are where it moves anything.

    One rung is retained rather than a ladder. The side was reached in a single resumed column-generation run, not climbed to, so there is no weaker certificate at this size to compare it against.
    Significance
    Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value", and by parity with T-019, which has the same shape: one certificate moving three registered cases and displacing a published value.

    This one displaces more. The movement is +0.21 at n=19 against T-019's +0.0842, the largest single-case movement in the register; and at n=20 and n=21 it displaces the peer-reviewed 2005 closed form previously used in the verified register. The September 2026 source audit corrects the earlier claim that no size-specific bounds had been reported; it does not change these measured displacements of the verified fields.

    Held below S5 for the reasons T-019 was: none of the three is a central open case, the weighted-resource lineage predates this project, the pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, and no case changes character at the new value.

    A calibration note for whoever scores the next one. This is the fourth result from one instrument in a day, and the S4 anchor is being carried here by the displacement rather than by the technique, which T-017 already banked. Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 19n = 20n = 21registerevidence 1evidence 2

  • T-021 V3 C3 Levy after Burns, Massaccesi · 2026-09-05 · n = 20, 21

    s(n)≥97/20=4.85 for n=20,21

    Claim and records
    Claim
    s(20)≥97/20 and s(21)≥97/20, from this project's weighted fractional unavoidable-set certificate at container side 97/20 = 4.85. Both sizes held 24/5 = 4.80 from T-020 earlier the same week in this register's verified fields; the movement is +0.05 at each. The certificate does not reach n=19: its total mass is 19848723/1000000 = 19.848723, above nineteen, so Condition 2 gives it n=20 and upward and T-020's 24/5 rung, retained beside it, still carries n=19.

    The two sizes take no monotonicity step, for the reason T-020 gives: only Condition 2 mentions n among the five conditions, so an atom set of mass M certifies its side for every integer strictly above M. From n=22 on the register already holds 5, so the certificate is true there and weaker.

    Where the rung came from is worth the record. A pre-registered bisection of [24/5, 9977/2000] ran four rungs unattended. The uniform grid walled at this side -- its restricted optimum crossed twenty at round 31 of 32 and stood at 20.000439 with placements still violated -- while a second site set, the 24/5 certificate's own 2260 atoms scaled by 97/96 and unioned with the grids, converged below twenty at the same side. The certificate is the second construction's; the first construction's crossing is why H-062 asks for two.
    Significance
    Scored at S3 by the calibration note T-020 wrote for exactly this case: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at the same two sizes, one rung higher, and neither size changes character at 4.85. What it adds beyond a rung is a measurement rather than a theorem, and the measurement is registered as such: the m = 5 covering wall is bracketed to [97/20, 39/8] -- a certificate at 4.85, crossings above twenty on both constructions at 4.875 -- which is the first bracket this project has put around a covering wall, and it sits far below the method's ceiling of 4.9885 rather than at it. That bears on planning, not on the strength of this claim.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 20n = 21registerevidence 1evidence 2

  • T-034 V3 C3 Levy after Burns, Massaccesi · 2026-09-23 · n = 21

    s(21)≥122/25=4.88

    Claim and records
    Claim
    s(21)≥122/25, from this project's weighted fractional unavoidable-set certificate at container side 122/25 = 4.88. The case held 97/20 = 4.85 from T-021 in this register's verified field, and the movement is +0.03. The certificate does not reach n=20: its total mass is 5036431/250000 = 20.145724, above twenty, so Condition 2 gives it n=21 and upward, and T-021's 97/20 rung, retained beside it, still carries n=20.

    The size takes no monotonicity step, for the reason T-020 gives: only Condition 2 mentions n among the five conditions, so an atom set of mass M certifies its side for every integer strictly above M. From n=22 on the register already holds 5, so the certificate is true there and weaker.

    The site set is the plainest the generator offers: auto grids (34, 46, 56) at inset 1/2 with no seed and no windows, converged below twenty-one in 36 LP rounds. At the same side a T-021-seeded set ran out its deadline unconverged, and a five-window set converged but stalled the interval route on a seam where atom rows sit exactly B apart; neither run decides anything about the side.
    Significance
    Scored at S3 by the calibration note T-020 wrote and T-021 applied: "Further sizes from the same generator, absent a new technique or a case that changes character, belong at S3." This is the same generator at one of the same sizes, one rung higher, and n=21 does not change character at 4.88. What it adds beyond the rung is a reading about the instrument rather than a theorem: the stock generator with no seed and no windows converged where the seeded and windowed site sets did not decide. The side also sits above 39/8 = 4.875, where both of H-062's constructions crossed twenty at n=20; a mass above twenty is consistent with that wall and says nothing about n=20.
    Novelty
    apparently-novel Not found in the recorded search, subject to its stated gaps
    Records

    n = 21registerevidence 1evidence 2

  • T-050 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 21

    s(21)≥5000/1001=4.995004995…

    Claim and records
    Claim
    s(21)≥5000/1001 = 4.995004995..., by Daniel's weighted point certificate of 23 September 2026. It raised the verified bound by 2878/25025, about 0.115, over T-034.

    The certificate is 4,604 D4-invariant rational points in 580 orbits, total weight 260057/12500 = 20.80456 < 21, decided over the rational angle net at N=6000 by the method of T-049.

    It was replayed here on 27 September 2026 by the source's Rust verifier at N=6000, least captured weight 10000083/10^7 at bin 684 as the source records, and by its exact Python re-check on four bins including the binding one; the two are one angle-net method.

    Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.
    Significance
    Moved n=21 by 0.115 over T-034 to within 5/1001 of the grid's 5, past this repository's own fixed-shrink ceiling of 4.9885 for the format. A substantive case result, S3; superseded within two days by the same author's exact value. Confirmed on 11 October: supersession does not lower a score, and the step, 0.115 at one count, is a case result as T-021 and T-034 are.
    Novelty
    previously-published Present in an identified source
    Records

    n = 21registerevidence 1evidence 2sourcereview

  • T-052 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 21

    s(21)=5, by a mixed cover of points and grid-line segments

    Claim and records
    Claim
    s(21)=5: the lower half by Daniel's mixed cover of 27 September 2026, the upper half by the 5×5 grid.

    The cover is 7,536 weighted points of [0,5]^2 plus mass spread uniformly along 1,872 segments of length 1/50 on the interior grid lines, total 522368729933/(25*10^9) = 20.894749197 < 21, exactly D4-invariant. Every closed unit square in [0,5]^2 captures mass at least one, a boundary point and a segment along an edge counting in full.

    The source certifies that at margin zero with two separately written checkers, zm_mixed.py in exact rational arithmetic and the Rust zmx2 with outward-widened binary64 enclosures, and Lean proves minSide 21 = 5 from the one checker statement.

    zmx2 was replayed here in full on 28 and 29 September 2026, D4-reduced over 2,500 roots and unreduced over 20,000, every root's census equal to the source's; zm_mixed.py was only sampled.

    Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.
    Significance
    An exact value for a case that was open, the second of the s(k^2 - 4) family after T-051, and the release that introduced line mass on the grid lines, which is what makes a zero-margin cover below the count possible at an integer side. S4 by the anchor "a reusable technique"; T-053 reuses it at n=45. Confirmed on 11 October: line mass is the idea later exact values at an integer side reuse (T-053, T-062, T-066, T-067, T-064, T-081), which is what a reusable technique at S4 means here, though not every one does: the point-only routes (T-054, T-055) and the families proved by other measures (T-084, T-086) do without it. T-073's segments at n=83 and 101 to 105 are an extension within a framework and are S3.
    Novelty
    previously-published Present in an identified source
    Records

    n = 21registerevidence 1evidence 2evidence 3sourcereview

  • T-055 V3 C3 Hosono after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · n = 21

    s(21)=5 by a point-only route

    Claim and records
    Claim
    s(21)=5 by a second, point-only route: the lower half by Hosono's point-only measure, completed on 28 September 2026 with a Lean 4 reduction, the upper half by the 5×5 grid.

    The lower half is Daniel's s21_lower_4.9950.txt support (T-050) scaled by 1001/1000 and re-weighted, 4,604 D4-invariant entries of total 2624862500021/125000000000, with capture threshold q = 249987/250000 over every closed unit square in [0,5]^2, so that 21q exceeds the total by 999979/125000000000.

    The capture statement is decided by the source's own exact rational replay of a retained certificate tree over 5,000 root boxes, and Lean proves minSide 21 = 5 from that one hypothesis.

    That replay was run here in full on 29 September 2026, the source's runner unchanged: every stage passed, and its records match the source's M1 run, 45,436 of the 45,446 output files byte for byte and the rest in every certified quantity. The Lean overlay was not built here.

    Hosono after Daniel, square-packing-bounds. The source names Daniel's mixed-cover proof (T-052) as first, claims no priority, and says its code was developed with Codex.
    Significance
    A second, point-only route to a value T-052 already holds, with a positive-margin threshold rather than a zero-margin cover and a Lean reduction of its own. A citable detail that changes no theorem. Confirmed on 11 October beside T-054.
    Novelty
    previously-published Present in an identified source
    Records

    n = 21registerevidence 1evidence 2evidence 3sourcereview

  • 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-081 V0 C1 Daniel after Burns, Massaccesi · 2026-10-03 · 14 cases

    s(k2−4)=k for every integer k from 5 up; k=5…18 are the cases held here

  • T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤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-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 16 of the retained witness (witness id 17) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 5 of its 21 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(21) — solved

s(21)=5. Established by a mixed cover with two exhaustive checks of its covering condition, Daniel (2026), building on Burns’s and Massaccesi’s weighted exact-rational covering method. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction. With s(32)=6 it is the second exact value this record holds for a case of the form k2−4 with k≥4, as the source says; s(45)=7, registered with it, is the third.

The packing

The upper bound is trivial: the 5×5 grid holds 25 unit squares, so it holds 21 with four cells empty, and s(21)≤5. The record catalogue does not picture n=21, and no arrangement below side 5 has ever been found. What is new is that none exists.

The lower bound

The certificate is a mixed cover: 7,536 rationally weighted points of [0,5]2 plus mass spread uniformly along 1,872 segments of length 1/50 on the interior grid lines x,y∈{1,2,3,4}, total 522368729933/(25·109)=20.894749197<21, exactly invariant under the square’s eight symmetries, such that every closed unit square inside [0,5]2, at every centre and every angle, captures mass at least 1, a point on its boundary counting and a segment along one of its edges counting in full. If 21 unit squares fit in a side s<5, scaling by 5/s gives 21 squares of side above 1 with disjoint interiors in [0,5]2, each strictly containing a concentric closed unit square. Those 21 closed unit squares are pairwise disjoint, so they would capture at least 21 from a total of 20.89.

The margin is exactly zero, and the line mass is what makes that possible: the 25 grid tiles each capture at least 1 by sharing edge mass, so a total below 21 at the integer side needs a closed square to count a segment along its edge in full. A square seated on a cell collects its whole boundary’s line mass, and a slightly tilted one loses part of an edge on one line and gains the complementary part on the parallel line one unit away. No angle net can decide such a cover; the source subdivides pose space instead, with two separately written checkers that share no code. zm_mixed.py, in exact rational arithmetic, certifies all 40,000 root boxes of the cover’s D4 fundamental region (461,204 boxes, 12.9 CPU-hours) with no uncertified leaf. The Rust zmx2 decides points and masses in integers and encloses where a grid line crosses the rotated square’s edges in binary64 intervals widened outward; it certifies all 2,500 roots of the same region and, assuming no symmetry, all 20,000 roots of the whole pose space. A Lean theorem, s21_eq_five_of_checker, derives minSide 21 = 5 from the single hypothesis S21CheckerCover, the statement both checkers’ D4 runs certify; the reduction, the D4 fold, the cover’s total and its invariance are kernel-checked, and the checker programs are not formalised.

The verified field rests on a complete replay here of zmx2 (E-n021-evand-mixed-cover-zmx2-replay, V3/C3). Built from the retained source with rustc 1.94.1, it certified all 2,500 D4 roots (1,826,222 boxes) and all 20,000 unreduced roots (14,709,448 boxes) on 28 and 29 September with no uncertified box, every root carrying the census of the source’s record of the same root, and the bundle’s own fast tier passed too; the receipts are in the packet. That replay is interval-certified, so it assumes correctly rounded binary64 arithmetic on the host. The exact checker was sampled here, 32 roots matching the source’s records box for box, and its complete re-sweep runs separately; recorded as a second, exact-algebraic replay, it would give this value a second machine method beside its C3. The review of 28 September re-derived both checkers’ lemmas against their code and found no mathematical defect. The Lean build was not run here, because Mathlib’s build cache is unreachable from this session.

Hosono published a second, point-only route to the same value on 28 September: Daniel’s earlier point support scaled to side 5 and re-weighted, with a capture threshold 249987/250000 below 1, decided by the source’s own exact rational replay, and a Lean reduction of everything but that replay. It claims no priority, and it is recorded as reported evidence (E-n021-wand125-point-endpoint-report). Its complete replay ran here on 29 September with the source’s runner unchanged, and its records match the source’s M1 run (E-n021-wand125-point-endpoint-source-replay, T-055), so the value has a second, point-only route; the verified field keeps Daniel’s, which came first. Hosono’s README says parts of the work were produced with AI assistance under human direction, and its s(21) write-up says “Code developed with Codex requires human and independent review”.

Earlier lower bounds

The previous verified bound, from 27 September, was the same author’s 5000/1001=4.995004995: 4,604 rationally weighted points in [0,5000/1001]2, total weight 260057/12500=20.80456<21, decided over a rational angle net at N=6000 and replayed here (E-n021-evand-5000-1001-source-replay). It remains valid evidence. A net cannot reach side 5 itself: the per-bin shrink costs about 2/N, which must stay below the margin, and at margin zero there is none. The certificate entered the source on 2026-09-23.

Before it, the verified bound was this repository’s T-034 certificate at side 122/25=4.88, of 2026-09-23: 1228 rationally weighted atoms on a D4-symmetric site set, total mass 5036431/250000=20.145724<21, and least covered mass 250001/250000. An exact event-cell sweep and an interval branch and bound independently decide its conditions from the retained bytes and agree on that least mass, and a review re-decided the same bytes by three routes and accepted them. Only Condition 2 mentions n among the five certificate conditions, so that atom set certifies its side for every integer above its mass, which is 21 and upward. This repository’s generator fixes the shrunken side at B=9977/10000, so a certificate of its shape cannot exist above 4.9885 here; that ceiling belongs to the generator’s settings, not to the weighted-point method.

Before that, the verified bound was 97/20=4.85, from the T-021 certificate: 1680 atoms of total mass 19848723/1000000=19.848723, which certifies n=20 and n=21 alike and remains the verified n=20 bound. The earlier T-020 certificate at 24/5 remains valid and still supplies the verified n=19 bound.

Hosono’s rectangle-density certificates reached 997/200=4.985 on 2026-09-26 and 399/80=4.9875 on 2026-09-28; both lie below Daniel’s 5000/1001, and they are recorded with that source’s other bounds. The DS7 survey’s Table 2 gives the decimal 4.7438 for this case, credited to Friedman, without an exact identity or a rounding guarantee; it is kept as opaque reported evidence. Corrected 2 October 2026: Nagamochi’s Lemma 1 is false (Karakuş 2026), so his closed form below is now a reported bound whose published proof is incomplete (review). This register had recorded that proof as verified, its own error, logged as defect D-516. Nagamochi’s general closed form, which applies to every N≥4, gives 1+14:

s(N)≥min{⌈N⌉,N−2⌊N⌋+1+1}

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-n021-evand-mixed-cover-zmx2-replay replayed here producer’s code V-evand-zmx2 (external); V-audit-evand-mixed-covers (first-party, premises)
verified upper E-basic-grid-upper replayed here independent V-check-basic-bounds (first-party)