T-094: Mixed rectangle-measure lower bounds verified at and
V3 C3 lower bound confirmed
Two rectangle densities of wand125/square-packing-bounds, checked at coverage one and published on 5 October 2026, prove = 8.48 and = 9.411.
Each is a density of uniform rectangles in D4 orbits, 536 at and 686 at , 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 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 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
Proven
- 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
Proven
- 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 , oldest first, each with what it established and how it stands now.
2005 published T-007 ·
for
V0 C1 lower bound incomplete on these cases, superseded by T-094
Nagamochi · Nagamochi 2005 · source · 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-046 ·
Rectangle-density lower bounds reported for 48 counts in
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
2026-09-28 published T-070 ·
Rectangle-density lower bounds replayed at 25 counts in
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
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 these cases, superseded by T-094
Karakuş · Karakuş 2026 · source · register
2026-10-02 published T-071 ·
Mixed rectangle-measure lower bounds replayed at
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
2026-10-04 published T-090 ·
Mixed rectangle-measure lower bounds verified at 17 counts in
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
2026-10-05 published T-094 this result ·
Mixed rectangle-measure lower bounds verified at and
V3 C3 lower bound confirmed
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-05 · packet · source · review · register
2026-10-08 published T-125 ·
Complete rational construction reports at 25 counts
V3 C3 upper bound confirmed
ry-xu · ry-xu square packing 2026 · packet · register
2026-10-08 published T-130 ·
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
2026-10-09 published T-138 ·
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
Links
- On this site
- Case record, · Frontier row, · Case record, · Frontier row, · T-094 in the results table
On GitHub, at main
- Register
- T-094 in
results.yaml, line 9292 - Evidence
E-n067-wand125-mixed-848-report·E-n067-wand125-mixed-848-sqverify-fast-replay·E-n084-wand125-mixed-9411-report·E-n084-wand125-mixed-9411-sqverify-fast-replay- Proofs and certificates
- certificate
candidate.json.gz· proofSOUNDNESS.md· auditreview-2026-10-05-wand125-october-5-and-independent-replays.md· certificatecandidate.json.gz - Sources
- wand125 mixed bounds 2026-10-05 (its own site, retained copy)
- Source packet
resources/web/wand125-mixed-bounds-2026-10-05/README.md- Artifacts
11 artifacts and controls
resources/web/wand125-mixed-bounds-2026-10-05/README.mdresources/web/wand125-mixed-bounds-2026-10-05/receipts/mixed-audit.jsondevtools/audit_wand125_point_and_mixed.pybenchmarks/measure-verifier/census-mixed/census.jsonbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-2026-10-05/mixed_n67_L848.jsonl.gzbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-2026-10-05/mixed_n84_L9411.jsonl.gzdevtools/sqverify_fast_census.pydocs/project/reviews/review-2026-10-05-wand125-october-5-and-independent-replays.mdbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-2026-10-05/mixed_n67_L848.control.jsonbenchmarks/measure-verifier/census-mixed/wand125-mixed-bounds-2026-10-05/mixed_n84_L9411.control.jsontests/test_sqverify_fast_census.py- Case file
frontier/n-067.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-084.md(verified lower, verified upper, reported lower, reported upper)