T-051: $s (32) = 6$

V3 C3 optimality confirmed

2026-09-26 published · Daniel after Burns, Massaccesi · $n = 32$

$s (32) = 6$ : the lower half by Evan Daniel's weighted closed cover of 26 September 2026, the upper half by the $6 \times 6$ grid.

The cover is 13,085 D4-invariant rational points of [0,6]^2, total weight 3171350535386/10^11 = 31.713505354 < 32, such that every closed unit square in [0,6]^2 captures weight at least one, a boundary point counting. A packing at side below 6 would scale to 32 disjoint closed unit squares capturing at least 32.

The margin is zero at the grid, so the source decides the cover by exhaustive exact pose-space subdivision of its D4 fundamental region (zeromargin.py, 7,200 root boxes), and a Lean theorem derives minSide 32 = 6 from that one checker hypothesis.

The complete zeromargin.py sweep was replayed here on 27 September 2026 with the source's runner, checker and settings: all 7,200 roots certified, 164,130 boxes, every root's census equal to the source's.

The source's third checker, zmx2, was run here on the same cover on 29 September 2026 with --pair-points: all 3,600 roots of the D4 region certified, 1,405,342 boxes, none uncertified. zmx2 is a second implementation of the same subdivision by the same author and agent. Its point test derives from zeromargin.py's, but it closes germs by its own pair lemma and decides by exact integer tests on outward-rounded binary64 enclosures of chord ends. On 2 October 2026 zmx2 was run here again with --sym-atoms, without the D4 fold, over all 28,800 roots of the whole pose space: none uncertified, and every root's census equal to the source's run.

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 first this record holds for s(k^2 - 4) with k >= 4, 0.204 above Nagamochi's closed form. S4 by the anchor "a reusable technique": the zero-margin closed cover decided by exhaustive pose-space subdivision, which the same author carried to $n = 21$ and 45 (T-052, T-053) and wand125 to $n = 45$ (T-054). Not S5: $n = 32$ is not a central open case of this project.
Composition: Compound. The upper half is the $6 \times 6$ grid replayed exactly by the basic-bounds checker (E-basic-grid-upper), a construction its replay establishes, so under epistemics.md's Scope and Composition the equality takes the C of its lower half, which sets the rung.

The lower half rests on complete replays here of the source's zero-margin pose-space subdivision by two checkers whose method values differ: zeromargin.py, exact-algebraic, over the 7,200 roots of the D4 fundamental region (E-n032-evand-closed-cover-source-run), and zmx2, interval-certified, over the 3,600 roots of the D4 region (E-n032-evand-closed-cover-zmx2-replay) and, with --sym-atoms and no fold, over all 28,800 roots of the whole pose space (E-n032-evand-zmx2-full-sym-replay). That is C3, with the two methods shown beside the rung.

The two checkers differ in how germs are closed (zmx2's pair lemma Z and pair dynamic programme over lines one unit apart, against zeromargin.py's monotone chains), in arithmetic and in their parsers. Taken as zeromargin.py's run and zmx2's run without the fold, they no longer share the D4 fold, the region or any symmetry premise: the zmx2 side rests on its own Lemma A (search/ZMX2.md section 4.9, proved, and checked against the code by the 2 October review) where zeromargin.py's rests on the fold, which the source's Lean development kernel-checks, and nothing in zeromargin.py corresponds to Lemma A.

The common mode is what remains shared: the author and AI agent and the statement decided; the point-in-square formulation, G0-G3 with the corner-and-vertex rule, one design in two arithmetics, which for a point cover is the primitive that decides most leaves; the pose parametrisation; and the branch-and-bound architecture. The source's Lean development kernel-checks the formulation on zeromargin.py's side, which bounds the common mode and does not remove it. The two checkers are separately written, not independent.

