n = 17 · Case Records · The Squares Project

n = 17 open ★=

$\frac{18641771}{4000000} \leq s (17) \leq 4.67553009 …$

The best packing known for 17 squares, side

4.67553009 …

, John Bidwell 1998

4.6604.676

456

4.1235.123

\sqrt{n}

\sqrt{n} + 1

Proven

$4.660442$ $\leq s (17) \leq$ $4.675531$

new result
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

Bounds

Best known packing

4.67553009…

4.67553009360455

Found by: John Bidwell 1998
Construction: hand
Tilt angles: $0^{\circ}$ , $39.80495897 …^{\circ}$ , $- 36.62378638 …^{\circ}$
Minimal polynomial, degree 18: $4775 s^{18} - 190430 s^{17} + 3501307 s^{16} - 39318012 s^{15} + 300416928 s^{14} - 1640654808 s^{13} + 6502333062 s^{12} - 18310153596 s^{11} + 32970034584 s^{10} - 18522084588 s^{9} - 93528282146 s^{8} + 350268230564 s^{7} - 662986732745 s^{6} + 808819596154 s^{5} - 660388959899 s^{4} + 358189195800 s^{3} - 126167814419 s^{2} + 26662976550 s - 2631254953 = 0$
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

4.67553009…

4.6755300936045509516342148538535054

The reported value, verified here.

Evidence: E-n017-certified-endpoint

Reported lower bound

$\frac{18641771}{4000000}$

Proved by: Guzhou0806 2026
Kind: counting
Scope: This field preserves the source report. The complete paired replay of R071 here on 2026-10-05 carries the same value into the verified field; R070 has not been replayed here.
Note: The R071 release of Guzhou0806/n17-square-packing (30 September 2026) states the strict bound $s (17) > 18641771 / 4000000$ = 4.66044275 for independently rotated unit squares with disjoint interiors and boundary contact allowed. Guzhou0806 / N17 project, on R068's continuation of Kleddamag's public 4.66001 charge (Kleddamag building on Squares Project (Joshua Levy), Mira and Guzhou0806): every point orbit, rule orbit and weight is R068's, and the strict cores are rebuilt over 5,114 orientation intervals at parent side 18452000/18641771, refining the previous day's R070 (46604427/10000000 over 5,107 intervals). The package credits Kleddamag for the 4.66001 framework, proof and JavaScript checker, discloses AI assistance, says its row-level partition records are missing, and states that its publisher checked file identities and saved records only and did not observe its CI.
Source: [Guzhou0806 n17 R071]
Evidence: E-n017-guzhou-r071-report

Verified lower bound

$\frac{18641771}{4000000}$

The reported value, verified here.

Evidence: E-n017-guzhou-r071-source-replay

Gap

0.01508734…

Verified upper minus verified lower.

Results in the register

T-001 V3 C3 Levy after Bentz · 2026-08-31 · n = 17
$s (17) \geq 4426213 / 1000000 = 4.426213$ , from a sixteen-point unavoidable set
Claim and records
Claim
Sixteen points make [0, 4426213/1000000]^2 unavoidable for open squares of side above one, so $s (17) \geq 4426213 / 1000000$ = 4.426213.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained; the packet to review is the statement, hypotheses, proof narrative, code map and replays. Rung 5 needs a proof-assistant formalization reviewed by human experts. The stronger side at the exact ceiling is T-003's business.
Significance
The first verified lower-bound movement in the register since Nagamochi 2005 at these n, and the strongest theorem this repository has proved itself to date; a two-case improvement in a specialist literature, 0.019 below Green's reported but sourceless value.
Novelty
apparently-novel Not found in the recorded search, subject to its stated gaps
Records
n = 17 register evidence 1 evidence 2
n = 17 register evidence 1 evidence 2
T-003 V3 C3 Levy after Bentz · 2026-08-31 · n = 17, 18
The sixteen-point set's unavoidability ceiling lies in $[4426213 / 1000000, 4427 / 1000)$
Claim and records
Claim
The sixteen-point set's unavoidability ceiling lies in [4426213/1000000, 4427/1000): certification at the left endpoint, an exact escaping pose at the right, with the top strips' a + 2b <= 2*sqrt(2) hypothesis identifying the closing mechanism at 753/250 + sqrt(2), inside the bracket.
Composition
Compound: the lower side of the bracket carries T-001's two methods and the refutation side rests on the interval audit alone. Both are machine-replayed here, so the bracket is C3; a second method on one side does not change the rung. The equality reading is deliberately not this claim.
Next rung
think-iye2: the shared certifier generalized to a Q(sqrt 2) scalar certifies at the ceiling exactly and an exact escape family above it turns the bracket into an equality at C3.
Significance
Sharpens what T-001's construction can and cannot give; the exact equality claim at 753/250 + sqrt(2) remains analysis until the Q(sqrt 2) certificate lands.
Novelty
apparently-novel Not found in the recorded search, subject to its stated gaps
Records
n = 17 n = 18 register evidence 1 evidence 2
n = 17 n = 18 register evidence 1 evidence 2
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
T-015 V3 C3 Massaccesi after Burns · 2026-09-03 · n = 17
$s (17) \geq 22529 / 5000 = 4.5058$
Claim and records
Claim
$s (17) \geq 22529 / 5000$ = 4.5058, by Massaccesi's 168-atom fractional unavoidable-set certificate on Burns's architecture: total mass 203/12 < 17 and mass at least 1 in every closed unit square of [0, 22529/5000]^2, reduced exactly to 181 rational directions and finitely many event cells.

It was replayed here by the source verifier and by an accumulation-independent repository instrument.

Gustavo Massaccesi, building on Sam Burns, in a blog post of 21 August 2026. Massaccesi marks the value "(?)".
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.

A method-distinct certificate would be shown beside the rung as a second machine method: a pose-space interval branch-and-bound over (theta, x, y) with the true unit square and weighted atoms, on the pattern of cases/green17/interval_audit.py (note that this certificate is tight, with every row minimum exactly 1 on open cells, so a naive box-splitting audit will not terminate at event lines and needs the semicontinuity argument built in); or, short of that, retain a from-scratch whole-check evaluator (the BC-149, BC-150 or BC-151 scratch evaluators) as a repository case with a replay so the reduction is no longer single-sourced on the record. Rung 5 needs a proof-assistant formalization of the eleven-lemma argument in the BC-150 packet, reviewed by human experts.

Superseded as the verified lower bound on 2026-09-04 by T-019, which certifies 459/100 at $n = 17$ with this project's denser certificate. This result stays true as stated and keeps its rungs; what changed is that the register no longer reads 22529/5000 as the strongest available at this size.
Significance
Raises the verified lower bound at $n = 17$ by 79587/1000000 = 0.079587 over this project's sixteen-point certificate T-001 and closes the gap to the reported record to 0.1697; Massaccesi's result, which this repository replayed, checked by an independent accumulation, and audited lemma by lemma in two reviews.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2
n = 17 register evidence 1 evidence 2
T-019 V3 C3 Levy after Burns, Massaccesi · 2026-09-04 · n = 17–19
$s (n) \geq 459 / 100 = 4.59$ for $n = 17, 18, 19$
Claim and records
Claim
$s (17) \geq 459 / 100$ , and $s (18) \geq 459 / 100$ and $s (19) \geq 459 / 100$ , from this project's weighted fractional unavoidable-set certificate at container side 459/100 = 4.59.

This displaces Massaccesi's 22529/5000 = 4.5058 (T-015) and the two cases T-016 carried from it, all three of which had held that value until 2026-09-04. The movement past the published value is +0.0842 at each of the three sizes.

