Improve or prove optimal the packing of 17 unit squares into a smallest square

Let $s(N)$ be the side length of the smallest axis-parallel square into which $N$ unit squares can be packed without overlap; the unit squares may be translated AND rotated arbitrarily. For $N=17$ (not a perfect square) the exact value $s(17)$ is unknown -- only a best-known packing (often using tilted squares) is recorded. Exhibit a packing of 17 unit squares into a square of side strictly less than the current best-known $s(17)$, or prove that the best-known packing is optimal. Tilted (rotated) unit squares frequently beat the naive axis-aligned arrangement, which is what makes these values hard.

Acceptance. FULLY RESOLVES: a rigorous proof determining $s(17)$. PARTIAL (improve record): for each of the 17 unit squares a center $(x_i,y_i)$ and rotation angle $\theta_i$, plus a container side $s < s(17)^{best}$, such that (i) every rotated unit square lies inside the $s\times s$ container and (ii) no two overlap; verifier -- separating-axis test (SAT) for each pair of rotated squares and each square-vs-container check, all exact from the given coordinates. PARTIAL: a certified lower bound on $s(17)$ narrowing the gap.