The point test is shared by derivation: on 1 October 2026 the source stated that zmx2 was written to be independent of zm_mixed.py only and that its author was permitted to read zeromargin.py, so Lemma P derives from zeromargin.py's G0-G3 (jlevy/squares#238, retained as packing/resources/web/evand-square-packing-2026-10-01/issue-238-author-2026-10-01.json). The brief that governed that reading was not public when this entry was reviewed. The source published it on 3 October, and the 4 October evand packet retains it (s12/tasks/s21-finish/xcheck.md, think-83zc): it forbids zm_mixed.py and its write-up and permits zeromargin.py, zmcheck and their write-ups, as the source said.
Next rung: V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained; whether a mapped same-project review of another author's result counts toward them is the owner's decision. V5 needs the source's hypothesis-free Lean theorem s32_eq_6 built, which decides a generated box tree in the kernel with zeromargin.py only as the tree generator's untrusted oracle, and a human expert's review of the formalization. Mathlib's build cache became reachable on 2026-09-30, and the conditional s32_eq_six_of_checker and s13_eq_4 were built here (the 2026-09-28 packet's receipts/lean/). The cost that remains is compute: a probe puts s32_eq_6 at 14 to 28 CPU-hours emitted in about 320 parts of about 4 GB each, with 8 to 10 GB for the generator (think-angg).

Beside the rung, the source's zmx2 --full --pair-points --sym-atoms run was replayed here on 2 October (think-48e1, E-n032-evand-zmx2-full-sym-replay), which took the D4 fold out of what the two checkers share. It changes neither rung: it is evidence of the kind already held, a machine replay of the source's own checker with a mapped review, as section 8 of the 2 October review says, and what it changes is the composition that rung 4's reviewers and oversight record will read.
Novelty: previously-published Present in an identified source

The case

Case record

567

5.6576.657

\sqrt{n}

\sqrt{n} + 1

Proven

$s (32) =$ $6$

optimal
exact

Citation record n-032

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

The case record

LowerUpper

Verified66

Reported66

Gap0 solved: the verified bounds meet

Results on the case

8 results in the register on $n = 32$ , 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-051
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-26 published T-051 this result
$s (32) = 6$
V3 C3 optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · review 3 · register
2026-09-27 published T-045
Rectangle-density lower bounds replayed at 15 counts in $n = 18 \dots 78$
V3 C3 lower bound confirmed superseded by T-051
wand125 after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · 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-051
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 = 32$ · Frontier row, $n = 32$ · T-051 in the results table

On GitHub, at main

Register: T-051 in results.yaml, line 4417
Evidence: E-n032-evand-closed-cover-report · E-n032-evand-closed-cover-source-run · E-n032-evand-closed-cover-zmx2-replay · E-n032-evand-zmx2-full-sym-report · E-n032-evand-zmx2-full-sym-replay · E-basic-grid-upper
Proofs and certificates: certificate s32_closed_cover_6.txt.gz · proof README.md · audit review-2026-09-27-evand-s32-s12.md · audit review-2026-09-28-wand125-point-only-s21-s45.md · proof README.md · audit review-2026-10-02-evand-s32-no-fold-run.md
Sources: evand square-packing 2026 (its own site, retained copy) · evand square-packing 2026-10-01
Source packet: resources/web/evand-square-packing-2026-09-26/README.md · resources/web/evand-square-packing-2026-09-28/README.md · resources/web/evand-square-packing-2026-10-01/README.md · resources/web/evand-zmx2-sym-atoms-2026-09-30/README.md
Artifacts: 22 artifacts and controls in 11 directories. Complete artifact list in the result entry. docs/project/reviews packing/devtools packing/resources/web/evand-square-packing-2026-09-26 packing/resources/web/evand-square-packing-2026-09-26/receipts packing/resources/web/evand-square-packing-2026-09-26/square-packing/s12/certificates/s32 packing/resources/web/evand-square-packing-2026-09-28 packing/resources/web/evand-square-packing-2026-09-28/receipts packing/resources/web/evand-square-packing-2026-10-01 packing/resources/web/evand-zmx2-sym-atoms-2026-09-30 packing/resources/web/evand-zmx2-sym-atoms-2026-09-30/receipts packing/tests
Case file: frontier/n-032.md (verified lower, verified upper, reported lower, reported upper)

T-051: s(32)=6s(32)=6

The case

Results on the case

Links

T-051: $s (32) = 6$