T-094: Mixed rectangle-measure lower bounds verified at n=67 and 84

V3 C3 lower bound confirmed

2026-10-05 published · wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · n=67,84

Two rectangle densities of wand125/square-packing-bounds, checked at coverage one and published on 5 October 2026, prove s(67)≥212/25 = 8.48 and s(84)≥9411/1000 = 9.411.

Each is a density of uniform rectangles in D4 orbits, 536 at n=67 and 686 at 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 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.

Significance, composition and next rung
Significance
The strongest verified lower bounds on record at 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.
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.
Novelty
previously-published Present in an identified source

The cases

Case record

n=67

8.488.707
8910
8.1859.185
nn+1

Proven

8.48000≤s(67)≤8.707107

  • exact

Citation record n-067

lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-094)

upperStenlund 1980, Squares in Squares

Open

  • optimality

The case record

LowerUpper
Gap22−1225≈ 0.22710678…
Case record

n=84

9.419.698
91011
9.16510.165
nn+1

Proven

9.41100≤s(84)≤9.698053

  • exact

Citation record n-084

lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-094)

upperry-xu 2026, GitHub (confirmed T-125)

Open

  • optimality

The case record

Results on these cases

12 results in the register on n=67,84, oldest first, each with what it established and how it stands now.

  1. 2005 published T-007 · n=67,84

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

    V0 C1 lower bound incomplete on these cases, superseded by T-094

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-09-04 published T-085 · n=67,84

    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 · n=67

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

    V0 C0 lower bound recorded superseded by T-094

    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-070 · n=67

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

    V3 C3 lower bound confirmed superseded by T-094

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

  5. 2026-09-29 published T-058 · n=67,84

    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=67,84

    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-094

    Karakuş · Karakuş 2026 · source · register

  7. 2026-10-02 published T-071 · n=84

    Mixed rectangle-measure lower bounds replayed at n=84…87

    V3 C3 lower bound confirmed superseded by T-094

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-02 · packet · source · review · register

  8. 2026-10-04 published T-090 · n=67,84

    Mixed rectangle-measure lower bounds verified at 17 counts in n=42…96

    V3 C3 lower bound confirmed on these cases, superseded by T-094

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-04 · packet · source · review · register

  9. 2026-10-05 published T-094 this result · n=67,84

    Mixed rectangle-measure lower bounds verified at n=67 and 84

    V3 C3 lower bound confirmed

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-05 · packet · source · review · register

  10. 2026-10-08 published T-125 · n=84

    Complete rational construction reports at 25 counts

    V3 C3 upper bound confirmed

    ry-xu · ry-xu square packing 2026 · packet · register

  11. 2026-10-08 published T-130 · n=84

    Five follow-up rational refinements from Francisco Couzo

    V3 C3 upper bound confirmed

    Couzo after Xu, Daniel, Ellsworth, Levy · Couzo follow-up refinements 2026-10-08 · packet · register

  12. 2026-10-09 published T-138 · n=84

    Exact witnesses at Mishapolk's printed ceilings, the smallest known at 103 and 258 when registered

    V3 C3 upper bound confirmed

    Mishapolk after Stenlund, Friedman, Ellsworth, Chaoweeraprasit, Couzo, Xu, Levy · Mishapolk decimal poses 2026-10-09 · packet · register