T-064: s(k2−3)=k$s(k^2-3)=k$ for every integer $k$$k$ from 6 up; $k=6\dots 18$$k=6\dots 18$ are the cases held here

S4 V3 C3 optimality confirmed

2026-09-30 published · Daniel after Burns, Massaccesi · 13 cases, $n=33$$n=33$ to 321

Evan Daniel's theorem s(k^2 - 3) = k for every integer k >= 6, dated 29 September 2026 by the source and public in its repository on 30 September: the lower half by one family of periodic measures, the upper half by the k x k grid.

This entry's scope is the projection of that theorem onto the cases this record holds, n <= 324, which is k = 6 to 18: $s(33)=6$$s(33)=6$, $s(46)=7$$s(46)=7$, $s(61)=8$$s(61)=8$, $s(78)=9$$s(78)=9$, $s(97)=10$$s(97)=10$, $s(118)=11$$s(118)=11$, $s(141)=12$$s(141)=12$, $s(166)=13$$s(166)=13$, $s(193)=14$$s(193)=14$, $s(222)=15$$s(222)=15$, $s(253)=16$$s(253)=16$, $s(286)=17$$s(286)=17$ and $s(321)=18$$s(321)=18$. The reported theorem does not end at k = 18.

For each k the measure on [0,k]^2 is a corner module in each corner, a profile of period one along each wall and Lebesgue measure on the middle square, of total mass k^2 - 4D with D = 423621306389/500000000000, so that 4D exceeds 3. The source states that every closed unit square in [0,k]^2 has mass at least one, and reduces that, for every k >= 6, to one finite statement it calls Valid7: every closed unit square in [0,7]^2 has mass at least one under the k = 7 measure.

The source's Lean development takes Valid7 as a hypothesis and, the source reports, kernel-checks that it implies the theorem for every k >= 6; it does not prove Valid7. Valid7 is the claim of the source's exact-rational Python checker, qx2_zm.py, which the source reports accepting all 9,800 root boxes in 32,079 leaves, with the axis-parallel poses decided by a separate exact enumeration; it reports six adversarial reviews of the certificate by AI agents and none by outside mathematicians.

On 2 October 2026 wand125 published a second, separately written exact-rational checker of Valid7 on the same cover, which reports all 156,800 root boxes of the unreduced pose space certified in 9,640,060 leaves, about 626 core-hours, and says Daniel's checker and lemma write-ups were not read. The two share the statement, the cover and its format.

Here both parts of the lower half were rebuilt. Daniel's checker was replayed in full on the retained cover on 2 and 3 October 2026, in two shards: all 9,800 root boxes and 32,079 leaves, none uncertified, each root's leaves equal to the published run's, which discharges Valid7 for this cover. The Lean reduction was built from retained bytes with the pinned toolchain, and bentz_of_valid7 depends only on the standard axioms. Together they prove the theorem here, for every k >= 6.

wand125's second checker was reviewed on 2 October and found sound but for one defect in its exact positivity test (D-1), which cannot make a true Valid7 fail. It was replayed here in full on 2 and 3 October with that test's accepting case made a refusal, in fourteen shards: all 156,800 root boxes certified in 9,808,968 leaves, none uncertified, and each root the source ran under its published code with the published leaves. So Valid7 is decided here by two separately written exact checkers, Daniel's reproduced with the producer's code and wand125's independently re-implemented.

So $s(97)=10$$s(97)=10$, $s(118)=11$$s(118)=11$, $s(141)=12$$s(141)=12$, $s(166)=13$$s(166)=13$, $s(193)=14$$s(193)=14$, $s(222)=15$$s(222)=15$, $s(253)=16$$s(253)=16$, $s(286)=17$$s(286)=17$ and $s(321)=18$$s(321)=18$ are proved here, nine cases closed. $s(33)=6$$s(33)=6$ and $s(46)=7$$s(46)=7$ were proved already on Bentz's proofs, $s(61)=8$$s(61)=8$ on Daniel's $s(60)$$s(60)$ cover (T-063), and $s(78)=9$$s(78)=9$ on wand125's $s(77)$$s(77)$ cover (T-067); this family proves each again by another route.

Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method. The source's CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.