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

S3 V3 C3 optimality confirmed

2026-09-04 published · chelokot · 16 cases, $n=7$$n=7$ to 322

s(k^2 - 2) = k for every integer k >= 2: chelokot's Lean theorem Records.NearSquare.squareMinusTwo_isMinimumSide, kernel-checked here. The lower half compensates each square of score at most one under Nagamochi's measure from other squares of the packing, so it does not use Nagamochi's Lemma 1, which is false (T-085); the upper half is the k x k grid with two squares removed.

This entry's scope is the cases this record holds, k = 3 to 18: $s(7)=3$$s(7)=3$, $s(14)=4$$s(14)=4$, $s(23)=5$$s(23)=5$, $s(34)=6$$s(34)=6$, $s(47)=7$$s(47)=7$, $s(62)=8$$s(62)=8$, $s(79)=9$$s(79)=9$, $s(98)=10$$s(98)=10$, $s(119)=11$$s(119)=11$, $s(142)=12$$s(142)=12$, $s(167)=13$$s(167)=13$, $s(194)=14$$s(194)=14$, $s(223)=15$$s(223)=15$, $s(254)=16$$s(254)=16$, $s(287)=17$$s(287)=17$ and $s(322)=18$$s(322)=18$. Nagamochi 2005 stated the family first (T-007).

The development was built here with its pinned toolchain and Mathlib's cache, and its axioms are exactly propext, Classical.choice and Quot.sound. chelokot, square-packing-archive, September 2026.