T-065: s(17)≤4.6755300936045509…, Bidwell's packing certified exactly

V3 C3 upper bound confirmed

2026-09-21 published · Kleddamag after Levy, Mira, Guzhou0806 · n=17

s(17)≤4.6755300936045509516342148538535054: seventeen unit squares fit in a square of at most that side. The figure is a rational outward ceiling, not the exact side of the packing.

Kleddamag's release of 21 September 2026 carries John Bidwell's 1998 construction forward as an exact rational witness, s(17)≤4675530093604551/10^15, which two exact implementations here and the source's own checker accept: 17 unit squares, 68 vertices contained, 136 pairs separated.

From that seed this project certified the packing at the unique root of its contact chart: the root exists and is unique in a frozen rational box, and all 68 wall and 136 pair obligations hold there, 36 as exact identities and 168 by rational interval bounds, and an independent audit reconstructs every interval record. This lowers Kleddamag's rational ceiling in the seventeenth decimal.

The ceiling agrees with Bidwell's record in the Kingbird catalogue at the catalogue's printed precision. No identity with the catalogue's degree-18 polynomial is proved, no new packing is claimed, and optimality is not claimed.

Kleddamag, Kleddamag/17-squares-certified-bound, for the rational witness of Bidwell's packing; its AUTHORS.md says the work was produced with AI agents under Kleddamag's direction.

Significance, composition and next rung
Significance
The first verified upper bound at n=17 below the grid's 5: the case's verified bracket becomes 4.66044 < s(17)≤4.67553009…, both ends machine-checked, where the upper end was a reported catalogue value. S3 by the anchor "a substantive case result or machine audit"; it moves no reported bound.
Composition
Two parts, both V3/C3. Kleddamag's rational witness is E-n017-kleddamag-rational-upper, replayed here exactly. The registered ceiling is E-n017-certified-endpoint, derived here from that witness and audited here; its accepted root proof and its reviewed symbolic identities are stated premises of the audit. The second part sets the bound.
Next rung
Rung 4 on either axis needs two adversarial AI reviews by distinct reviewers and a retained human oversight record. With exp-245 the packing's side is the catalogue's degree-18 root, so whether to restate this bound at Bidwell's exact algebraic value is a registration decision. First-order stationarity is certified (exp-242), and a local minimum modulo sliders holds in the capture-target form (exp-244, exp-248); global optimality is unproved.
Novelty
previously-published Present in an identified source

The case

Case record

n=17

4.664.676
456
4.1235.123
nn+1

Proven

4.66044≤s(17)≤4.675531

  • exact

Citation record n-017

lowerGuzhou0806 after Kleddamag et al. 2026, GitHub (confirmed T-093)

upperBidwell 1998, Squares in Squares (confirmed T-065)

Open

  • optimality

The case record

Results on the case

17 results in the register on n=17, 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-093

    Nagamochi · Nagamochi 2005 · source · register

  2. 2026-08-21 published T-015

    s(17)≥22529/5000=4.5058

    V3 C3 lower bound confirmed superseded by T-093

    Massaccesi after Burns · Burns–Massaccesi n17 · packet · register

  3. 2026-08-31 established T-001

    s(17)≥4426213/1000000=4.426213, from a sixteen-point unavoidable set

    V3 C3 lower bound confirmed superseded by T-093

    Levy after Bentz · register

  4. 2026-08-31 established T-003

    The sixteen-point set's unavoidability ceiling lies in [4426213/1000000,4427/1000)

    V3 C3 method limit confirmed

    Levy after Bentz · register

  5. 2026-09-04 established T-019

    s(n)≥459/100=4.59 for n=17,18,19

    V3 C3 lower bound confirmed superseded by T-093

    Levy after Burns, Massaccesi · register

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

  7. 2026-09-20 published T-032

    s(17)≥461300/99999=4.61304613…, and beneath it Mira's s(17)≥4613/1000

    V3 C3 lower bound confirmed superseded by T-093

    Guzhou0806, Mira after Levy, Burns, Massaccesi · n17 weighted certificates 2026-09-20 · packet · register

  8. 2026-09-21 published T-038

    s(17)>461300/99853=4.6197910929…

    V3 C3 lower bound confirmed superseded by T-093

    Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register

  9. 2026-09-21 published T-065 this result

    s(17)≤4.6755300936045509…, Bidwell's packing certified exactly

    V3 C3 upper bound confirmed

    Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register

  10. 2026-09-25 published T-039

    s(17)>231001/50000=4.62002

    V3 C3 lower bound confirmed superseded by T-093

    Guzhou0806 after Kleddamag, Mira, Levy · Guzhou0806 n17 R052 · packet · source · review · register

  11. 2026-09-26 published T-040

    s(17)>232001/50000=4.64002

    V3 C3 lower bound confirmed superseded by T-093

    Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 4.640020 · packet · source · review · register

  12. 2026-09-27 published T-041

    s(17)>466001/100000=4.66001

    V3 C3 lower bound confirmed superseded by T-093

    Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 4.66001 · packet · source · review · register

  13. 2026-09-28 published T-042

    s(17)>233009/50000=4.66018

    V3 C3 lower bound confirmed superseded by T-093

    Guzhou0806 after Kleddamag, Mira, Levy · Guzhou0806 n17 R067 · packet · source · review · register

  14. 2026-09-28 published T-043

    s(17)>116511/25000=4.66044

    V3 C3 lower bound confirmed superseded by T-093

    Guzhou0806 after Kleddamag, Mira, Levy · Guzhou0806 n17 R068 · packet · source · review · register

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

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

    Karakuş · Karakuş 2026 · source · register

  17. 2026-09-30 published T-093

    s(17)>18641771/4000000=4.66044275

    V3 C3 lower bound confirmed

    Guzhou0806 after Kleddamag, Mira, Levy · Guzhou0806 n17 R071 · packet · source · review · register