T-052: , by a mixed cover of points and grid-line segments
V3 C3 optimality confirmed
: the lower half by Evan Daniel's mixed cover of 27 September 2026, the upper half by the grid.
The cover is 7,536 weighted points of [0,5]^2 plus mass spread uniformly along 1,872 segments of length 1/50 on the interior grid lines, total 522368729933/(25*10^9) = 20.894749197 < 21, exactly D4-invariant. Every closed unit square in [0,5]^2 captures mass at least one, a boundary point and a segment along an edge counting in full.
The source certifies that at margin zero with two separately written checkers, zm_mixed.py in exact rational arithmetic and the Rust zmx2 with outward-widened binary64 enclosures, and Lean proves minSide 21 = 5 from the one checker statement.
zmx2 was replayed here in full on 28 and 29 September 2026, D4-reduced over 2,500 roots and unreduced over 20,000, 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, the second of the s(k^2 - 4) family after T-051, and the release that introduced line mass on the grid lines, which is what makes a zero-margin cover below the count possible at an integer side. S4 by the anchor "a reusable technique"; T-053 reuses it at .
- Composition
- Compound: the lower half is E-n021-evand-mixed-cover-zmx2-replay (interval-certified, zmx2 replayed here), the upper half the grid (E-basic-grid-upper, exact-algebraic). The two machine entries differ in method, but they certify different halves; the lower half, which sets the minimum, stands on one replayed method, and the equality is C3, as T-008 reads its own halves.
- 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 12.9 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method; the shared pose-space architecture stays the residual common-mode risk. V5 would need the checker statement S21CheckerCover proved in Lean and a human expert's review of the formalization; the reduction s21_eq_five_of_checker, from that statement to , was kernel-checked here on 2026-09-30 with the standard axioms only (the 2026-09-28 packet's receipts/lean/).
- Novelty
- previously-published Present in an identified source
The case
Results on the case
12 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007
for
V0 C1 lower bound incomplete on this case, superseded by T-052
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 established T-020
for
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-05 established T-021
for
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 established T-034
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 published T-050
V3 C3 lower bound confirmed superseded by T-052
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · source · review · register
2026-09-27 published T-052 this result
, 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-055
by a 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 ..100;B·UB(n)on 64 grid rowsV3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
for every nonsquare
V3 C3 lower bound confirmed on this case, superseded by T-052
Karakuş · Karakuş 2026 · source · register
2026-10-03 published T-081
for every integer from 5 up; 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, · Frontier row, · T-052 in the results table
On GitHub, at main
- Register
- T-052 in
results.yaml, line 4579 - Evidence
E-n021-evand-mixed-cover-report·E-n021-evand-mixed-cover-zmx2-replay·E-basic-grid-upper- Proofs and certificates
- certificate
s21_mixed_cover_5.txt.gz· proofREADME.md· auditreview-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
8 artifacts and controls
resources/web/evand-square-packing-2026-09-28/README.mdresources/web/evand-square-packing-2026-09-28/square-packing/s12/certificates/s21/README.mdresources/web/evand-square-packing-2026-09-28/square-packing/s12/lean/Sqpack/S21.leanresources/web/evand-square-packing-2026-09-28/receipts/audit.jsondevtools/audit_evand_mixed_covers.pydevtools/check_basic_bounds.pydocs/project/reviews/review-2026-09-28-evand-s21-s45-mixed-covers.mdtests/test_evand_mixed_covers.py- Case file
frontier/n-021.md(verified lower, verified upper, reported lower, reported upper)