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

Evan 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, and the third of the family s(k^2 - 4) = k for k = 5, 6, 7 with T-051 and T-052. The technique is T-052's, which alone would argue for S3 by the calibration T-020 wrote, but that calibration exempts a case that changes character, and this one goes from open to solved; with its two siblings it is a bound family, so S4.
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. wand125'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ş; chelokot · 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
wand125 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
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-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 4659
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