T-096: Mixed rectangle-measure lower bound replayed at n=18, on a net the certificate declares

V3 C3 lower bound confirmed superseded by T-102

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

A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 5 October 2026, proves s(18)≥47/10 = 4.7.

The certificate is a density of 136 uniform rectangles in D4 orbits, and no point mass, of total mass 1799999/100000, on a net it declares itself: core side 999/1000 and 416 half-angle tangents of step 1/1001. The source's earlier mixed certificates, from T-069 on, use core side 9977/10000 on 201 tangents of step 83/40000. Since 999/1000 (1 + 1/1001) = 500499/500500 < 1, every unit square contains a concentric core of side 999/1000 at a net angle strictly in its interior. The source reports every such core capturing mass at least one: at all 415 oblique net angles by code/mixed_rotated_verify.cpp, its research copy of Tokoharu's verify.cpp at coverage threshold one, run by the same driver as T-069's certificates, and at the axis by exact integer tables.

The value is above the 939/200 = 4.695 of the source's rectangle certificate rect_n18_L4695 (T-045), the reported and verified lower bound at n=18, by 0.005. Its mass is below 19 too, but the record holds more there.

The certificate passed a complete replay here on 5 October 2026 of the bundle's own driver and the source's unchanged checker on the pinned tarball: all 416 net nodes, each regenerated record equal to the certificate's own. The replay runs the source's own algorithm and is not an independent decision of coverage. Its exact premises, those of the declared net among them, were recomputed here, every shipped record and input was bound to the declared net and the expanded candidate, and the 5 October review found no defect. This repository's clean-room verifier sqverify-fast, extended to read a declared net, also decided all 416 directions here, a second implementation that is not yet a registered verifier and on which no rung rests.

wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in jlevy/squares#366. The source says parts of the work were produced with AI assistance under human direction.

Significance, composition and next rung
Significance
Raised the verified lower bound at n=18 by 0.005, to within 0.123 of Hämäläinen's packing, by the certificate kind and checker of T-069 and later on a finer net that the same driver reads from the candidate: a parameter choice within the framework, no new technique, at S3 as those are. The 5 October review confirmed the draft.
Composition
One claim on one certificate, on its own reported entry and its own replay entry. E-n018-wand125-mixed-470-source-replay replays it in full with the bundle's own driver and the source's checker: one interval-certified method, reproduced with the producer's code, C3. Coverage is decided by the source's C++ checker alone, byte for byte the checker the 28 September and 2, 3 and 5 October reviews read; 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 replay here runs the source's own checker. The checker's controls were made on the n=37 certificate of the same kind. A sqverify-fast evidence entry (think-3ok2) would show beside the rung as independently re-implemented.
Novelty
previously-published Present in an identified source

The case

Case record

n=18

4.704.823
456
4.2435.243
nn+1

Proven

4.70500≤s(18)≤4.822876

  • exact

Citation record n-018

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

upperHämäläinen 1980, Squares in Squares

Open

  • optimality

The case record

LowerUpper
Gap72−241200≈ 0.11787565…

Results on the case

17 results in the register on n=18, 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-102

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-08-21 published T-016

    s(n)≥22529/5000 for n=18,19, by monotonicity from T-015

    V3 C3 lower bound confirmed superseded by T-102

    Massaccesi after Burns · Burns–Massaccesi n17 · packet · register

  3. 2026-08-31 established T-002

    s(18)≥4426213/1000000, by monotonicity from T-001

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Bentz · register

  4. 2026-08-31 established T-003

    The sixteen-point set's unavoidability ceiling lies in [4426213/1000000,4427/1000)

    V3 C3 method limit confirmed

    Levy after Bentz · register

  5. 2026-09-04 established T-019

    s(n)≥459/100=4.59 for n=17,18,19

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Burns, Massaccesi · register

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

  7. 2026-09-18 established T-027

    s(18)≥467/100=4.67

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Burns, Massaccesi · register

  8. 2026-09-19 established T-028

    s(18)≥187/40=4.675

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Burns, Massaccesi · register

  9. 2026-09-19 established T-029

    s(18)≥1871/400=4.6775

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Burns, Massaccesi · register

  10. 2026-09-19 established T-030

    s(18)≥4679/1000=4.679

    V3 C3 lower bound confirmed superseded by T-102

    Levy after Burns, Massaccesi · register

  11. 2026-09-27 published T-045

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

    V3 C3 lower bound confirmed superseded by T-102

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

  12. 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-102

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

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

  14. 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-102

    Karakuş · Karakuş 2026 · source · register

  15. 2026-10-05 published T-096 this result

    Mixed rectangle-measure lower bound replayed at n=18, on a net the certificate declares

    V3 C3 lower bound confirmed superseded by T-102

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

  16. 2026-10-06 published T-099

    Mixed rectangle-measure lower bound verified at n=18, on a finer declared net

    V3 C3 lower bound confirmed superseded by T-102

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds finer net 2026-10-06 · packet · source 1 · source 2 · review · register

  17. 2026-10-06 published T-102

    Mixed rectangle-measure lower bound verified at n=18, on the finest declared net yet

    V3 C3 lower bound confirmed

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