T-032: $s (17) \geq 461300 / 99999 = 4.61304613 \dots$ , and beneath it Mira's $s (17) \geq 4613 / 1000$

V3 C3 lower bound confirmed superseded by T-093

2026-09-20 published · Guzhou0806, Mira after Levy, Burns, Massaccesi · $n = 17$

$s (17) \geq 461300 / 99999$ = 4.61304613..., by Guzhou0806's R012 parent-angle certificate of 20 September 2026. Beneath it, $s (17) \geq 4613 / 1000$ by Mira's 1620-atom weighted certificate of 7 September 2026. The case previously held 459/100 from T-019, and the movement is +0.02305 at the R012 value and +0.023 at Mira's side.

The R012 argument is this repository's weighted method with three changes. Parents have side A = 99999/100000 inside [0, L]^2 at L = 4613/1000, and the bound is L/A. A catalogue of 2925 closed parent-angle intervals covers [0, pi/4], and each interval picks its own concentric closed core, by direction and side, strictly inside every parent of the interval. Coverage by the measure is required only over the legal parent-centre square for the interval.

The measure is Mira's, rounded to 10^-5 with weights rounded up, 1616 atoms of mass 424969/25000; every core captures at least gamma = 250023/250000, and 17 gamma exceeds the mass by 701/250000. One size: the measure's mass is just below 17, so the certificate also says $s (18)$ and $s (19)$ are at least this value, and the register already holds 4679/1000 and 24/5 there.

R012 was replayed here by the source's exact checker and decided again by this repository's interval branch and bound. Mira's certificate is in this repository's certificate schema, and both stock verifiers accept it unchanged.

Guzhou0806, n17-square-packing, and Mira, 17squares. Both certificates descend from T-019 and credit it.

Significance, composition and next rung

Significance: Raises the verified lower bound at $n = 17$ by 0.02305 over T-019 and closes the gap to Bidwell's 4.67553009 to 0.0625. Scored as T-015 was, and for the same reason: a result by others that this repository replayed, decided by a second method and read closely. Two things keep it at S3. The technique is the one T-017 and T-019 banked, extended by others; and almost all of the movement is Mira's support and weights, R012's selector and parent-centre restriction adding 1.7e-5 on a fixed measure. What those two extensions are worth on a measure optimised against them is open and is not this result.
Composition: Primary at $n = 17$ on the R012 certificate: the bound is L/A from one catalogue and one measure, with no monotonicity step. That certificate is decided by two evidence entries whose methods differ, the source's exact event-cell replay and this repository's interval decision of all 2925 entries, both passing on the archived bytes; that is C3, with the two methods shown beside the rung.

The exact route is the source's own checker, whose sweep descends from this repository's, so its independence is of method from the interval route and not of authorship from the generator; the proof review also decided every entry with this repository's sweep kernel and agreed on all 2925 minima, as review scratch.

Mira's certificate carries its own pair of entries, the stock exact verifier and the stock interval verifier, and supports the weaker statement $s (17) \geq 4613 / 1000$ independently of R012. The reduction from a packing to R012's finite obligations is a read argument, closed in the review artifact, and is what a formal port would address.
Next rung: Mira's dilation endpoint, 4.61302863588611..., needs a T-022-style proof note for this certificate and is superseded by the R012 value in any case. A retained exact-route instrument for R012 that does not share the source's sweep lineage would make the exact leg this repository's own; the review's scratch pass shows the stock kernel decides every entry in about six minutes once its centre domain is a parameter.

V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record beside the 2026-09-20 proof review. Rung 5 needs a proof-assistant formalization of the reduction, reviewed by human experts. The method's open question is what the selector and the parent-centre restriction gain when the measure is optimised against them; Mira reports a failed attempt at 4.615 on the unrestricted test.
Novelty: previously-published Present in an identified source

The case

Case record

4.664.676

456

4.1235.123

\sqrt{n}

\sqrt{n} + 1

Proven

$4.66044$ $\leq s (17) \leq$ $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

LowerUpper

Verified

\frac{18641771}{4000000}

4.67553009…

Reported

\frac{18641771}{4000000}

4.67553009…

Gap0.01508734…

Results on the case

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

2005 published T-007
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
V0 C1 lower bound incomplete on this case, superseded by T-093
Nagamochi · Nagamochi 2005 · source · register
2026-08-21 published T-015
$s (17) \geq 22529 / 5000 = 4.5058$
V3 C3 lower bound confirmed superseded by T-093
Massaccesi after Burns · Burns–Massaccesi n17 · packet · register
2026-08-31 established T-001
$s (17) \geq 4426213 / 1000000 = 4.426213$ , from a sixteen-point unavoidable set
V3 C3 lower bound confirmed superseded by T-093
Levy after Bentz · register
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
2026-09-04 established T-019
$s (n) \geq 459 / 100 = 4.59$ for $n = 17, 18, 19$
V3 C3 lower bound confirmed superseded by T-093
Levy after Burns, Massaccesi · register
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
2026-09-20 published T-032 this result
$s (17) \geq 461300 / 99999 = 4.61304613 \dots$ , and beneath it Mira's $s (17) \geq 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
2026-09-21 published T-038
$s (17) > 461300 / 99853 = 4.6197910929 \dots$
V3 C3 lower bound confirmed superseded by T-093
Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register
2026-09-21 published T-065
$s (17) \leq 4.6755300936045509 \dots$ , Bidwell's packing certified exactly
V3 C3 upper bound confirmed
Kleddamag after Levy, Mira, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register
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
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
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
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
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
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
2026-09-29 published T-083
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
V3 C3 lower bound confirmed on this case, superseded by T-093
Karakuş · Karakuş 2026 · source · register
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

Links

On this site: Case record, $n = 17$ · Frontier row, $n = 17$ · T-032 in the results table

On GitHub, at main

Register: T-032 in results.yaml, line 2611
Evidence: E-n017-guzhou-r012-source-replay · E-n017-guzhou-r012-interval-decision · E-n017-mira-4613-exact-replay · E-n017-mira-4613-interval-decision
Proofs and certificates: certificate orbits.json · certificate catalogue.json · certificate best-certificate.json
Sources: n17 weighted certificates 2026-09-20 (its own site, retained copy)
Source packet: resources/web/n17-weighted-certificates-2026-09-20/README.md
Artifacts: 7 artifacts and controls
resources/web/n17-weighted-certificates-2026-09-20/README.md resources/web/n17-weighted-certificates-2026-09-20/guzhou0806-n17-square-packing/certificates/R012/PROOF.md resources/web/n17-weighted-certificates-2026-09-20/guzhou0806-n17-square-packing/certificates/R012/verify.py resources/web/n17-weighted-certificates-2026-09-20/replay_guzhou_r012_first_party.py resources/web/n17-weighted-certificates-2026-09-20/replay_mira_4613_first_party.py resources/web/n17-weighted-certificates-2026-09-20/mira-17squares/certificates/lower_bound_4p613/best-certificate.json tests/test_n17_external_weighted_certificates.py
Case file: frontier/n-017.md (verified lower, verified upper, reported lower, reported upper)

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

The case

Results on the case

Links

T-032: $s (17) \geq 461300 / 99999 = 4.61304613 \dots$ , and beneath it Mira's $s (17) \geq 4613 / 1000$