T-053: $s (45) = 7$ , by a mixed cover of points and grid-line segments

V3 C3 Optimality confirmed

2026-09-27 published · Daniel after Burns, Massaccesi · $n = 45$

$s (45) = 7$ : the lower half by Daniel's mixed cover of 27 September 2026, the upper half by the $7 \times 7$ grid.

The cover is 19,989 weighted points of [0,7]^2 plus mass spread uniformly along 3,912 segments of length 1/50 on the interior grid lines, total 2238676387/(5*10^7) = 44.77352774 < 45, exactly D4-invariant. Every closed unit square in [0,7]^2 captures mass at least one, with boundary points and edge segments counting in full.

The source certifies it at margin zero with the same two checkers as T-052, zm_mixed.py over 78,400 roots of the D4 region and zmx2 over 4,900 D4 roots and 39,200 unreduced roots. Nothing about this cover is in Lean beyond lemmas proved for every side.

zmx2 was replayed here in full on 28 and 29 September 2026, over all 4,900 D4 roots and all 39,200 unreduced roots, every root's census equal to the source's; zm_mixed.py was only sampled.

Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.

Significance, composition and next rung

Significance: An exact value for a case that was open, 0.169 above Nagamochi's closed form, by the technique of T-052 at a third count. S3 by the anchor 'a substantive case result', as T-062 ( $s (60) = 8$ ), T-066 ( $s (59) = 8$ ) and T-067 ( $s (77) = 9$ ) are: the recipe's first instances, T-051 and T-052, hold the S4 for the technique, and the family s(k^2 - 4) = k is T-081's claim and carries its S4 there. The draft's S4 rested on this count going from open to solved and on three siblings making a bound family; every exact value closes a case, and a family in the S4 sense is one argument at every k, not three certificates. Changed from S4 on 11 October, as the 2 October review of T-062 asked, so that the two carry one score.
Composition: Compound: the lower half is E-n045-evand-mixed-cover-zmx2-replay (interval-certified), the upper half the grid (E-basic-grid-upper, exact-algebraic). As for T-052, the two machine methods certify different halves; the lower half stands on one replayed method and sets the minimum, and the equality is C3. Hosono's point-only lower half (T-054) is a second certificate under the same checker and is registered separately.
Next rung: V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A complete zm_mixed.py re-sweep, about 16.5 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method; the source's own zm_mixed.py record was imported from a working-name run (review finding F1), so a fresh complete run also retires that finding. V5 would need a top theorem and the checker programs formalised, and a human expert's review of the formalization.
Novelty: previously-published Present in an identified source

The case

Case record

678

6.7087.708

\sqrt{n}

\sqrt{n} + 1

Proven

$s (45) =$ $7$

optimal
exact

Citation record n-045

lowerDaniel after Burns, Massaccesi 2026, GitHub (confirmed T-053)

The case record

LowerUpper

Verified77

Reported77

Gap0 solved: the verified bounds meet

Results on the case

8 results in the register on $n = 45$ , 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-053
Nagamochi · Nagamochi 2005 · source · 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ş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-27 published T-053 this result
$s (45) = 7$ , by a mixed cover of points and grid-line segments
V3 C3 Optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-09-28 · packet · source · review · register
2026-09-28 published T-054
$s (45) = 7$ by a second, point-only route
V3 C3 Simplification confirmed
Hosono after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point and mixed bounds 2026-09-28 · 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
Hosono 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-053
Karakuş · Karakuş 2026 · source · register
2026-10-03 published T-081
$s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here
V0 C1 Optimality reviewed on this case, second certificate, reported
Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register
2026-10-07 published T-124
Reported non-strict local minima for 178 source configurations
V0 C0 Restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register

Links

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

On GitHub, at main

Register: T-053 in results.yaml, line 4784
Evidence: E-n045-evand-mixed-cover-report · E-n045-evand-mixed-cover-zmx2-replay · E-basic-grid-upper
Proofs and certificates: certificate s45_mixed_cover_7.txt.gz · proof README.md · audit review-2026-09-28-evand-s21-s45-mixed-covers.md
Sources: evand square-packing 2026-09-28 (its own site, retained copy)
Source packet: resources/web/evand-square-packing-2026-09-28/README.md
Artifacts: 7 artifacts and controls
resources/web/evand-square-packing-2026-09-28/README.md resources/web/evand-square-packing-2026-09-28/square-packing/s12/certificates/s45/README.md resources/web/evand-square-packing-2026-09-28/receipts/audit.json devtools/audit_evand_mixed_covers.py devtools/check_basic_bounds.py docs/project/reviews/review-2026-09-28-evand-s21-s45-mixed-covers.md tests/test_evand_mixed_covers.py
Case file: frontier/n-045.md (verified lower, verified upper, reported lower, reported upper)

T-053: s(45)=7s(45)=7, by a mixed cover of points and grid-line segments

The case

Results on the case

Links

T-053: $s (45) = 7$ , by a mixed cover of points and grid-line segments