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

2026-10-06 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 6 October 2026, proves s(18)≥588/125 = 4.704.

The certificate is a density of 209 uniform rectangles in D4 orbits, and no point mass, of total mass 1799999/100000, on a net it declares itself: core side 1999/2000 and 832 half-angle tangents of step 1/2006, finer than the 416 of step 1/1001 at core 999/1000 that T-096's certificate declares. Since 1999/2000 (1 + 1/2006) = 4011993/4012000 < 1, and the last tangent 831/2006 is past tan(pi/8), every unit square contains a concentric core of side 1999/2000 at a net angle strictly in its interior.

The source reports every such core capturing mass at least one: at all 831 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-096's certificate changed only to allow more workers, and at the axis by exact integer tables.

The value is above T-096's 47/10, the source's earlier certificate and the reported and verified lower bound at n=18 before it, by 0.004, and supersedes it.

The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 832 directions of the net the candidate declares, and two mutants 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 6 October review of the certificate re-derived the 832-node net in exact arithmetic and found no defect. The source's own checker was also replayed here in full, the bundle's own driver over all 832 nodes with its assertions on, each returning the certificate's own record: confirmed, reproduced with the producer's code.

wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 6 October 2026 on jlevy/squares#366. 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 bound on record at n=18, by 0.004 above T-096, and the strongest reported. The certificate kind and checker of T-069 and later on a net twice as fine as T-096's, a parameter choice the same driver reads from the candidate; no new technique, at S3 as T-096, T-074 and T-045 are. The 6 October review confirmed the draft.
Composition
One primary certificate on its reported entry and its replay entry. The replay is sqverify-fast at all 832 directions of the net the retained candidate declares: one interval-certified method, replayed here by an independent implementation, C3, on the census route, whose per-certificate conditions for a declared net the soundness review of the declared-net change set and this certificate meets. Beside it, the bundle's own driver replayed the source's checker over all 832 nodes, the axis tables among them, each returning the shipped record: a complete reproduction with the producer's code, not a second method.
Next rung
V4 and C4 need two adversarial AI reviews of this result by distinct reviewers and a human oversight record. One is retained, the review of 6 October that read the certificate. A second machine method would be a method-distinct decision of rotated coverage; the complete replay of the source's own checker already stands beside the rung (E-n018-wand125-mixed-4704-source-replay).
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

    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 this result

    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