Packing k² − ⌈√(32k)⌉ − 1 unit squares in a square of side less than k

Let s(N) be the side of the smallest square containing N unit squares with disjoint interiors, and let c*(k) be the largest c with s(k² − c) = k. We prove c*(k) < 4√(2k) + 1 for every integer k ≥ 6, that is, s(k² − ⌈√(32k)⌉ − 1) < k. The construction is Ryu's L-shaped packing: an aligned grid and two bands of b tilted rows. Both ends of each band are filled with axis-parallel rows, and b is the odd integer nearest √(2k). The odd width keeps the rounding loss of each filled end below 3/2. This lowers the constant of the O(√k) bound valid for every k ≥ 6 from 8 (Ryu) to 4√2. The bound is the smallest explicit one we know of for 42 ≤ k < 1.6·10⁷, except at five values of k where Ryu has computer-assisted bounds. Exact rational certificates for k ≤ 600 are checked by two independently written programs. Files: the note as PDF (draft v0.1, 5 pages) and its LaTeX source. Code, exact certificates and checkers: squarepack-certs, folder theorem-a/, commit b1b3f6bda13739c9eeecc1ceaefec9178294e0ca.