Axis-parallel square packing with an exact formula for optimal packing of seven squares

How large a square is needed to hold axis-parallel squares of prescribed side lengths? We give exact formulas for the optimal side through seven squares, with explicit constructions and geometric lower-bound proofs. For every n ≥ 6, the optimum for n squares is a sum of at most $n-3$ of the prescribed side lengths. This bound is sharp on an open set of side lengths and yields the optimal Euclidean Lipschitz constant √n-3 of the optimum as a function of the n side lengths.