Bounds

Results in the register

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

  \(s(n) \ge \min(\lceil\sqrt{n}\rceil, \sqrt{n - 2\lfloor\sqrt{n}\rfloor + 1} + 1)\)$s(n)\ge min(\lceil \sqrt{n}\rceil ,\sqrt{n-2\lfloor \sqrt{n}\rfloor +1}+1)$ for \(4 \le n \le 324\)$4\le n\le 324$

• T-045 S3 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 15 cases

  Rectangle-density lower bounds replayed at 15 counts in \(n = 18\ldots78\)$n=18\dots 78$

• T-046 S3 V0 C0 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · 48 cases

  Rectangle-density lower bounds reported for 48 counts in \(n = 18\ldots95\)$n=18\dots 95$

• T-058 S2 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases

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

• T-064 S4 V3 C3 Daniel after Burns, Massaccesi · 2026-10-01 · 13 cases

  \(s(k^2 - 3) = k\)$s(k^2-3)=k$ for every integer \(k\)$k$ from 6 up; \(k = 6\ldots18\)$k=6\dots 18$ are the cases held here

• T-067 S3 V3 C3 wand125 after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-01 · n = 77, 78

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

  Claim and records

  Claim

  \(s(77) = 9\)$s(77)=9$: the lower half by wand125's mixed cover of 1 October 2026, the upper half by the \(9 \times 9\)$9\times 9$ grid. The cover's total is below 78 too, so it gives \(s(78) = 9\)$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\)$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)\)$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.

  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\)$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\)$n=77$ alone, since T-064 registers \(s(78) = 9\)$s(78)=9$ (result-import.md, register table); it took in \(n = 78\)$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\)$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.

  Significance

  An exact value for a case that was open, and a second route to \(s(78) = 9\)$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)\)$s(59)$ and \(s(77)\)$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.

  Novelty

  previously-published Present in an identified source

  Records

  n = 77n = 78registerevidence 1evidence 2evidence 3sourcereview

  n = 77n = 78registerevidence 1evidence 2evidence 3sourcereview

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

  \(s(n) \ge 1/2 + \sqrt{n - \lfloor\sqrt{n}\rfloor + 1/4}\)$s(n)\ge 1/2+\sqrt{n-\lfloor \sqrt{n}\rfloor +1/4}$ for every nonsquare \(8 \le n \le 324\)$8\le n\le 324$

• T-085 S3 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases

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

In the frontier survey On GitHub