T-137: An exact rational refinement of Ryan Xu's packing of 70 squares
V3 C3 upper bound confirmed
One complete rational source certificate by Eric Deleeuw, reported on jlevy/squares#483, proves a finite upper bound at the exact side it states: .
The certificate gives a rational side and, for each unit square, a rational centre in the centred box and the tangent of its half-angle; its side already carries the dilation it states. The author reports that its own exact Fraction checker accepts all 280 corners and all 2,415 pairs with zero tolerance, and that David Ellsworth's check_packing.py accepts a 60-digit export; the generator and the exact checker were written together.
All three retained jobs, the positive with its duplicate-square and outside-container controls, were decided again here on 10 October 2026 by both maintained exact routes, from an exact fact derived from the pinned certificate with every centre moved by half the side, and equal their retained rows. A third exact route, half-extent containment and exact intersection area, decided it with six controls and found the fact to be the packing the pinned upstream file states. No route here is the source's code, so the replay is independently re-implemented. The 10 October review found no blocking defect.
The side is 1.43e-10 below the ceiling the case holds, Ryan Xu's certificate (T-125); the case record is unchanged, so it is pending adoption.
Credit Eric Deleeuw (https://github.com/ebdeleeuw/square-packing-n70) for the refinement and the rational certificate, after Ryan Xu's arrangement and published warm-start coordinates (issue 432). The source discloses OpenAI Codex assistance with the refinement, the certificate, the verification tools and the submission.
Significance, composition and next rung
- Significance
- A smaller finite construction side at , 1.43e-10 below the case ceiling; no lower bound or optimum.
- Next rung
- V4 and C4 need a retained human oversight record: two accepted adversarial reviews by distinct AI reviewers are retained, the 10 October review and the 11 October final review (docs/project/reviews/review-2026-10-11-final-upper-bounds.md). No house move is due for this entry: the house recommendation at 70 goes to T-146, whose side there is smaller and whose 11 October review accepted it, and this entry stays verified, as the smallest side the record held before it.
- Novelty
- previously-published Present in an identified source
The case
Proven
- exact
Citation record n-070
lowerwand125 after Tokoharu, Levy et al. 2026, GitHub (confirmed T-091)
upperry-xu 2026, GitHub (confirmed T-125)
Open
- optimality
The case record
Results on the case
16 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-091
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-22 published T-044
Weighted point lower bounds for ten counts in , plus seven from the same files
V3 C3 lower bound confirmed superseded by T-091
wand125 after Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point bounds 2026 · 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-091
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-091
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 this case, superseded by T-091
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-091
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-091
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-01 · packet · packet · source · review · register
2026-10-02 published T-077
Rectangle-density lower bounds replayed at , 42 and 70
V3 C3 lower bound confirmed superseded by T-091
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-10-02 · packet · packet · source 1 · source 2 · review 1 · review 2 · register
2026-10-03 published T-082
Mixed rectangle-measure lower bounds verified at 22 counts in
V3 C3 lower bound confirmed on this case, superseded by 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-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-101
Exact certificates of 77 catalogue packings:
s(n) ≤ S',1.2e-16to9.8e-15above each sideV3 C3 upper bound confirmed on this case, superseded by T-125
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-10 published T-137 this result
An exact rational refinement of Ryan Xu's packing of 70 squares
V3 C3 upper bound confirmed
Deleeuw after Xu, Levy · Deleeuw n70 refinement 2026-10-10 · packet · register
2026-10-10 published T-146
Exact rational certificates at fifteen counts from Evan Daniel's regularized record lists
V3 C3 upper bound confirmed
Daniel after Xu, Chaoweeraprasit, Mishapolk, Levy · Daniel regularized lists 2026-10-10 · packet · register
Links
- On this site
- Case record, · Frontier row, · T-137 in the results table
On GitHub, at main
- Register
- T-137 in
results.yaml, line 14365 - Evidence
E-deleeuw-483-certificate-report·E-deleeuw-483-exact-feasibility- Proofs and certificates
- certificate
facts· certificaten-070.yaml.gz - Sources
- Deleeuw n70 refinement 2026-10-10
- Source packet
resources/web/ebdeleeuw-n70-refinement-2026-10-10/README.md- Artifacts
9 artifacts and controls
resources/web/ebdeleeuw-n70-refinement-2026-10-10/README.mdresources/web/ebdeleeuw-n70-refinement-2026-10-10/acquisition/claims.jsonresources/web/ebdeleeuw-n70-refinement-2026-10-10/facts/n-070.yaml.gzresources/web/ebdeleeuw-n70-refinement-2026-10-10/receipts/exact-certification.json.xzdevtools/upper_bound_reports.pydevtools/check_half_angle_area.pydocs/project/reviews/review-2026-10-10-upper-bound-imports-476-481-483-484.mdtests/test_upper_bound_reports.pytests/test_check_half_angle_area.py- Case file
frontier/n-070.md(verified lower, verified upper, reported lower, reported upper)