A stronger public candidate, anabologyco-maker's side 4.5705 (nine thousand one hundred forty-one two-thousandths) of 16 August 2026 (GitHub; not replayed here), was outside the record's search corpus when this was registered and was found on 2026-09-07; it lies 0.0195 below this result. Two rungs are retained below it, 451/100 and 229/50.

The September 2026 DS7 audit identifies a stronger reported n19 bound from Theorem 10 at k=4, approximately 4.6172815, with an unresolved theorem/table discrepancy and missing proof. T-019 does not improve that report; its public source displacement is supported at n17 and n18, while all three certified inequalities and their movements from the prior register remain valid.

The three sizes do not need a monotonicity step. Only Condition 2 mentions n among the five conditions, so an atom set of mass 423327/25000 certifies the side for every integer above it, which is 17 and upward; monotonicity would give the same thing and is not what is used.

It does not improve $n = 20$ , where Nagamochi's 1 + sqrt(13) = 4.6055... is larger -- the certificate does prove $s (20) \geq 459 / 100$ , but that is the weaker statement.
Composition
Primary at all three sizes: one certificate, one accepted verdict, the bound being the container side directly. Its mass 423327/25000 is below seventeen, and Condition 2 is the only condition that mentions n. The same certificate therefore applies directly at n17, n18 and n19; monotonicity would also prove the latter two inequalities but is unnecessary for this certificate.
Next rung
A second machine method decides it, the interval-certified decision, the first here that is not exact-algebraic. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.

The bound itself: the retained certificate's total is 423327/25000 = 16.933080, leaving 0.066920 below seventeen, and that margin is what a further rung has to be found inside.

One figure from the ladder is worth carrying, because it contradicts the obvious reading. Margin is not monotone in the side. The 451/100 rung two below this one has total 16.593620 and margin 0.406380 -- an order of magnitude more headroom at a side 0.08 lower -- and the 229/50 rung between them has margin 0.034265, half of what 459/100 has at a higher side. So the covering value at a given side is set by the site set at least as much as by the side itself, and a better site set at a higher side can open the margin back up rather than close it. The $n = 12$ ladder shows the same shape in the same direction: margin 0.007175 at 197/50, then 0.029410 at the higher 79/20.

Massaccesi's own atoms are the reference point and not a limit: they give a covering value of 203/12 at 4.5058, tight by construction, which bounds nothing about what a different site set reaches at a larger side.

A further rung is therefore a search question, and the quantity to read is the restricted optimum a converged run reaches, never an extrapolated rate.

One such question was asked and answered on 2026-09-04, at $n = 18$ and side 117/25 = 4.68, and it is recorded here as measurement rather than as a claim about tau*. Three site sets in succession -- 538, 578 and 618 orbits -- returned a restricted optimum of exactly 18.000000, the third of them after 157 row-generation rounds that grew the row set from 15888 to 27516 and cost 7056 s. Adding sites can only lower a restricted optimum, and across those three it did not move at all.

Two readings are open and the run did not separate them. Either the covering value at that side is at or above eighteen, in which case no certificate exists there; or the site sets are still short of it and the optimum is sitting on a degenerate vertex, which the collapse of pricing from 90 s to 1--3 s suggests -- a dual that sparse is what a degenerate basis looks like. Exactly round values are the known artefact signature in this pipeline, 18.0 having been one for $n = 17$ 's grid-31 optima, so the second reading cannot be dismissed.

What is not in doubt is the cost of settling it: two hours for the round that did not move. The run was stopped for that reason rather than for its answer, and the side is available to a later block with a cheaper decision path.

The method's own ceiling is not close here. A certificate for n cannot exist above ceil(sqrt(n)) * B, a wider container holding ceil(sqrt(n))^2 pairwise disjoint axis-parallel B-squares whose masses Condition 5 forces past n; for $n = 17$ that is 5B = 4.9885, so 459/100 still has 0.3985 of runway. Unlike $n = 12$ , where the ceiling sits below the conjectured value and forecloses the case, nothing structural stops this one.

Where the next rung is worth spending on, though, is not $n = 17$ . Of the five conditions only Condition 2 mentions n, and the covering program behind the search does not contain n at all -- minimising total mass subject to every admissible B-square carrying mass at least 1 is a question about L, B and the net. So one atom set proves $s (n)$ >= L for every integer n above its mass, this certificate's 16.933080 reaching 17, 18 and 19 directly, and a larger n is strictly easier at the same side.

The headroom said the rest, when this was written. $n = 17$ had 0.0855 to its best known packing at 4.675530; $n = 18$ had 0.2329 to 4.822876 and $n = 19$ had 0.2956 to 4.885618, both still carrying this certificate's side in the verified register; and $n = 20$ had 0.3944 to the trivial 5, holding Nagamochi's closed-form 1 + sqrt(13) = 4.605551. A run at a side whose covering value lands between 17 and 18 would raise $n = 18$ and leave $n = 17$ where it is; one landing between 19 and 20 would displace a published closed form.

The resumed search ran the same day and is registered as T-020, at side 24/5 with retained certificate mass 18.922620, between eighteen and nineteen. It supersedes this result at $n = 19$ and moves $n = 20$ and $n = 21$ as well. What this result still holds alone is $n = 17$ and $n = 18$ : T-020's atoms are too heavy for either, which is the reach rule above read in the other direction. This result stays true as stated at all three of its sizes and keeps its rungs.

For $n = 17$ the reading is unchanged and the runway is 0.3985 to the ceiling and 0.0855 to the packing. For $n = 18$ , T-030 now certifies 4679/1000; T-029's 1871/400 remains as the previous rung. 117/25 remains the open probe this next_rung named.
Significance
Scored against the rubric's anchor for S4, "a reusable technique, bound family, or resolved disputed value". One certificate moves three registered cases, and it replaces a published value rather than an inherited or closed-form one -- the only bound this project has displaced that someone else had put in print.

A stronger public candidate found afterwards, anabologyco-maker's 9141/2000 = 4.5705 of 16 August 2026 (GitHub; not replayed here), was outside the search corpus at scoring time, so the displacement at n17 and n18 is 0.0195 over that public report and 0.0842 over the one this record had adopted. At n19, the DS7 audit now retains a stronger source-reported bound than T-019; its 0.0842 movement refers to the prior register. The family-level score is unchanged.

Held below S5 because none of $n = 17$ , 18, 19 is a central open case, the movement is 0.0842 rather than a qualitative change, weighted resource counting predates this project, the recent pure-atomic rational direction-net architecture follows Burns, the LP parameter line follows Massaccesi, and the case does not change character at the new value.
Novelty
apparently-novel Not found in the recorded search, subject to its stated gaps
Records
n = 17 n = 18 n = 19 register evidence 1 evidence 2
n = 17 n = 18 n = 19 register evidence 1 evidence 2
T-032 V3 C3 Guzhou0806, Mira after Levy, Burns, Massaccesi · 2026-09-21 · n = 17
$s (17) \geq 461300 / 99999 = 4.61304613 \dots$ , and beneath it Mira's $s (17) \geq 4613 / 1000$
Claim and records
Claim
$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.
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.
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.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 evidence 3 evidence 4
n = 17 register evidence 1 evidence 2 evidence 3 evidence 4
T-038 V3 C3 Kleddamag after Levy, Mira, Guzhou0806 · 2026-09-29 · n = 17
$s (17) > 461300 / 99853 = 4.6197910929 \dots$
Claim and records
Claim
$s (17) > 461300 / 99853$ = 4.6197910929..., by Kleddamag's 17-squares-certified-bound v1.0.0 release of 21 September 2026. It raised the verified bound by 0.0067450 over Guzhou0806's R012 (T-032).

The certificate is a mixed point and two-of-three threshold charge, exact, nonnegative and D4-invariant, of budget 16998427356 integer units, over 7,853 contiguous parent-angle intervals, each with a closed core strictly inside every parent, in the container 4613/1000 with parents of side 99853/100000. The minimum core charge 1000020517 gives seventeen cores a surplus of 1921433 over the budget, and compactness makes the bound strict.

