T-251: Hosono reports a Lean kernel proof of Daniel's ValidTilt9, so s(k2−4)=k$s(k^2-4)=k$ for every $k\ge 8$$k\ge 8$

2005 published T-007 · 11 of these cases

s(n)≥min(⌈n​⌉,n−2⌊n​⌋+1​+1)$s(n)\ge min(\lceil \sqrt{n}\rceil ,\sqrt{n-2\lfloor \sqrt{n}\rfloor +1}+1)$ for $4\le n\le 324$$4\le n\le 324$

Lower bound incomplete on these cases, superseded by T-062, T-067, T-081 (reported), T-083 and T-191

Nagamochi · Nagamochi 2005 · source · register

2026-09-04 published T-085 · 11 of these cases

Nagamochi 2005, Lemma 1 is false for every container with $a>3$$a>3$ and $b>2$$b>2$

Correction confirmed

Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

2026-09-27 published T-045 · case 77

Rectangle-density lower bounds replayed at 15 counts in $n=18\dots 78$$n=18\dots 78$

Lower bound confirmed superseded by T-067

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register

2026-09-27 published T-046 · cases 60, 77

Rectangle-density lower bounds verified at 48 counts in $n=18\dots 95$$n=18\dots 95$

Lower bound confirmed superseded by T-062 and T-067

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register

2026-09-28 published T-062 · case 60

$s(60)=8$$s(60)=8$, by a mixed cover of points and grid-line segments

Optimality confirmed

Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · source · review · register

2026-09-28 published T-070 · case 60

Rectangle-density lower bounds replayed at 25 counts in $n=29\dots 95$$n=29\dots 95$

Lower bound confirmed superseded by T-062

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register

2026-09-29 published T-058 · cases 60, 77, 96

Rectangle-certificate ceiling α·UB(n) proved for $n=1$$n=1$..100; B·UB(n) on 64 grid rows

Method limit confirmed

Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register

2026-09-29 published T-083 · 11 of these cases

s(n)≥1/2+n−⌊n​⌋+1/4​$s(n)\ge 1/2+\sqrt{n-\lfloor \sqrt{n}\rfloor +1/4}$ for every nonsquare $8\le n\le 324$$8\le n\le 324$

Lower bound confirmed

Karakuş · Karakuş 2026 · source · register

2026-10-01 published T-067 · case 77

$s(77)=9$$s(77)=9$, by a mixed cover extended from Daniel's $s(60)$$s(60)$ cover

Optimality confirmed

Hosono after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register

2026-10-02 published T-075 · case 96

Mixed rectangle-measure lower bounds replayed at nine counts in $n=83\dots 96$$n=83\dots 96$

Lower bound confirmed on these cases, superseded by T-081 (reported) and T-191

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds afternoon 2026-10-02 · packet · source 1 · source 2 · review · register

2026-10-03 published T-081 · 11 of these cases

s(k2−4)=k$s(k^2-4)=k$ for every integer $k$$k$ from 5 up; $k=5\dots 18$$k=5\dots 18$ are the cases held here

Optimality reviewed

Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register

2026-10-03 published T-082 · case 96

Mixed rectangle-measure lower bounds verified at 22 counts in $n=51\dots 96$$n=51\dots 96$

Lower bound confirmed on these cases, superseded by T-081 (reported) and T-191

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-03 · packet · packet · source · review · register

2026-10-04 published T-090 · case 96

Mixed rectangle-measure lower bounds verified at 17 counts in $n=42\dots 96$$n=42\dots 96$

Lower bound confirmed on these cases, superseded by T-081 (reported) and T-191

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 mixed bounds 2026-10-04 · packet · source · review · register

2026-10-07 published T-124 · 11 of these cases

Reported non-strict local minima for 178 source configurations

Restricted optimality recorded

Daniel after Couzo · Daniel exact and local reports 2026 · packet · register

2026-10-12 published T-261 · 11 of these cases

Reported grade-C local minima for 233 source configurations of field degree at most 4

Restricted optimality incomplete

Daniel after Schadt, Ellsworth, Levy · Daniel exact and local reports 2026-10-12 · packet · packet · register

2026-10-13 published T-180 · 11 of these cases

Closed-form lower bound $s(N)\ge a(N)$$s(N)\ge a(N)$ for every non-square $N\ge 49$$N\ge 49$, reported

Lower bound reviewed on these cases, superseded by T-062, T-067, T-081 (reported), T-083 and T-191

Hosono · wand125 closed form 2026-10-14 · packet · packet · register

2026-10-15 published T-191 · case 96

$s(95)=10$$s(95)=10$, by a mixed cover of points and grid-line segments

Optimality confirmed

Greff after Daniel, Hosono · bengreff s95 certificate 2026-10-15 · packet · source · review · register

2026-10-16 published T-251 this result · 11 of these cases

Hosono reports a Lean kernel proof of Daniel's ValidTilt9, so s(k2−4)=k$s(k^2-4)=k$ for every $k\ge 8$$k\ge 8$

Formalization recorded

Hosono after Daniel, Levy, Burns, Massaccesi · wand125 ValidTilt9 Lean 2026-10-16 · packet · source · register