T-096: Mixed rectangle-measure lower bound replayed at , on a net the certificate declares
V3 C3 lower bound confirmed superseded by T-102
A rectangle density of wand125/square-packing-bounds, checked at coverage one on a net it declares and published on 5 October 2026, proves = 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 , 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 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 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
Results on the case
17 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-102
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-102
Massaccesi after Burns · Burns–Massaccesi n17 · packet · register
2026-08-31 established T-002
, by monotonicity from T-001
V3 C3 lower bound confirmed superseded by T-102
Levy after Bentz · register
2026-08-31 established T-003
The sixteen-point set's unavoidability ceiling lies in
V3 C3 method limit confirmed
Levy after Bentz · register
2026-09-04 established T-019
for
V3 C3 lower bound confirmed superseded by T-102
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-18 established T-027
V3 C3 lower bound confirmed superseded by T-102
Levy after Burns, Massaccesi · register
2026-09-19 established T-028
V3 C3 lower bound confirmed superseded by T-102
Levy after Burns, Massaccesi · register
2026-09-19 established T-029
V3 C3 lower bound confirmed superseded by T-102
Levy after Burns, Massaccesi · register
2026-09-19 established T-030
V3 C3 lower bound confirmed superseded by T-102
Levy after Burns, Massaccesi · register
2026-09-27 published T-045
Rectangle-density lower bounds replayed at 15 counts in
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
2026-09-27 published T-046
Rectangle-density lower bounds reported for 48 counts in
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
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-102
Karakuş · Karakuş 2026 · source · register
2026-10-05 published T-096 this result
Mixed rectangle-measure lower bound replayed at , 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
2026-10-06 published T-099
Mixed rectangle-measure lower bound verified at , 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
2026-10-06 published T-102
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-096 in the results table
On GitHub, at main
- Register
- T-096 in
results.yaml, line 9534 - Evidence
E-n018-wand125-mixed-470-report·E-n018-wand125-mixed-470-source-replay- Proofs and certificates
- certificate
candidate.json.gz· proofcontinuous-density-certificate.ja.md· auditreview-2026-10-05-wand125-declared-net-n18-n66.md - Sources
- wand125 mixed bounds finer net 2026-10-05 (its own site, retained copy)
- Source packet
resources/web/wand125-mixed-bounds-finer-net-2026-10-05/README.md- Artifacts
12 artifacts and controls
resources/web/wand125-mixed-bounds-finer-net-2026-10-05/README.mdresources/web/wand125-mixed-bounds-finer-net-2026-10-05/receipts/n18-L470/audit.jsonresources/web/wand125-mixed-bounds-finer-net-2026-10-05/receipts/n18-L470/bundle.jsondevtools/audit_wand125_declared_net.pysqverify_fast/SOUNDNESS.mdresources/web/wand125-mixed-bounds-finer-net-2026-10-05/receipts/n18-L470/full/compare.jsonresources/web/wand125-mixed-bounds-finer-net-2026-10-05/receipts/n18-L470/full/run.metabenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-finer-net-2026-10-05/mixed_n18_L470.jsonl.gzdocs/project/reviews/review-2026-10-05-wand125-declared-net-n18-n66.mdtests/test_wand125_checker_controls.pyresources/web/wand125-point-and-mixed-2026-10-01/receipts/n37/control.jsontests/test_audit_wand125_declared_net.py- Case file
frontier/n-018.md(verified lower, verified upper, reported lower, reported upper)