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-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-071 S3 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-02 · n = 84–87

  Mixed rectangle-measure lower bounds replayed at \(n = 84\ldots87\)$n=84\dots 87$

  Claim and records

  Claim

  Two rectangle densities of wand125/square-packing-bounds, checked at coverage one and published on 2 October 2026, prove \(s(84) \ge 47/5\)$s(84)\ge 47/5$ = 9.4 and \(s(85) \ge 471/50\)$s(85)\ge 471/50$ = 9.42. The \(n = 85\)$n=85$ certificate's mass is below 86 and 87 too, so it gives \(s(86) \ge 471/50\)$s(86)\ge 471/50$ and \(s(87) \ge 471/50\)$s(87)\ge 471/50$ as well: four counts in all.
  
  Each certificate is a density of uniform rectangles with no point mass, of total mass n - 1/100000, at core side 9977/10000 on 201 net half-angles of step 83/40000: 661 rectangles at \(n = 84\)$n=84$ and 587 at \(n = 85\)$n=85$. Each is accepted at every oblique net angle by code/mixed_rotated_verify.cpp, the research copy of Tokoharu's verify.cpp that the source's \(s(50)\)$s(50)$ certificate (T-048) and the five certificates of T-069 use, which accepts coverage at least 1 where Tokoharu's requires 10001/10000, and at angle zero by exact integer tables. The least oblique lower bounds are 1.00000000089 at \(n = 84\)$n=84$ and 1.0000000017 at \(n = 85\)$n=85$.
  
  Both values exceed Green's reported 2 sqrt(2) + (247 + 12 sqrt(2))/41 = 9.2667335..., which this record holds at both counts by monotonicity from \(n = 82\)$n=82$, by more than 0.1332 and 0.1532; the source's own improvement figures are measured from 9.2667, below Green's value, and are not lower bounds. At \(n = 86\)$n=86$ and 87 the \(n = 85\)$n=85$ value is also above the rectangle certificates T-068 reports there, 1873/200 and 941/100.
  
  Each certificate passed a complete replay here on 2 October 2026 of the source's unchanged checker and per-angle functions on its pinned tarball: all 201 directions, each returning the certificate's own record. The replays run the source's own algorithm and are not an independent decision of coverage.
  
  wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 2 October 2026 on jlevy/squares#282. The source says parts of the work were produced with AI assistance under human direction.

  Composition

  Two primary certificates, each on its own reported entry and its own replay entry. \(n = 86\)$n=86$ and 87 take the \(n = 85\)$n=85$ certificate directly, its mass being below those counts, so no step is added. Each replay runs the source's C++ checker unchanged: one interval-certified method, replayed here, C3. Coverage is decided by that checker alone; the axis tables are a second implementation for one direction and not a second method.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A second machine method would be a method-distinct decision of rotated coverage; the replays here run the source's own checker. The checker's controls were made on the \(n = 37\)$n=37$ certificate of the same kind.

  Significance

  Raised the verified lower bound at four counts, \(n = 84\)$n=84$ to 87, past Green's reported value at \(n = 84\)$n=84$ and 85 by the widest margins over it on record, by the certificate kind of T-048 and T-069. Further sizes from one generator at S3; the 2 October review of these certificates proposed S3, which the replays leave standing.

  Novelty

  previously-published Present in an identified source

  Records

  n = 84n = 85n = 86n = 87registerevidence 1evidence 2evidence 3evidence 4sourcereview

  n = 84n = 85n = 86n = 87registerevidence 1evidence 2evidence 3evidence 4sourcereview

• 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$

• T-090 S3 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-05 · 17 cases

  Mixed rectangle-measure lower bounds verified at 17 counts in \(n = 42\ldots96\)$n=42\dots 96$

• T-094 S3 V3 C3 wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-10-05 · n = 67, 84

  Mixed rectangle-measure lower bounds verified at \(n = 67\)$n=67$ and \(84\)$84$

  Claim and records

  Claim

  Two rectangle densities of wand125/square-packing-bounds, checked at coverage one and published on 5 October 2026, prove \(s(67) \ge 212/25\)$s(67)\ge 212/25$ = 8.48 and \(s(84) \ge 9411/1000\)$s(84)\ge 9411/1000$ = 9.411.
  
  Each is a density of uniform rectangles in D4 orbits, 536 at \(n = 67\)$n=67$ and 686 at \(n = 84\)$n=84$, and no point mass, of total mass n - 1/100000, at core side 9977/10000 on 201 net half-angles of step 83/40000, of the kind and checker of T-082, T-090 and T-091. The source reports each accepted at all 200 oblique net angles by code/mixed_rotated_verify.cpp, its research copy of Tokoharu's verify.cpp at coverage threshold one, and at the axis by exact integer tables. Both supersede the source's certificates of T-090 at the same count, mixed_n67_L8475 and mixed_n84_L94075.
  
  Both values are above what the record held at their counts: the verified 1691/200 and 47/5, by 0.025 and 0.011, and T-090's reported 339/40 and 3763/400, by 0.005 and 0.0035. A packing of n + 1 squares contains one of n, but at \(n = 68\)$n=68$ and 85 the record already holds more in both lanes (851/100 and 473/50), so neither carries further.
  
  Each certificate was decided here on 5 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 201 net directions of the retained candidate, and two mutants of each scaled below coverage one were refused: confirmed, independently re-implemented. The verifier shares no code with the source's checker and runs the same net-and-shrink method, so it is a second implementation and not a second method. The source's own checker was not run here.
  
  wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in two comments of 5 October 2026 on jlevy/squares#282. The source says parts of the work were produced with AI assistance under human direction.

  Composition

  Two primary certificates, each on its own reported entry and its own replay entry. Each replay is sqverify-fast at all 201 net directions of the retained candidate: one interval-certified method, replayed here by an independent implementation, C3. The source's checker and axis tables were not run here, so no second method and no reproduction with the producer's code stands beside it.

  Next rung

  V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A replay of the source's own checker, devtools.audit_wand125_point_and_mixed mixed-shard wand125-mixed-bounds-2026-10-05 --runners 2 (about 26.5 CPU-hours planned), would add a reproduction with the producer's code beside the rung; a second machine method would be a method-distinct decision of rotated coverage.

  Significance

  The strongest verified lower bounds on record at \(n = 67\)$n=67$ and 84, above the replayed rectangle and mixed certificates that held them by 0.025 and 0.011. Further sizes from the generator and checker of T-069, T-071, T-072, T-075, T-082, T-090 and T-091, with no new technique, at S3 as those are. The review of 5 October confirmed S3: that they are the source's first certificates verified here by an independently re-implemented replay is a fact about this repository's confirmation, not about the result.

  Novelty

  previously-published Present in an identified source

  Records

  n = 67n = 84registerevidence 1evidence 2evidence 3evidence 4sourcereview

  n = 67n = 84registerevidence 1evidence 2evidence 3evidence 4sourcereview

In the frontier survey On GitHub