It was replayed here in full on 21 September 2026 by the source's two complete checkers, a Python and a JavaScript event-cell sweep, which agreed on all 509 histogram bins; they are one method.

Kleddamag, 17-squares-certified-bound, in the lineage the release names itself: Mira, Guzhou0806 / N17 project, and this repository's threshold-atom work. Its AUTHORS.md says the project was directed by Kleddamag with the research, implementation and verification done by OpenAI Codex.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. Unlike the later releases, this certificate carries only point and two-of-three atoms, which this repository's native parent-core route models, so a complete native run of it is the reachable second machine method, which would be shown beside the rung. No test under packing/tests exercises this packet; the control named is the release's own independent_controls.py, which the 2026-09-21 review used to close the containment and centre-domain premises. Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-09-25 by Guzhou0806's R052 (T-039); stays true as stated.
Significance
Raised the verified lower bound at $n = 17$ by 0.0067 over R012 and brought into the record the mixed point/threshold parent-core architecture every later $n = 17$ rung is built on. Scored as T-015 and T-032 were: a result by others replayed here, on this project's weighted method extended by others.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-039 V3 C3 Guzhou0806 after Kleddamag, Mira, Levy · 2026-09-29 · n = 17
$s (17) > 231001 / 50000 = 4.62002$
Claim and records
Claim
$s (17) > 231001 / 50000$ = 4.62002, by Guzhou0806 / N17 project's R052 release of 25 September 2026. It raised the verified bound by 1142853/4992650000, about 0.000229, over T-038.

The certificate has 2,354 point orbits and 514 two-of-three and 54 three-of-five threshold orbits (18,585 sites) over 15,721 parent-angle intervals, parents of side 230650/231001 in the container 4613/1000. Seventeen cores at the minimum core charge 999426274093 exceed the budget 16990246659579 (units of 10^-12) by 2 units, no slack beyond integer rounding.

It was replayed here in full on 25 September 2026 by the source's Python/Numba and Node/BigInt sweeps, each reproducing the source's own row ledger byte for byte; they are one event-cell method. This repository's native parent-core route verifies every exact premise but refuses the coverage at its engine ceilings.

Guzhou0806 / N17 project, n17-square-packing, on Kleddamag's v1.0.0 mixed point/threshold parent-core architecture (T-038). The release names itself as produced "with AI assistance" and credits Kleddamag, Mira-acc and this repository's threshold lineage.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second machine method needs the native parent-core engine's static ceilings raised past this certificate's 8,937 atoms, 9,261 sites and 44,685 member slots, so that its complete coverage decision can run; its four-row sizing run is not a decision. Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-09-27 by Kleddamag's v1.1.0 (T-040); stays true as stated.
Significance
A substantive case result that held the verified field at $n = 17$ for two days. Its movement, 0.000229, is small, and it adds three-of-five groups under the k-of-m rule already reviewed at $n = 11$ to T-038's architecture. S3 by the T-015 and T-032 precedent, at the low end of it.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-040 V3 C3 Kleddamag after Levy, Mira, Guzhou0806 · 2026-09-29 · n = 17
$s (17) > 232001 / 50000 = 4.64002$
Claim and records
Claim
$s (17) > 232001 / 50000$ = 4.64002, by Kleddamag's 17-squares-certified-bound v1.1.0 release of 26 September 2026. It raised the verified bound by exactly 1/50 over R052 (T-039).

It widens v1.0.0's charge with weighted-threshold features (coefficients 2, 1, 1, 1 at threshold 3) and pairwise-intersecting winning-subset features, every distinct rule of capacity one: 280 point, 155 two-of-three, 26 three-of-five, one four-of-seven, 54 weighted and 30 winning-subset orbits over 2,048 parent-angle intervals, with parents of side 32950/33143 in the container 4613/1000. Seventeen cores at the minimum core charge 998727933 exceed the budget 16978369232 (units of 10^-9) by 5629.

It was replayed here in full on 27 September 2026 by the source's launcher, running its Python and JavaScript BigInt checkers over every interval; they agree with each other and with all three published ledger pairs, and they are one event-cell method.

Kleddamag, 17-squares-certified-bound, building on Squares Project (Joshua Levy), Mira and Guzhou0806, as its ATTRIBUTION.md states. Its AUTHORS.md says the work was produced with AI agents (OpenAI Codex) under Kleddamag's direction.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. This repository's native parent-core route models only k-of-m threshold atoms, so it cannot yet read the weighted and winning-subset features; extending it to them is the reachable second machine method. The only packing/tests control is the retention check of the packet's compressed files; the adversarial control is the source's controls.py, replayed here (eight corrupted certificates rejected by both checkers). Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-09-27 by Kleddamag's 466001/100000 (T-041); stays true as stated.
Significance
Raised the verified lower bound at $n = 17$ by 0.02, with T-041's 0.01999 the largest step of the ladder after R012's 0.02305, and it is the release that introduced the weighted-threshold and winning-subset charge features that 4.66001, R067 and R068 reuse. Those features could argue for S4's reusable technique, but they are others' extension of the weighted method this project banked, so it is held at S3 as T-032 was.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-041 V3 C3 Kleddamag after Levy, Mira, Guzhou0806 · 2026-09-29 · n = 17
$s (17) > 466001 / 100000 = 4.66001$
Claim and records
Claim
$s (17) > 466001 / 100000$ = 4.66001, by the bounds/4.66001/ package of Kleddamag's 17-squares-certified-bound, published untagged on 27 September 2026. It raised the verified bound by exactly 1999/100000 over T-040.

It keeps v1.1.0's checkers byte for byte and combines two completed charge candidates: 224 point, 225 two-of-three, 30 three-of-five, two four-of-seven, 154 weighted-threshold and 254 pairwise-intersecting winning-subset orbits, 7,048 feature images over 20,856 sites, all 86 distinct rules of capacity one, over 2,168 parent-angle intervals with parents of side 461300/466001 in the container 4613/1000. Seventeen cores at the minimum core charge 1000026844 exceed the budget 17000402008 (units of 10^-9) by 54340.

It was replayed here in full on 27 September 2026 by the source's Python and JavaScript BigInt checkers, which agree on every interval and with both published ledger pairs; they are one event-cell method.

Kleddamag, 17-squares-certified-bound, building on Squares Project (Joshua Levy), Mira and Guzhou0806, as its ATTRIBUTION.md states, produced with AI agents (OpenAI Codex) under Kleddamag's direction.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second machine method is not at hand: the native parent-core route cannot read the weighted and winning-subset features, and the review's independent exact sweep, which shares no code with the source and reproduced all 2,168 row minima, was review scratch and is the same method. Retaining that sweep as a repository instrument would make the exact leg this repository's own. Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-09-29 by Guzhou0806's R068 (T-043), which continues this charge; stays true as stated.
Significance
Raised the verified lower bound at $n = 17$ by 0.01999 on T-040's checkers and budget rules, with a larger dictionary of the same features. A substantive case result, S3 by the T-015 and T-032 precedent.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-042 V3 C3 Guzhou0806 after Kleddamag, Mira, Levy · 2026-09-29 · n = 17
$s (17) > 233009 / 50000 = 4.66018$
Claim and records
Claim
$s (17) > 233009 / 50000$ = 4.66018, by Guzhou0806 / N17 project's R067 release of 28 September 2026. R068 (T-043) superseded it the same day, so it never held the case's verified field.

The certificate is Kleddamag's 4.66001 charge (T-041) unchanged, budget 17000402008 units of 10^-9, at the larger parent side 32950/33287, with strict cores rebuilt over 2,808 parent-angle intervals whose endpoints contain every 4.66001 endpoint. Seventeen cores at the minimum core charge 1000026844 exceed the budget by 54340.

