Packing n² − n + 1 unit squares in a square of side less than n, for every n ≥ 15

Let s(N) be the smallest side of a square containing N unit squares with disjoint interiors, rotations allowed. We prove s(n² − n + 1) < n for every integer n ≥ 15. More generally, n² − n + 1 + p + 2q unit squares fit below side n whenever p, q ≥ 0 are integers and 16p + 21q ≤ n − 15. The proof iterates the four-piece construction of Arslanov, Mustafin and Shangitbayev, using known and new base packings and exact rational packings of 257 squares in 17 × 16 and 443 squares in 22 × 21. Independently written exact programs check the finite inputs, and we supply generated certificates for 15 ≤ n ≤ 64. Lean 4 formalises the first theorem and the two unmixed bounds, including kernel checks of all 18 input pieces. The contribution is an explicit threshold and construction, rather than a new asymptotic waste bound. Files: the note as PDF (draft v0.9, 7 pages) and its LaTeX source. Exact certificates and checkers: squarepack-certs, commit 078789a4cfd36f915f1bfbe76d742413d79b2965. Lean 4 formalisation: squarepack-lean, commit 947bdae.