T-100: Mixed rectangle-measure lower bound verified at , past the best 18-square packing
V3 C3 lower bound confirmed superseded by T-103
A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 6 October 2026, proves = 4.8229.
The certificate is a density of 313 uniform rectangles in D4 orbits, and no point mass, of total mass 1899999/100000, on the net T-096's certificate declares: core side 999/1000 and 416 half-angle tangents of step 1/1001, with 999/1000 (1 + 1/1001) = 500499/500500 < 1. The source reports every core at a net angle 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-096's certificate, and at the axis by exact integer tables.
The value is above the 1927/400 = 4.8175 of the source's rectangle certificate rect_n19_L48175 (T-074), the reported and verified lower bound at before it, by 0.0054. It is also above (7 + sqrt 7)/2 = 4.8228757..., the side of Hämäläinen's packing of 18 squares and the verified upper bound at , by about 2.43e-5, so < , as the source notes.
The certificate was decided here on 6 October 2026 by sqverify-fast, this repository's clean-room measure verifier, at all 416 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 found no defect. The source's own checker was replayed here at 10 of the 416 directions, each returning the certificate's own record, and not in full.
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 , by 0.0054, and the first to pass the side of the best packing of 18 squares, which separates from (Evan Daniel's question on jlevy/squares#281), by about 2.43e-5. The certificate kind and checker of T-069 and later on T-096's declared net; no new technique, at S3 as T-074 is, the separation a corollary of this bound and Hämäläinen's packing rather than a method or a family of bounds. 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 416 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. The source's checker was replayed at 10 directions and its axis tables were not run in full here, so no second method and no complete reproduction with the producer's code stands beside it.
The separation < is cited from 's record, whose verified upper bound is E-lifted-q7-upper, the exact verification of Hämäläinen's packing; this entry adds no evidence for it beyond its own bound. - 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 complete replay of the source's own checker, the bundle's driver over all 416 nodes by devtools.audit_wand125_declared_net replay (13.4 CPU-hours priced here), 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 case
Results on the case
13 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007
for
V0 C1 lower bound incomplete on this case, superseded by T-103
Nagamochi · Nagamochi 2005 · source · register
2026-08-21 published T-016
for , by monotonicity from T-015
V3 C3 lower bound confirmed superseded by T-103
Massaccesi after Burns · Burns–Massaccesi n17 · packet · register
2026-09-04 established T-019
for
V3 C3 lower bound confirmed superseded by T-103
Levy after Burns, Massaccesi · register
2026-09-04 established T-020
for
V3 C3 lower bound confirmed superseded by T-103
Levy after Burns, Massaccesi · register
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-27 published T-045
Rectangle-density lower bounds replayed at 15 counts in
V3 C3 lower bound confirmed superseded by T-103
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register
2026-09-27 published T-046
Rectangle-density lower bounds reported for 48 counts in
V0 C0 lower bound recorded superseded by T-103
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · register
2026-09-29 published T-058
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsV3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
for every nonsquare
V3 C3 lower bound confirmed on this case, superseded by T-103
Karakuş · Karakuş 2026 · source · register
2026-10-01 published T-068
Rectangle-density lower bounds verified at 34 counts in
V3 C3 lower bound confirmed on this case, superseded by T-103
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-01 published T-074
Rectangle-density lower bounds replayed at 31 counts in
V3 C3 lower bound confirmed on this case, superseded by T-103
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · packet · source · review · register
2026-10-06 published T-100 this result
Mixed rectangle-measure lower bound verified at , past the best 18-square packing
V3 C3 lower bound confirmed superseded by T-103
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds finer net 2026-10-06 · packet · source · review · register
2026-10-06 published T-103
Mixed rectangle-measure lower bound verified at , 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
Links
- On this site
- Case record, · Frontier row, · T-100 in the results table
On GitHub, at main
- Register
- T-100 in
results.yaml, line 10039 - Evidence
E-n019-wand125-mixed-48229-report·E-n019-wand125-mixed-48229-sqverify-fast-replay- Proofs and certificates
- certificate
candidate.json.gz· proofSOUNDNESS.md· auditreview-2026-10-06-wand125-finer-net-n18-n19.md - Sources
- wand125 mixed bounds finer net 2026-10-06 (its own site, retained copy)
- Source packet
resources/web/wand125-mixed-bounds-finer-net-2026-10-06/README.md- Artifacts
15 artifacts and controls
resources/web/wand125-mixed-bounds-finer-net-2026-10-06/README.mdresources/web/wand125-mixed-bounds-finer-net-2026-10-06/receipts/n19-L48229/audit.jsonresources/web/wand125-mixed-bounds-finer-net-2026-10-06/receipts/n19-L48229/bundle.jsonresources/web/wand125-mixed-bounds-finer-net-2026-10-06/receipts/n19-L48229/sample/nodes-000-411.jsondevtools/audit_wand125_declared_net.pysqverify_fast/SOUNDNESS.mdbenchmarks/measure-verifier/census-mixed/census.jsonbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-finer-net-2026-10-06/mixed_n19_L48229.jsonl.gzdevtools/sqverify_fast_census.pydocs/project/reviews/review-2026-10-06-wand125-finer-net-n18-n19.mddocs/project/reviews/review-2026-10-06-sqverify-fast-declared-net-soundness.mdbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-finer-net-2026-10-06/mixed_n19_L48229.control.jsontests/test_sqverify_fast_census.pyresources/web/wand125-mixed-bounds-finer-net-2026-10-06/receipts/n19-L48229/control.jsontests/test_audit_wand125_declared_net.py- Case file
frontier/n-019.md(verified lower, verified upper, reported lower, reported upper)