$n=45$$n=45$

$s(45)$$s(45)$ — solved

$s(45)=7$$s(45)=7$. Established by a mixed cover with two exhaustive checks of its covering condition, Daniel (2026), building on Burns’s and Massaccesi’s weighted exact-rational covering method. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction. With $s(21)=5$$s(21)=5$, registered with it, and $s(32)=6$$s(32)=6$, it is the third exact value this record holds for a case of the form k2−4$k^2-4$ with $k\ge 4$$k\ge 4$, as the source says.

The packing

The upper bound is trivial: the $7\times 7$$7\times 7$ grid holds 49 unit squares, so it holds 45 with four cells empty, and $s(45)\le 7$$s(45)\le 7$. The record catalogue does not picture $n=45$$n=45$, and no arrangement below side 7 has ever been found. What is new is that none exists.

The lower bound

The certificate is a mixed cover in the format of $s(21)$$s(21)$’s: 19,989 rationally weighted points of [0,7]2$[0,7{]}^2$ plus mass spread uniformly along 3,912 segments of length $1/50$$1/50$ on the interior grid lines $x,y\in \{1,\dots ,6\}$$x,y\in \{1,\dots ,6\}$, total 2238676387/(5⋅107)=44.77352774<45$2238676387/(5·{10}^7)=44.77352774<45$, exactly invariant under the square’s eight symmetries, such that every closed unit square inside [0,7]2$[0,7{]}^2$, at every centre and every angle, captures mass at least $1$$1$, a point on its boundary counting and a segment along one of its edges counting in full. If 45 unit squares fit in a side $s<7$$s<7$, scaling by $7/s$$7/s$ gives 45 pairwise disjoint closed unit squares in [0,7]2$[0,7{]}^2$, which would capture at least 45 from a total of $44.77$$44.77$. As for $s(21)$$s(21)$, the margin is exactly zero at the grid, and the line mass, $32.8$$32.8$ of the total, is what makes that possible.

The source certifies it with the same two checkers, byte for byte. zm_mixed.py, in exact rational arithmetic, certifies all 78,400 root boxes of the cover’s D4 fundamental region (437,510 boxes, 16.5 CPU-hours) with no uncertified leaf; that record was produced under the cover’s working file name and imported into the bundle with only its input path changed, which the source discloses. The Rust zmx2, with its binary64 enclosures widened outward, certifies all 4,900 roots of the same region and, assuming no symmetry, all 39,200 roots of the whole pose space. Nothing about this cover is in Lean: the reduction is the $m=7$$m=7$ case of lemmas the source proves in Lean for every side, but there is no data file and no top theorem, and the cover was not separately audited at the source.

The verified field rests on a complete replay here of zmx2 (E-n045-evand-mixed-cover-zmx2-replay, V3/C3). Built from the retained source with rustc 1.94.1, it certified all 4,900 D4 roots (2,071,984 boxes) and all 39,200 unreduced roots (16,648,752 boxes) on 28 and 29 September with no uncertified box, every root carrying the census of the source’s record of the same root, and the bundle’s own fast tier passed too; the receipts are in the packet. That replay is interval-certified, so it assumes correctly rounded binary64 arithmetic on the host. The exact checker was sampled here, 32 roots matching the source’s records box for box, and its complete re-sweep runs separately; recorded as a second, exact-algebraic replay, it would give this value a second machine method beside its C3. The review of 28 September found the value sound as stated, with one fewer kernel-checked link than $s(21)$$s(21)$: the cover’s total and invariance rest on three independent parsers, not on Lean.

Hosono published a second, point-only route to the same value on 28 September: 12,645 D4-invariant weighted points, total 12666371418707823/248=44.99999100001…$12666371418707823/2^{48}=44.99999100001\dots$, whose capture condition is decided by Daniel’s unmodified zmx2 with its --pair-points option. It claims no priority. Its source check was replayed here in full (E-n045-wand125-point-cover-source-replay): all 4,900 D4 roots certified with the source’s reference census, 1,295,460 boxes to depth 38, and the point-only review found it sound. It is the same checker as the replay above, so it adds a second certificate for the value, not a second method. Hosono’s README says parts of the work were produced with AI assistance under human direction.

Earlier lower bounds

Hosono’s rectangle-density certificate in Tokoharu’s format, retained, reported $1391/200=6.955$$1391/200=6.955$ on 2026-09-27, with total mass $4499/100=44.99<45$$4499/100=44.99<45$; it was the case’s reported bound until this registration and stays as evidence. Its complete coverage replay never ran here. The source gives Hosono’s earlier $1389/200$$1389/200$ as the previous bound. Corrected 2 October 2026: Nagamochi’s Lemma 1 is false (Karakuş 2026), so his closed form below is now a reported bound whose published proof is incomplete (review). This register had recorded that proof as verified, its own error, logged as defect D-516. Before 2026 it was Nagamochi’s general closed form, which applies to every $N\ge 4$$N\ge 4$ and gives 1+34​≈6.830952$1+\sqrt{34}\approx 6.830952$ here:

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.