T-067: s(77)=9, by a mixed cover extended from Daniel's s(60) cover

V3 C3 optimality confirmed

2026-10-01 published · wand125 after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · n=77,78

s(77)=9: the lower half by wand125's mixed cover of 1 October 2026, the upper half by the 9×9 grid. The cover's total is below 78 too, so it gives s(78)=9 as well, a second route to the k = 9 case of the family Evan Daniel reports (T-064).

The cover is 28,273 weighted points of [0,9]^2 plus mass spread uniformly along 6,420 segments, total 43347137744028965/2^49 = 76.999984600031... < 77, exactly D4-invariant, in Evan Daniel's mixed format. It is Daniel's s(60)=8 cover cut at 4 in both coordinates with a central band inserted, plus a symmetric band measure of mass about 16.43 found by a linear program, the whole scaled to just below 77. Eighty-four points that lay on loaded grid lines were replaced by segments of length 2/1000 on the same lines, which the source says its exact checker needs. Every closed unit square in [0,9]^2 captures mass at least one, so a packing of 77 at side below 9, scaled up to side 9, would capture at least 77.

The source reports the cover accepted by Daniel's checkers: zmx2 over 8,100 symmetry-reduced roots and over 64,800 unreduced ones, and zm_mixed.py in exact rational arithmetic over 129,600 roots, none uncertified. It has no Lean statement.

zmx2 was replayed here in full on 2 October 2026, with --pair-points as the source ran it: all 8,100 D4 roots in one run and all 64,800 unreduced roots in two region runs read as one record, none uncertified, with the box totals the source states. Its run records are not published, so no root-for-root comparison was possible. The source's own verification script cannot pass as published, because its checksum file lists run logs that are not in the repository, so its two zmx2 steps were run here as this repository's own sequence.

wand125, square-packing-bounds, building directly on Evan Daniel's s(60) cover, format and checkers. Registration was requested in jlevy/squares#279. The source says parts of the work were produced with AI assistance under human direction.

Significance, composition and next rung
Significance
An exact value for a case that was open, and a second route to s(78)=9: a substantive case result at S3, set beside T-062, whose cover it extends. The 2 October review of the s(59) and s(77) covers confirmed the draft: the band insertion that carries a side-8 cover to side 9 is the one new idea, and at one instance it is a case result, not yet a technique.
Composition
Compound, and the minimum is set by the lower half. The lower half is E-n077-wand125-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic); the equality is C3, as T-066 reads its own. The checker is Daniel's, which also decides T-062 and T-066. The zm_mixed.py sweep the source reports is not replayed here, and sets nothing.

n=78 takes the same certificate directly, its total being below 78, so no step is added. At registration this entry's scope was n=77 alone, since T-064 registers s(78)=9 (result-import.md, register table); it took in n=78 at stage 4, on 2 October 2026, because the verified bound there rested on this replay alone, T-064's own route being unreplayed until its Valid7 replay and Lean build passed here on 2 and 3 October. The verified bound at n=78 still cites this replay alone. T-064 keeps its claim, which names this route.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. The source's zm_mixed.py sweep, about 94 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method (think-mx3k). V5 would need a Lean statement for this cover and a human expert's review of the formalization.
Novelty
previously-published Present in an identified source

The cases

Case record

n=77

9
8910
8.7759.775
nn+1

Proven

s(77)=9

  • optimal
  • exact

Citation record n-077

lowerwand125 after Daniel, Levy et al. 2026, GitHub (confirmed T-067)

The case record

LowerUpper
Verified99
Reported99
Gap0 solved: the verified bounds meet
Case record

n=78

9
8910
8.8329.832
nn+1

Proven

s(78)=9

  • optimal
  • exact

Citation record n-078

lowerwand125 after Daniel, Levy et al. 2026, GitHub (confirmed T-067)

The case record

LowerUpper
Verified99
Reported99
Gap0 solved: the verified bounds meet

Results on these cases

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

  1. 2005 published T-007 · n=77,78

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

    V0 C1 lower bound incomplete on these cases, superseded by T-064 and T-067

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-09-04 published T-085 · n=77,78

    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-045 · n=77,78

    Rectangle-density lower bounds replayed at 15 counts in n=18…78

    V3 C3 lower bound confirmed superseded by T-064 and T-067

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

  4. 2026-09-27 published T-046 · n=77,78

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

    V0 C0 lower bound recorded superseded by T-064 and T-067

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

  5. 2026-09-29 published T-058 · n=77,78

    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

  6. 2026-09-29 published T-083 · n=77,78

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

    V3 C3 lower bound confirmed on these cases, superseded by T-064 and T-067

    Karakuş · Karakuş 2026 · source · register

  7. 2026-09-30 published T-064 · n=78

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

    V3 C3 optimality confirmed on these cases, current best, reported

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

  8. 2026-10-01 published T-067 this result · n=77,78

    s(77)=9, by a mixed cover extended from Daniel's s(60) cover

    V3 C3 optimality confirmed

    wand125 after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register

  9. 2026-10-03 published T-081 · n=77

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

    V0 C1 optimality reviewed on these cases, second certificate, reported

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

  10. 2026-10-07 published T-124 · n=77,78

    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