T-071: Mixed rectangle-measure lower bounds replayed at
V3 C3 lower bound confirmed superseded by T-075, T-090, T-091 and T-094
Two rectangle densities of wand125/square-packing-bounds, checked at coverage one and published on 2 October 2026, prove = 9.4 and = 9.42. The certificate's mass is below 86 and 87 too, so it gives and as well: four counts in all.
Each certificate is a density of uniform rectangles with no point mass, of total mass n - 1/100000, at core side 9977/10000 on 201 net half-angles of step 83/40000: 661 rectangles at and 587 at . Each is accepted at every oblique net angle by code/mixed_rotated_verify.cpp, the research copy of Tokoharu's verify.cpp that the source's certificate (T-048) and the five certificates of T-069 use, which accepts coverage at least 1 where Tokoharu's requires 10001/10000, and at angle zero by exact integer tables. The least oblique lower bounds are 1.00000000089 at and 1.0000000017 at .
Both values exceed Green's reported 2 sqrt(2) + (247 + 12 sqrt(2))/41 = 9.2667335..., which this record holds at both counts by monotonicity from , by more than 0.1332 and 0.1532; the source's own improvement figures are measured from 9.2667, below Green's value, and are not lower bounds. At and 87 the value is also above the rectangle certificates T-068 reports there, 1873/200 and 941/100.
Each certificate passed a complete replay here on 2 October 2026 of the source's unchanged checker and per-angle functions on its pinned tarball: all 201 directions, each returning the certificate's own record. The replays run the source's own algorithm and are not an independent decision of coverage.
wand125 after Tokoharu and Levy, square-packing-bounds. Registration was requested in a comment of 2 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
- Raised the verified lower bound at four counts, to 87, past Green's reported value at and 85 by the widest margins over it on record, by the certificate kind of T-048 and T-069. Further sizes from one generator at S3; the 2 October review of these certificates proposed S3, which the replays leave standing.
- Composition
- Two primary certificates, each on its own reported entry and its own replay entry. and 87 take the certificate directly, its mass being below those counts, so no step is added. Each replay runs the source's C++ checker unchanged: one interval-certified method, replayed here, C3. Coverage is decided by that checker alone; 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 replays here run the source's own checker. The checker's controls were made on the certificate of the same kind.
- Novelty
- previously-published Present in an identified source
The cases
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
Proven
- exact
Citation record n-085
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-075)
upperFriedman 1997, Squares in Squares
Open
- optimality
The case record
Proven
- exact
Citation record n-086
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-090)
upperry-xu 2026, GitHub (confirmed T-125)
Open
- optimality
The case record
Proven
- exact
Citation record n-087
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-091)
upperEllsworth et al., Squares in Squares (confirmed T-101)
Open
- optimality
The case record
Results on these cases
18 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-075, T-090, T-091 and 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-24 published T-089 ·
and , Chang's packings, certified exactly
V3 C3 upper bound confirmed superseded by T-101
Chang, Ellsworth after Cantrell, Hajba, Stenlund, Bidwell; Chang after Ellsworth, Cantrell, Schadt, Hajba, DeVincentis · Chang n83 2026-09-24 · Chang n87 2026-09-24 · packet · 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-090
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-090
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-075, T-090, T-091 and T-094
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 these cases, superseded by T-090 and T-091
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · source · review · register
2026-10-02 published T-071 this result ·
Mixed rectangle-measure lower bounds replayed at
V3 C3 lower bound confirmed superseded by T-075, T-090, T-091 and T-094
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-02 · packet · source · review · register
2026-10-02 published T-075 ·
Mixed rectangle-measure lower bounds replayed at nine counts in
V3 C3 lower bound confirmed
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds afternoon 2026-10-02 · packet · source 1 · source 2 · review · register
2026-10-03 published T-082 ·
Mixed rectangle-measure lower bounds verified at 22 counts in
V3 C3 lower bound confirmed on these cases, superseded by T-090 and T-091
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · 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
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-04 · packet · source · review · register
2026-10-04 published T-091 ·
Mixed rectangle-measure lower bounds verified at 17 counts in
V3 C3 lower bound confirmed
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds evening 2026-10-04 · packet · source · review · register
2026-10-05 published T-094 ·
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-05 published T-101 ·
Exact certificates of 77 catalogue packings:
s(n) ≤ S',1.2e-16to9.8e-15above each sideV3 C3 upper bound confirmed
Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · 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, · Case record, · Frontier row, · Case record, · Frontier row, · T-071 in the results table
On GitHub, at main
- Register
- T-071 in
results.yaml, line 6561 - Evidence
E-n084-wand125-mixed-940-report·E-n084-wand125-mixed-940-source-replay·E-n085-wand125-mixed-942-report·E-n085-wand125-mixed-942-source-replay- Proofs and certificates
- certificate
candidate.json.gz· proofcontinuous-density-certificate.ja.md· auditreview-2026-10-02-wand125-mixed-rectangle-bounds.md· certificatecandidate.json.gz - Sources
- wand125 mixed bounds 2026-10-02 (its own site, retained copy)
- Source packet
resources/web/wand125-mixed-bounds-2026-10-02/README.md- Artifacts
10 artifacts and controls
resources/web/wand125-mixed-bounds-2026-10-02/README.mdresources/web/wand125-mixed-bounds-2026-10-02/square-packing-bounds/certificates/mixed_n84_L940/README.mdresources/web/wand125-mixed-bounds-2026-10-02/square-packing-bounds/certificates/mixed_n85_L942/README.mdresources/web/wand125-mixed-bounds-2026-10-02/receipts/mixed-audit.jsonresources/web/wand125-mixed-bounds-2026-10-02/receipts/n84/merged.jsonresources/web/wand125-mixed-bounds-2026-10-02/receipts/n85/merged.jsondevtools/audit_wand125_point_and_mixed.pydocs/project/reviews/review-2026-10-02-wand125-mixed-rectangle-bounds.mdtests/test_wand125_checker_controls.pyresources/web/wand125-point-and-mixed-2026-10-01/receipts/n37/control.json- Case file
frontier/n-084.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-085.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-086.md(verified lower, verified upper, reported lower, reported upper) ·frontier/n-087.md(verified lower, verified upper, reported lower, reported upper)