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

V3 C3 optimality confirmed

2026-09-27 published · Daniel after Burns, Massaccesi · n=21

s(21)=5: the lower half by Evan 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.

Evan 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, composition and next rung
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.
Composition
Compound: the lower half is E-n021-evand-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic). The two machine entries differ in method, but they certify different halves; the lower half, which sets the minimum, stands on one replayed method, and the equality is C3, as T-008 reads its own halves.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A complete zm_mixed.py re-sweep, about 12.9 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method; the shared pose-space architecture stays the residual common-mode risk. V5 would need the checker statement S21CheckerCover proved in Lean and a human expert's review of the formalization; the reduction s21_eq_five_of_checker, from that statement to s(21)=5, was kernel-checked here on 2026-09-30 with the standard axioms only (the 2026-09-28 packet's receipts/lean/).
Novelty
previously-published Present in an identified source

The case

Case record

n=21

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)

The case record

LowerUpper
Verified55
Reported55
Gap0 solved: the verified bounds meet

Results on the case

12 results in the register on n=21, oldest first, each with what it established and how it stands now.

  1. 2005 published T-007

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

    V0 C1 lower bound incomplete on this case, superseded by T-052

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-09-04 established T-020

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

    V3 C3 lower bound confirmed superseded by T-052

    Levy after Burns, Massaccesi · register

  3. 2026-09-04 published T-085

    Nagamochi 2005, Lemma 1 is false for every container with a>3 and b>2

    V3 C3 correction confirmed

    Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

  4. 2026-09-05 established T-021

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

    V3 C3 lower bound confirmed superseded by T-052

    Levy after Burns, Massaccesi · register

  5. 2026-09-23 established T-034

    s(21)≥122/25=4.88

    V3 C3 lower bound confirmed superseded by T-052

    Levy after Burns, Massaccesi · register

  6. 2026-09-23 published T-050

    s(21)≥5000/1001=4.995004995…

    V3 C3 lower bound confirmed superseded by T-052

    Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · source · review · register

  7. 2026-09-27 published T-052 this result

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

    V3 C3 optimality confirmed

    Daniel after Burns, Massaccesi · evand square-packing 2026-09-28 · packet · source · review · register

  8. 2026-09-28 published T-055

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

    V3 C3 simplification confirmed

    wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point and mixed bounds 2026-09-28 · packet · source · review · register

  9. 2026-09-29 published T-058

    Rectangle-certificate ceiling α·UB(n) proved for n=1..100; B·UB(n) on 64 grid rows

    V3 C3 method limit confirmed

    wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register

  10. 2026-09-29 published T-083

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤324

    V3 C3 lower bound confirmed on this case, superseded by T-052

    Karakuş · Karakuş 2026 · source · register

  11. 2026-10-03 published T-081

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

    V0 C1 optimality reviewed on this case, second certificate, reported

    Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register

  12. 2026-10-07 published T-124

    Reported non-strict local minima for 178 source configurations

    V0 C0 restricted optimality recorded

    Daniel after Couzo · Daniel exact and local reports 2026 · packet · register