It was replayed here in full on 29 September 2026 by the source's paired launcher, Guzhou0806's C++ checker with Kleddamag's Node BigInt checker, and devtools.audit_guzhou_r068 found the fresh and published ledgers identical on all 2,808 rows; the two checkers are one event-cell method.

Guzhou0806 / N17 project, n17-square-packing, on Kleddamag's charge. The release names itself as made "with AI assistance".
Next rung
No rung change is sought: the result never held a field, and a method-distinct decision would be spent better on R068, which runs the same charge further. Superseded on its publication day, 2026-09-28, by Guzhou0806's R068 (T-043), before it held the verified field; stays true as stated.
Significance
True and replayed in full, but superseded on its publication day by R068 before it held any field: a citable intermediate, +0.00017 over T-041, that changes no standing bound. Registered because it was replayed and reviewed here.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 source review
n = 17 register evidence 1 source review
T-043 V3 C3 Guzhou0806 after Kleddamag, Mira, Levy · 2026-09-29 · n = 17
$s (17) > 116511 / 25000 = 4.66044$
Claim and records
Claim
$s (17) > 116511 / 25000$ = 4.66044, by Guzhou0806 / N17 project's R068 release of 28 September 2026, continuing Kleddamag's public 4.66001 charge (T-041). It raised the verified bound by exactly 43/100000 over T-041 and leaves 0.0150901 to Bidwell's 4.67553009.

The 889 rule orbits and their weights are 4.66001's byte for byte; one zero-weight site orbit moves by 1/12500 and one weighted four-site point orbit is added, for a budget of 17000448944 units of 10^-9, and the strict cores are rebuilt over 4,991 parent-angle intervals with parents of side 115325/116511 in the container 4613/1000. Seventeen cores at the minimum core charge 1000026844 exceed the budget by 7404.

It was replayed here in full on 28 and 29 September 2026, the first local validation on record: the package says its publisher ran no local validation and did not observe its CI. Guzhou0806's own C++ checker and Kleddamag's Node BigInt checker ran over every interval, and devtools.audit_guzhou_r068 found the fresh and published ledgers identical row for row; the two checkers are one event-cell method.

Guzhou0806 / N17 project, n17-square-packing. The package credits Kleddamag for the charge, the proof and the Node BigInt checker (Kleddamag building on Squares Project (Joshua Levy), Mira and Guzhou0806), and discloses AI assistance.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained; the mapped 2026-09-28 review is not recorded in this entry's reviews, and whether it counts is the owner's decision. The native parent-core route models only k-of-m threshold atoms and cannot read the weighted and winning-subset features, so extending it to them is the reachable second machine method. The review's code-independent exact sweep reproduced nine sampled rows; completing and retaining it would make the exact leg this repository's own but is the same method. Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-10-05 by Guzhou0806's R071 (T-093), which keeps this charge; stays true as stated.
Significance
The case's verified lower bound, +0.00043 over T-041 from one added point orbit on an unchanged charge and a finer catalogue. A substantive case result at S3 by the T-015 and T-032 precedent; the movement is small, and this repository's replay is the first local validation of it on record.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
T-065 V3 C3 Kleddamag after Levy, Mira, Guzhou0806 · 2026-10-01 · n = 17
$s (17) \leq 4.6755300936045509 \dots$ , Bidwell's packing certified exactly
Claim and records
Claim
$s (17) \leq 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) \leq 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.
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.
Significance
The first verified upper bound at $n = 17$ below the grid's 5: the case's verified bracket becomes 4.66044 < $s (17) \leq 4.67553009 \dots$ , 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.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
T-085 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
T-093 V3 C3 Guzhou0806 after Kleddamag, Mira, Levy · 2026-10-05 · n = 17
$s (17) > 18641771 / 4000000 = 4.66044275$
Claim and records
Claim
$s (17) > 18641771 / 4000000$ = 4.66044275, by Guzhou0806 / N17 project's R071 release of 30 September 2026, on the charge of R068 (T-043). It raised the verified bound by exactly 11/4000000 over T-043's 116511/25000 and leaves 0.0150873 to Bidwell's 4.67553009.

The certificate keeps every point orbit, rule orbit and weight of R068, and its budget of 17000448944 units of 10^-9, and rebuilds every strict core for the smaller parent side 18452000/18641771 in the container 4613/1000, over 5,114 parent-angle intervals that refine R068's 4,991. The source reports a least core charge of 1000026844 over all 5,114 intervals, so seventeen cores exceed the budget by 7404. It refines R070 of the day before, $s (17) > 46604427 / 10000000$ = 4.6604427 over 5,107 intervals, which it supersedes.

It was replayed here in full on 5 October 2026, the first replay of it outside its source: the source retains a completion summary of its own run and says the row records are missing, and its GitHub Actions replay passed unobserved by its publisher. The source's run_public.js ran Guzhou0806's C++ checker and Kleddamag's Node BigInt checker over every interval, and devtools.audit_guzhou_r071 found the two fresh ledgers identical row for row, every row at 1000026844; the two checkers are T-043's byte for byte and one event-cell method. Both refuse two mutated certificates.

Guzhou0806 / N17 project, n17-square-packing, on R068's continuation of Kleddamag's 4.66001 charge. The package credits Kleddamag for the 4.66001 framework, proof and BigInt checker (Kleddamag building on Squares Project (Joshua Levy), Mira and Guzhou0806), and discloses AI assistance.
Next rung
V4 and C4 need a second adversarial AI review by a distinct reviewer and a human oversight record, as T-043's next_rung says; a second machine method needs the native parent-core route to read the weighted and winning-subset features, which it still cannot. The r071-bound artifact of the source's CI run, which expires on 2026-12-29 and could not be fetched here, holds a third ledger that could be compared row by row with the fresh ones; it would add a comparison, not a rung. R070's obstruction puts the reach of this charge below 186417711/40000000 (review RF-7), so a higher bound needs a new charge or an argument across parents. Rung 5 needs a proof-assistant formalization reviewed by human experts.
Significance
The case's verified lower bound, 2.75 x 10^-6 above T-043 from T-043's charge unchanged, a finer catalogue and rebuilt cores: the construction of T-042, which is S2, adding no orbit, rule, weight or method. T-043's step was 156 times this one and T-039's, the S3 precedent the draft weighed, 83 times; R070's obstruction shows the charge cannot reach 1/40000000 further, so this is the end of a recipe rather than an opening. Holding the verified field is a fact about the frontier, not the claim; a reader who weighs it above the size of the step would score S3 by T-039, and the score gates nothing.
Novelty
previously-published Present in an identified source
Records
n = 17 register evidence 1 evidence 2 source review
n = 17 register evidence 1 evidence 2 source review

Verification

upper: audited here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 5 of the retained witness (witness id 6) translates 0.071507 along (-0.707107, 0.707107) with the packing still valid, so the configuration admits a non-trivial feasible motion; 2 of its 17 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.

Open questions

Blocker (mathematics): The certified endpoint is feasible and its side is the root of the catalogue's degree-18 polynomial (exp-245, 2 October 2026); global optimality is not established. E-n017-certified-endpoint, E-n017-catalogue-polynomial-identity
Blocker (source evidence): MacIver's historical n17 claim needs the fourteen C1-C14 certificates, exact ledger and theorem-assembly scripts, and their complete replay; those artifacts are absent from the inspected public source commit. E-n017-maciver-reported-lower
Blocker (source evidence): The complete source checker has not been independently replayed here. E-n017-anabologyco-weighted-certificate
Priority: The manuscript dated 8 August 2026, '[MacIver 2026 n17]', reports s(17) > (40sqrt(2)+19)/17 + 1/200, approximately 4.450208382054341, through conditional counting on a deformed Green scaffold. This historical source claim is weaker than the independently verified 459/100 and has not been replayed here. (David R. MacIver)

