T-062: s(60)=8, by a mixed cover of points and grid-line segments

V3 C3 optimality confirmed

2026-09-28 published · Daniel after Burns, Massaccesi · n=60

s(60)=8: the lower half by Evan Daniel's mixed cover of 28 September 2026, the upper half by the 8×8 grid.

The cover is 23,744 weighted points of [0,8]^2 plus mass spread uniformly along 5,216 segments of length 1/50 on the interior grid lines, total 748233441/12500000 = 59.85867528 < 60, exactly D4-invariant. Every closed unit square in [0,8]^2 captures mass at least one, a boundary point and a segment along an edge counting in full, so a packing of 60 at side s below 8, its centres scaled by 8/s, would give 60 pairwise disjoint closed unit squares in [0,8]^2 capturing at least 60.

The source certifies that at margin zero with two separately written checkers: zm_mixed.py in exact rational arithmetic over 102,400 root boxes, and the Rust zmx2 with outward-rounded binary64 enclosures over 6,400 symmetry-reduced roots and 51,200 unreduced ones, none uncertified. It has no Lean theorem for this cover.

zmx2 was replayed here in full on 2 October 2026, over all 6,400 D4 roots and all 51,200 unreduced roots, every root's census equal to the source's; zm_mixed.py was not run. wand125's s(59)=8 (T-066), replayed here the same day with the same checker, gives this value a second route by monotonicity.

Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method. Registration was requested in jlevy/squares#256. The source's CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.

Significance, composition and next rung
Significance
An exact value for a case that was open, by the line-cover recipe of T-052 and T-053 carried to side 8, adding no technique: a substantive case result, S3. The 2 October review of the geometric premises confirmed the draft, and noted that the family argument that lifted T-053 to S4 applies here exactly as there, so the two should carry one score; which one is the rescoring pass's (think-qh3s).
Composition
Compound, and the minimum is set by the lower half. The lower half is E-n060-evand-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic). As for T-052 and T-053, the two machine entries certify different halves; the lower half stands on one replayed method, and the equality is C3. The second route, T-066's s(59) cover, was made from this cover and decided by the same zmx2, so it adds a certificate and not a method.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review, of the geometric premises, is retained. A complete zm_mixed.py sweep, about 20 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method (think-mx3k); the shared author, agent and pose-space architecture stay the residual common-mode risk. V5 would need a Lean data file and top theorem for this cover, which the source has not attempted, and a human expert's review of the formalization.
Novelty
previously-published Present in an identified source

The case

Case record

n=60

8
789
7.7468.746
nn+1

Proven

s(60)=8

  • optimal
  • exact

Citation record n-060

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

The case record

LowerUpper
Verified88
Reported88
Gap0 solved: the verified bounds meet

Results on the case

9 results in the register on n=60, 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-062

    Nagamochi · Nagamochi 2005 · source · register

  2. 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

  3. 2026-09-27 published T-046

    Rectangle-density lower bounds reported for 48 counts in n=18…95

    V0 C0 lower bound recorded superseded by T-062

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register

  4. 2026-09-28 published T-062 this result

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

    V3 C3 optimality confirmed

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

  5. 2026-09-28 published T-070

    Rectangle-density lower bounds replayed at 25 counts in n=29…95

    V3 C3 lower bound confirmed superseded by T-062

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register

  6. 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

  7. 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-062

    Karakuş · Karakuş 2026 · source · register

  8. 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

  9. 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