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

V3 C3 simplification confirmed

2026-09-28 published · wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · n=21

s(21)=5 by a second, point-only route: the lower half by wand125'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 Evan 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.

wand125 after Evan 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, composition and next rung
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.
Composition
Compound, and the minimum is set by the lower half. The lower half is E-n021-wand125-point-endpoint-source-replay (exact-algebraic, the source's runner replayed here), the upper half the grid (E-basic-grid-upper); the equality is C3. The runner is the source's, so the replay, reproduced with the producer's code, confirms the source's run rather than adding a second method, and the Lean reduction, not built here, adds nothing to the rung.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A build of the Lean overlay with its axiom receipt, and the runner's lemmas formalised (review F10), would be the road to rung 5. The controls end at the first root box that holds a pose, so neither exercises the sieve or frontier stages; a control refused deeper in the tree would test more of the runner.
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

    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 this result

    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