Evidence and sources

35 evidence entries

[Kingbird] record catalogue
[Nagamochi 2005] lower bound proof
[Guzhou0806 n17 R071] lower bound proof
[Guzhou0806 n17 R070] context
[Guzhou0806 n17 R068] lower bound proof
[Guzhou0806 n17 R067] context
[Burns–Massaccesi n17] lower bound proof
[GitHub n17 certificates 2026] lower bound proof
[Kleddamag n17 4.66001] lower bound proof
[Kleddamag n17 4.640020] lower bound proof
[Kleddamag n17 certified bound] lower bound proof
[Guzhou0806 n17 R052] lower bound proof
[Guzhou0806 n17 R050] context
[Guzhou0806 n17 R043] context
[Guzhou0806 n17 R042] context
[Guzhou0806 n17 R052 continuation] context
[Guzhou R038 2026] lower bound proof
[ahyangyi 17squares v1.1.1] lower bound proof
[Friedman DS7] survey
[MacIver 2026 n17] lower bound proof
[n17 weighted certificates 2026-09-20] lower bound proof

In the frontier survey On GitHub

$s (17)$ — open

$s (17) \leq 4.6755300936045509516342148538535054$ is now certified by exact identities and rational interval bounds. The reported record, $4.67553009360455 \dots$ , was found by John Bidwell in 1998, building on a packing of Hämäläinen’s from 1980. The certified packing’s side is exactly that record: it is the root of the catalogue’s degree-18 polynomial, which is irreducible over $ℚ$ (exp-245; until 2 October 2026 this page recorded that identity as unproved), and the decimal above is a rational outward ceiling on it. The verified lower bound is the strict inequality $s (17) > 18641771 / 4000000 = 4.66044275$ , from Guzhou0806 / N17 project’s R071 release, published on 30 September 2026 and replayed here on 5 October, $11 / 4000000$ above R068’s $116511 / 25000$ , whose charge it keeps. R071 keeps every point orbit, rule orbit and weight of R068 and rebuilds every strict core over $5, 114$ orientation intervals, with parents of side $18452000 / 18641771$ in the same container $4613 / 1000$ . The budget stays $17000448944$ units of $10^{- 9}$ , and the counting surplus stays $17 \times 1000026844 - 17000448944 = 7404$ . The package credits Kleddamag for the $4.66001$ framework, proof and BigInt checker, and discloses AI assistance; its publisher checked file identities and saved records only, its row-level records are missing, and its CI replay passed unobserved, so the replay here is its first independent check. Both of its checkers ran here over every interval, Guzhou0806’s own C++ checker and Kleddamag’s Node BigInt checker, the bytes R068’s replay here ran, and agree with each other on every interval minimum and cell count, every row at $1000026844$ ; both refuse two mutated certificates. This supports V3/C3 on one machine method: the two sweeps are one event-cell method, and this repository’s native parent-core route models only $k$ -of- $m$ threshold atoms, so it cannot yet read the weighted and winning-subset features and gives no method-distinct decision. The proof review found no mathematical defect, re-derived every premise the new parent side and cores touch, and reproduced 227 rows of the replay’s ledger with a sweep sharing no code with the source; the two steps the source’s proof asserts are proved in the review of R067 and R068, and neither uses the parent side. R070’s obstruction shows this charge cannot prove a bound $1 / 40000000$ higher, so a further step needs a new charge. The gap to the catalogue’s printed record is $0.01508734360455$ .

The previous verified lower bound was $116511 / 25000 = 4.66044$ , from Guzhou0806 / N17 project’s R068 release, published on 28 September 2026 and replayed here that night, $43 / 100000$ above Kleddamag’s $4.66001$ , whose charge it continues. R068 keeps that charge’s $889$ rule orbits and their weights unchanged, moves one zero-weight site orbit by $1 / 12500$ , adds one weighted four-site point orbit on the diagonal at $(1.34, 1.34)$ , and rebuilds the strict cores over $4, 991$ orientation intervals, with parents of side $115325 / 116511$ . Its two checkers, the same as R071’s, ran here over every interval and agree with each other and with the published ledgers. The same day’s R067, $233009 / 50000 = 4.66018$ , ran the $4.66001$ charge unchanged at parent side $32950 / 33287$ over $2, 808$ intervals; it was replayed here in full too and never held the verified field. R070 of 29 September, $46604427 / 10000000 = 4.6604427$ over $5, 107$ intervals, is the release R071 refines; it was never replayed here and never held the verified field.

Before R068 the verified lower bound was $466001 / 100000 = 4.66001$ , published on 27 September 2026 and replayed here the same day. Kleddamag, building on Squares Project (Joshua Levy), Mira and Guzhou0806: an exact weighted-certificate proof over 2,168 orientation intervals. That is the lineage the release’s own ATTRIBUTION.md states — this project’s weighted-covering, strict-core, event-cell and threshold-budget methods, Mira’s 17squares support and parent-angle catalogue, and R038’s parent-side reduction — and the release claims no invention of those methods and says that attribution implies no upstream coauthorship or endorsement. Its AUTHORS.md says the work was produced with AI agents (OpenAI Codex) under Kleddamag’s direction. It keeps Kleddamag’s parent-core architecture — container side $4613 / 1000$ , here with parents of side $461300 / 466001$ — and combines two completed charge candidates: $224$ point orbits, $225$ two-of-three, $30$ three-of-five and two four-of-seven threshold orbits, $154$ weighted-threshold orbits in four coefficient patterns and $254$ pairwise-intersecting winning-subset orbits on three to ten sites, $7, 048$ feature images in all over $2, 620$ site orbits ( $20, 856$ sites). Every one of its $86$ distinct rules has capacity one. Both of the source’s complete checkers, a Python sweep in rational arithmetic and a JavaScript BigInt sweep, are the v1.1.0 engines byte for byte; they ran here over every interval and agree on every interval minimum and cell count. The counting surplus is $17 \times 1000026844 - 17000402008 = 54340$ units of $10^{- 9}$ . This supports V3/C3 on one machine method: the two sweeps are one event-cell method, and this repository’s native parent-core route models only $k$ -of- $m$ threshold atoms, so it cannot yet read the weighted and winning-subset features and gives no method-distinct decision. The proof review is a separate record, docs/project/reviews/review-2026-09-27-n17-kleddamag-466001.md. R068 exceeds it by exactly $43 / 100000 = 0.00043$ .

Before that the verified lower bound was $232001 / 50000 = 4.64002$ , from Kleddamag’s v1.1.0 release of 26 September 2026, replayed here on 27 September: Kleddamag, building on Squares Project (Joshua Levy), Mira and Guzhou0806, on the same lineage. It widened Kleddamag’s own v1.0.0 charge dictionary to $280$ point orbits, $155$ two-of-three, $26$ three-of-five and one four-of-seven threshold orbit, $54$ weighted-threshold orbits (coefficients $2, 1, 1, 1$ , threshold $3$ ) and $30$ pairwise-intersecting winning-subset orbits over $2, 048$ angle intervals, with parents of side $32950 / 33143$ and a counting surplus of $17 \times 998727933 - 16978369232 = 5629$ units of $10^{- 9}$ , also at V3/C3. Its review found no mathematical defect. Its AUTHORS.md says Kleddamag directed the work and that separate OpenAI Codex research tasks constructed and exactly checked the $4.640020$ certificate. The $4.66001$ bound exceeds it by exactly $1999 / 100000 = 0.01999$ .

