T-137: An exact rational refinement of Ryan Xu's packing of 70 squares

V3 C3 upper bound confirmed

2026-10-10 published · Deleeuw after Xu, Levy · n=70

One complete rational source certificate by Eric Deleeuw, reported on jlevy/squares#483, proves a finite upper bound at the exact side it states: s(70)≤8.88096037156625096037155737.

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 n=70, 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

Case record

n=70

8.658.881
8910
8.3679.367
nn+1

Proven

8.65750≤s(70)≤8.880961

  • 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

LowerUpper
Gap0.22346037…

Results on the case

16 results in the register on n=70, oldest first, each with what it established and how it stands now.

  1. 2005 published T-007

    s(n)≥min(⌈n⌉,n−2⌊n⌋+1+1) for 4≤n≤324

    V0 C1 lower bound incomplete on this case, superseded by T-091

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-09-04 published T-085

    Nagamochi 2005, Lemma 1 is false for every container with a>3 and b>2

    V3 C3 correction confirmed

    Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

  3. 2026-09-22 published T-044

    Weighted point lower bounds for ten counts in n=26…72, 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

  4. 2026-09-27 published T-046

    Rectangle-density lower bounds reported for 48 counts in n=18…95

    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

  5. 2026-09-28 published T-070

    Rectangle-density lower bounds replayed at 25 counts in n=29…95

    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

  6. 2026-09-29 published T-058

    Rectangle-certificate ceiling α·UB(n) proved for n=1..100; B·UB(n) on 64 grid rows

    V3 C3 method limit confirmed

    wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register

  7. 2026-09-29 published T-083

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤324

    V3 C3 lower bound confirmed on this case, superseded by T-091

    Karakuş · Karakuş 2026 · source · register

  8. 2026-10-01 published T-068

    Rectangle-density lower bounds verified at 34 counts in n=19…95

    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

  9. 2026-10-01 published T-074

    Rectangle-density lower bounds replayed at 31 counts in n=19…95

    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

  10. 2026-10-02 published T-077

    Rectangle-density lower bounds replayed at n=20, 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

  11. 2026-10-03 published T-082

    Mixed rectangle-measure lower bounds verified at 22 counts in n=51…96

    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

  12. 2026-10-04 published T-091

    Mixed rectangle-measure lower bounds verified at 17 counts in n=53…95

    V3 C3 lower bound confirmed

    wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds evening 2026-10-04 · packet · source · review · register

  13. 2026-10-05 published T-101

    Exact certificates of 77 catalogue packings: s(n) ≤ S', 1.2e-16 to 9.8e-15 above each side

    V3 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

  14. 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

  15. 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

  16. 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