Before v1.1.0 the verified bound was $231001 / 50000 = 4.62002$ , from the R052 release of Guzhou0806 / N17 project, published on 25 September 2026 and replayed and reviewed here the same day. R052 was produced with AI assistance on Kleddamag’s v1.0.0 mixed point/threshold parent-core architecture and extends Guzhou0806’s own R050 with enlarged resources: $2, 354$ point orbits and $514$ two-of-three and $54$ three-of-five threshold orbits ( $18, 585$ sites, $4, 504$ groups, $2, 922$ columns) over $15, 721$ angle intervals. Its SOURCE_NOTICES.md says Guzhou0806 / N17 project used AI assistance for exploration, implementation, computation, checking and documentation, with non-proposer AI review in its final local acceptance, and names Mira-acc/17squares and Joshua Levy’s squares project in its method lineage. The source’s Python/Numba and Node/BigInt sweeps both ran here over every interval, and each reproduced the source’s own row ledger byte for byte. The counting surplus is $17 \times 999426274093 - 16990246659579 = 2$ units of $10^{- 12}$ , no slack beyond integer rounding. That too is V3/C3 on one machine method: the native interval route verifies every exact premise but refuses the coverage at its engine ceilings. Its review found no mathematical defect. Kleddamag’s v1.1.0 exceeds it by exactly $1 / 50 = 0.02$ .

Before R052 the verified bound was $461300 / 99853 = 4.619791092907 \dots$ , from Kleddamag’s v1.0.0 release, replayed and reviewed here on 21 September 2026. Its complete Python and JavaScript scans cover all $7, 853$ parent-angle intervals, agree on all $509$ histogram bins, and give $17 \times 1000020517 - 16998427356 = 1921433$ integer units of counting surplus, also at V3/C3. R052 exceeds it by $1142853 / 4992650000 \approx 0.000229$ . Its AUTHORS.md says Kleddamag initiated and directed the project and OpenAI Codex performed the mathematical exploration, the searches and checks, and the certificate and proof. Before that, the verified bound was $461300 / 99999 = 4.61304613 \dots$ , from Guzhou0806’s R012 parent-angle certificate of 20 September 2026 (T-032), which remains valid historical evidence at V3/C3, confirmed by two machine methods: the source’s own checker re-run, and an independent re-implementation here.

R012 uses this repository’s weighted method with three changes and was the first external certificate to supply this case’s verified bound. Instead of covering every closed $B$ -square, it covers only what a real parent needs: squares of side $A = 99999 / 100000$ inside $[0, 4613 / 1000]^{2}$ , with the bound $L / A$ recovered by rescaling at the end. A catalogue of $2925$ closed parent-angle intervals covers $[0, π / 4]$ , and each interval chooses its own concentric closed core — its own direction and its own side — strictly inside every parent of that interval. Coverage is then required only over the legal parent-centre square for the interval, which is smaller than the set of all contained cores, and that restriction is what the extra strength buys: five placements the source retains as counterexamples fail the unrestricted test and pass this one. The measure is $1616$ atoms in $206$ D4 orbits of total mass $424969 / 25000$ , every core captures at least $γ = 250023 / 250000$ , and $17 γ$ exceeds the mass by $701 / 250000$ . It is decided at V3/C3 by two methods that fail differently: the source’s own exact event-cell checker, which recomputed all $2925$ intervals here over $9, 231, 165$ centre strips, and this repository’s interval branch and bound, which certified the same $2925$ entries over $34, 465, 227$ boxes with none stalled and every bracket containing the exact minimum. The catalogue minimum is exactly $γ$ , so there is no slack anywhere: raising the threshold by one part in $10^{6}$ at an entry that attains it is refused.

Beneath it sits the certificate R012 is built on, which was the strongest value on record until R012 passed it thirteen days later. Mira’s weighted certificate of 7 September 2026 gives $s (17) \geq 4613 / 1000 = 4.613$ on $1620$ atoms of mass $849899249 / 50000000$ , core side $19997 / 20000$ and a $2880$ -step direction net, with least covered mass $1000002103 / 1000000000$ . It is written in this repository’s own certificate schema — it starts from the T-019 atoms and retains that file unchanged — so both stock verifiers decide it with no translation layer, and both accept it: the exact sweep finds that least value at net direction $2194$ , and the interval route pins it on the doubled $5761$ -direction net to a zero-width enclosure at the same rational. Mira’s own headline is larger, the dilation endpoint $4.61302863588611 \dots$ , but that step needs a T-022-style proof note this certificate does not carry, so the record holds the container side. Nothing is lost: R012’s value is larger still.

Both results descend from this repository’s T-019 and credit it, and both disclose model assistance and claim neither peer review nor priority. R012’s ATTRIBUTION.md names it as research by “Guzhou0806 / N17 project, with AI assistance”, and Mira’s paper says its earlier computation and exposition “were developed with assistance from OpenAI’s GPT-5.6 Pro under human direction” and that the September patch and its integration also used AI assistance. Mira’s certificate was published hours after the 7 September GitHub check that built the earlier packet, which is why neither was in the record until 20 September. The two are separate results with separate premises: R012 recomputes every obligation on its own measure and does not depend on Mira’s certificate being valid. What the machines do not decide is the reduction from a packing to R012’s $2925$ finite obligations — the angle folding, the endpoint containment test, the union of centre squares, the counting and the rescaling. Those were read line by line in the proof review, which found no error and supplied two steps the source’s note omits.

Weaker bounds are kept for their provenance rather than their strength. This repository’s own T-019, $s (17) \geq 459 / 100 = 4.59$ of 2026-09-04, held the case until R012 displaced it: 1184 rationally weighted atoms of total mass $423327 / 25000$ , least covered mass $200009 / 200000$ , decided by the same two verifiers. It is still the ancestor of everything above it, and it still holds $n = 18$ and $n = 19$ in company with the certificates that have since passed it there. Gustavo Massaccesi’s August 2026 certificate ([Burns–Massaccesi n17], T-015) gave $22529 / 5000 = 4.5058$ — 168 rationally weighted atoms of total mass $203 / 12 < 17$ , reduced exactly to 181 rational directions and $16, 562, 293$ event cells — and held this case from 2026-09-03 until T-019 displaced it a day later. It is source-backed, from a blog post by Massaccesi, who marks the value “(?)”; it is replayed here twice, by the retained source verifier and by an accumulation-independent repository instrument that agrees on every direction cell (H-052, exp-059), with the argument audited lemma by lemma (BC-150 packet, BC-151 review). It is also the control that tests this repository’s verifiers rather than its certificates, and it still is. Massaccesi’s certificate re-parametrises Sam Burns’s note of 6 August 2026, which proposed the side $44811 / 10000 = 4.4811$ on 268 atoms of total mass $16.9476$ with least covered mass $10003 / 10000$ , and whose verifier is the one Massaccesi modified; that verifier replays here unchanged (E-n017-burns-source-replay, 7 September 2026), the repository’s exact sweep accepts the same atoms re-encoded as a control (E-n017-burns-control-decision, a published control whose least covered mass is not exactly $1$ ), and its rung sat between Brandwijk’s $89 / 20$ capsule of 18 July and Massaccesi’s value for a fortnight. The note’s byline is “ChatGPT (GPT-5.6 Pro, OpenAI)”; Burns’s post says the model “developed the certificate during this project” and that he operated it. Burns’s companion post describes a near-record arrangement at side $4.677648$ , $0.002118$ above Bidwell’s, with eleven axis-aligned squares and six at a common tilt of ${39.6319}^{\circ}$ , a contact topology he reports as distinct from Bidwell’s; the coordinates are retained under resources/web/burns-n17-series-addendum-2026-09-07/, and the contact graph has not been reconstructed here. Below it, the repository’s own sixteen-point certificate — cases/green17, $s (17) \geq 4.426213$ , T-001, certified by the Bentz-lemma cell certificate and an independent interval branch-and-bound — was previously the second strongest and remains a first-party theorem confirmed by two methods, its producer’s code re-run and an independently re-implemented interval audit, above Nagamochi’s general $4.162278$ and a hair below Green’s reported but sourceless $(40 \sqrt{2} + 19) / 17 \approx 4.4452$ . Certifying the sixteen-point set at its exact ceiling $753 / 250 + \sqrt{2} \approx 4.42621356$ is a typed follow-on (think-iye2). Green’s own sixteen points, which DS7’s Figure 34 calls unavoidable at his value, are not: a closed unit square in the container misses all of them by $0.00545$ , so the figure proves no bound above about $4.3978$ (review). An earlier audit catalogued eight public lower-bound postings for this size between 18 July and 21 August 2026, and the record’s indexed corpus held three of them. Kim Brandwijk’s Zenodo capsule of 18 July gave $89 / 20 = 4.45$ from an exact sixteen-point set; Burns’s note of 6 August gave $44811 / 10000 = 4.4811$ . Three GitHub repositories followed, none of them in the indexed corpus until the 7 September 2026 check that found them ([GitHub n17 certificates 2026]): Mira’s first version on 10 August at $4.450837$ , Stanislav Fort’s on 11 August at $4.456575$ , and Mira’s second on 11 August at $4.468292$ . Those three are exact sixteen-point certificates on one architecture — the pose space subdivided in integer arithmetic into point, piercing and infeasible leaves — and they are the strongest integral sixteen-point bounds on record, above both Brandwijk’s capsule and cases/green17; Mira’s and Fort’s replay here under their own Python checkers (E-n017-mira-point-certificate-replay, E-n017-fort-point-certificate-replay). anabologyco-maker’s repository followed with $4.57$ on 13 August and the side $9141 / 2000 = 4.5705$ on 16 August: 560 weighted atoms on the $1 / 4000$ grid, decided not over a direction net but over an exact orientation partition of $148, 937$ cells, with a Lean 4 layer over the finite checks. It is source-backed only — its decisive Sturm, endpoint and coverage stages need Boost and its Lean layer needs Lean 4.33, neither available here (E-n017-anabologyco-weighted-certificate) — and it was the strongest public value on record until Mira’s certificate of 7 September passed it. Massaccesi’s $22529 / 5000$ closed the sequence on 21 August. Corrected 2 October 2026: Nagamochi’s value is now a reported bound, his Lemma 1 being false (Karakuş 2026; review). This register had recorded that proof as verified, its own error, logged as defect D-516.

Later public claims improved on the historical R012 value $461300 / 99999$ .

Guzhou0806’s R038 certificate, in the same repository, reports the strict lower bound $461300000000 / 99974999999 = 4.614153538431 \dots$ . Its complete published proof, checker, source pin and source-result files are now retained in the Guzhou source tree. That release keeps its required Mira numerical certificate external, identified by SOURCE_PIN.json; retaining the tree does not replay the geometric obligations. No local complete R038 replay is claimed, and the verified field does not rely on it.

Kleddamag’s $461300 / 99853 = 4.619791092907 \dots$ , the v1.0.0 release, was the verified bound from 22 to 25 September 2026 and is now the previous one. Its bytes are retained here, a full two-checker replay reproduced its published RESULT.json byte for byte, and the review found no blocking defect. The verified field recorded that result through E-n017-kleddamag-461300-99853-source-replay, which remains valid evidence. The decision before 22 September to wait for a method-distinct checker was an admission-policy error: the complete rigorous replay and discharged proof assumptions already supported a verified bound at C3. The replay date remains 21 September; no new full replay was run for that record correction on 22 September.

The packet retains the source’s manifest-bound result bytes, and Session 150 and the review attest that the local run reproduced them. A separately named local raw replay directory was not retained; the source outputs are not relabelled as local receipts. T-032 keeps its original R012 statement and evidence; adopting the stronger external bound neither rewrites that result nor creates a new theorem identifier.

Guzhou0806 then published three releases on Kleddamag’s architecture, each numerically superseded by R052 and each retained here only as a publication record in the R052 packet, none replayed: R042 on 23 September ( $115325 / 24963 \approx 4.619837$ ), R043 the same day ( $461300 / 99851 \approx 4.619884$ ), and R050 on 24 September ( $4613000 / 998509 \approx 4.619888$ ). R052’s geometry is R050’s, uniformly rescaled, with five of R050’s $15, 706$ angle rows each split into four. The complete R052 package, its four replay receipts and the native route’s refusal are retained here, and the verified field records the result through E-n017-guzhou-r052-source-replay. As with Kleddamag’s bound, no new theorem identifier is created. Deciding the certificate natively needs the interval engine’s atom, site and member-slot ceilings raised in a new proof commit; a sizing run on four of its rows prices the full run at roughly 8 to 49 CPU-hours, an estimate and not a decision.

Kleddamag’s v1.1.0 release of 26 September 2026 then raised the bound to $232001 / 50000 = 4.640020$ . Its new package, bounds/4.640020/, carries the certificate, a proof and method note, a general-rule Python checker and a separately written JavaScript BigInt checker, a controls script, and the source’s own receipts; the v1.0.0 files are unchanged in the same tree. The release measures its advance against its own $4.619791 \dots$ , not against R052, and states that no code from R052 was used. The packet retains every file that changed or was added since v1.0.0, and the verified field records the result through E-n017-kleddamag-4640020-source-replay. As with the earlier external bounds, no new theorem identifier is created. Its budget rules go beyond the architecture reviewed on 21 and 25 September: a weighted threshold charges at most $⌊ Σ a_{i} / k ⌋$ disjoint cores, and a winning-subset feature whose listed subsets pairwise intersect charges at most one. Deciding it natively needs the parent-core route to represent both feature kinds before any coverage engine question arises.

A later revision of the same repository, of 27 September 2026 and not yet tagged (its changelog lists it as unreleased), then raised the bound to $466001 / 100000 = 4.66001$ in a new package, bounds/4.66001/. Its checkers and their shared modules are the $4.640020$ bytes; only the launcher’s target and interval count and the controls’ target and sampled intervals change. The certificate combines completed charges from two separate research tasks and subdivides eight of an original $2, 048$ intervals sixteen ways with regenerated strict cores, keeping the charge fixed. Its embedded source string still reads “exact diagnostic pending”, which the release explains as preserved text from an earlier construction stage, kept so that the certificate file is unchanged. The packet retains every file that changed or was added since v1.1.0, and the verified field records the result through E-n017-kleddamag-466001-source-replay. No new theorem identifier is created. The feature kinds and budget rules are the ones v1.1.0 introduced, on many more orbits: the weighted thresholds now include coefficients $2, 1, 1, 1, 1, 1$ at $4$ , $2, 1, 1, 1, 1, 1, 1, 1$ at $5$ and $4, 1, 1, 1, 1, 1$ at $5$ , each still firing at most once on disjoint cores, and the winning-subset rules run on three to ten sites.

Guzhou0806 / N17 project’s R067 and R068 packages, published on 28 September, are retained with complete paired replays of both in their packet. The verified field recorded R068 through E-n017-guzhou-r068-source-replay from 29 September to 5 October, and R067, the intermediate, is recorded through E-n017-guzhou-r067-source-replay. As with the earlier external bounds, no new theorem identifier is created. R068 also ships the C010 research material: a shifted-core strip sweep and an exact counterexample to a separate charge aimed at $9321 / 2000$ , which the source says is not a global bound and which carries none here.

Guzhou0806 / N17 project’s R070 and R071, published on 29 and 30 September, are retained in their packet, with the complete paired replay of R071 here and its two mutated-certificate controls. The verified field records R071 through E-n017-guzhou-r071-source-replay; R070 has no entry and was not replayed. Both keep R068’s charge exactly — every point orbit, rule orbit and weight, the budget $17000448944$ and the requested minimum — and rebuild every strict core for a smaller parent. R070 claims $46604427 / 10000000 = 4.6604427$ over $5, 107$ intervals that refine R068’s $4, 991$ , and publishes complete four-partition C++ and BigInt ledgers, which agree row by row here: every interval at minimum $1000026844$ , surplus $7404$ . R071 is built on R070’s certificate, bisects seven of its intervals, and claims $18641771 / 4000000 = 4.66044275$ over $5, 114$ ; its row-level records are missing, as the source says, and a completion summary of a three-partition run reports the same minimum and surplus and names the BigInt checker and launcher bytes R068’s replay here ran. The replay here regenerated both ledgers: the two agree on every row, every row at minimum $1000026844$ , $2, 263, 809, 819, 494$ cells in all. The source’s own GitHub Actions replays of both passed; their publisher, which discloses AI assistance, did not observe them. Neither release’s other material carries a bound: R070’s same-budget overlay of $319$ orbits and its obstruction at one parent within a fixed-weight enhancement class, and R071’s conditional joint geometry at $9321 / 2000$ inside one first-anchor box, which the source says does not prove $s (17) > 4.6605$ .

Three other public reports are recorded without carrying a bound here. ahyangyi’s 17squares v1.1.1 of 23 September reports $184547267428061 / 40000000000000 \approx 4.6136817$ , below R038 and below the verified bound; its author’s commit message says it is not frontier any more, and it is not retained. Kleddamag’s untagged v1.2.0 of 29 September reports $46601 / 10000 = 4.6601$ , its $4.66001$ charge unchanged over $2, 543$ intervals, with a research checkpoint of conditional exclusions and unfinished routes that claims no bound; it is below R067 and below the verified bound, asks for no work, and is not retained. R052’s source also reports that Kleddamag holds an unpublished internal strict bound of $4.62001$ . That is second-hand, below R052 and unverified, and it is not recorded here as a bound.

Guzhou0806’s R052 continuation, published on 25 September, claims $s (17) > 462003 / 100000 = 4.62003$ from R052’s sites moved by an exact D4-symmetric deformation and two more angle rows split four ways ( $15, 727$ rows, surplus again 2 units). Kleddamag’s public $232001 / 50000 = 4.64002$ of 26 September supersedes it, so it is kept only as a publication record in its own packet, with local receipts for its records, containment and new C++ full replay. That C++ kernel runs the same exact event-cell sweep as the source’s Python and Node/BigInt checkers, so it is not a method-distinct decision.

An additional source, David R. MacIver’s manuscript dated 8 August 2026, reports $s (17) > (40 \sqrt{2} + 19) / 17 + 1 / 200 \approx 4.450208382054341$ by deforming Green’s sixteen-point scaffold and using conditional counting. The archived source review retains the paper at its public 10 August commit, together with his center-area and center-count manuscripts. The n17 claim is historical and source-reported: the public Lean file proves supporting algebra, while the fourteen certificate files and exact ledger/assembly scripts needed for the full bound are absent from the inspected snapshot. The operative verified lower bound is Guzhou0806’s strict R071 bound $18641771 / 4000000$ described above; the MacIver claim remains historical and source-reported.

Certified Endpoint Upper Bound

The exact root and centroid construction certify 17 unit squares in a square of side at most $4.6755300936045509516342148538535054$ . This is a rational outward ceiling, not a claim that the endpoint side equals that decimal. The endpoint review records all 68 wall and 136 pair obligations and an independent exact interval audit. It improves the earlier rational witness at $4675530093604551 / 10^{15}$ , which remains a verified fallback.

The upper ceiling agrees with Bidwell’s catalogue decimal at its printed precision, and since 2 October 2026 the side is identified exactly. The chart polynomials’ resultant has one irreducible degree-18 factor with a root at the certified point, and mapped to the side it is the catalogue’s polynomial with unit 1 (H-265, exp-245, output review). The certified side is therefore Bidwell’s algebraic number $S^{*}$ , and the decimal is a ceiling on it. Neither result proves a global minimum. The lower bound remains strictly below it, so status remains open.

The attempt to prove $s (17) = S^{*}$ follows the local half, global half and capture that settled $n = 11$ . Each part and the evidential status of each claim are explained in The n = 17 Optimality Proof, Explained. None of it moves a bound or the status.

Three orientation classes, and a correction

This is the smallest case whose best known packing uses squares at three different angles, a distinction frequently misattributed to $n = 11$ (which uses two: axis-aligned and $\approx {40.182}^{\circ}$ ). Bidwell’s packing uses the unequal nonzero orientations $+ {39.8049589798}^{\circ}$ and $- {36.6237863834}^{\circ}$ , not the symmetric shorthand $\pm 40^{\circ}$ previously stored here. Those values are transcribed from the analytic entities in the primary Kingbird SVG. The certified endpoint is a separate exact reconstruction. Its side is the catalogue’s degree-18 root (exp-245); that its configuration is the pictured packing, contact for contact, has not been established.

Degree 18

The catalogue reports a side length algebraic of degree 18 — more than twice the degree at $n = 11$ , and a useful calibration on how fast algebraic complexity grows once the contact graph stops being simple. Gensane and Ryckelynck derived it from a four-equation system of degree 7 in $\cos θ_{1}, \cos θ_{2}, \sin θ_{1}, \sin θ_{2}$ , and observed that Friedman’s rounded $4.6755$ “seems to be false.”

Their reported decimal and the catalogue’s differ from the ninth decimal onward ( $4.6755300960455$ versus $4.67553009360455$ ). Direct evaluation resolves the numerical discrepancy in favour of the catalogue: the stored degree-18 polynomial has a root $4.6755300936045509516 \dots$ , within $9.52 \times 10^{- 16}$ of the catalogue decimal, while the reported decimal is $2.44 \times 10^{- 9}$ away and gives polynomial residual about $56.9$ . The remaining source question is whether the paper has a decimal transcription slip or intended a different equation. Since 2 October 2026 the certified endpoint’s side is identified with that root exactly (exp-245). The polynomial is irreducible over $ℚ$ , by factorization and by Rabin tests at four primes in the independent review. $S^{*}$ therefore has algebraic degree 18, with this polynomial as its minimal polynomial; the review encloses $S^{*} = 4.6755300936045509516341112704831466487671 \dots$ to width $10^{- 40}$ .

Why it matters downstream

$s (17)$ is a workhorse: the catalogue records several larger records — $s (83)$ , $s (84)$ , and others — as extensions of Bidwell’s packing. An error in it would propagate.

Reported Lower Bound

The reported lower bound is Guzhou0806’s strict R071 bound $s (17) > 18641771 / 4000000 = 4.66044275$ , on R068’s continuation of Kleddamag’s $4.66001$ charge (retained packet), and since its complete paired replay here on 5 October 2026 it is the verified bound too, described above. R068’s $116511 / 25000$ , R070’s $46604427 / 10000000$ , Kleddamag’s $466001 / 100000$ , its v1.1.0 $232001 / 50000$ , Guzhou0806’s R052 $231001 / 50000$ , Kleddamag’s $461300 / 99853$ , Guzhou0806’s earlier R012 result and R067 remain recorded above as historical evidence.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.

bound	evidence	run	code	programs
verified lower	`E-n017-guzhou-r071-source-replay`	replayed here	producer’s code	`V-guzhou-n17-verify-cpp`, `V-kleddamag-n17-verify` (external); `V-audit-guzhou-r071`, `V-replay-guzhou-r071` (first-party, premises)
verified upper	`E-n017-certified-endpoint`	audited here	independent	`V-n17-endpoint-checkers` (first-party); `V-audit-n17-endpoint-receipt` (first-party, premises)