Three papers on packing unit squares into larger regions, centred on the classical question: what is the side \(s(n)\) of the smallest square that contains \(n\) interior-disjoint unit squares, rotations allowed? Each paper has an overview and tutorial page, a PDF, and a machine-verification audit in the repository.
Proves \(s(17) > \tfrac{40\sqrt2+19}{17} + \tfrac{1}{200} \approx 4.4502\), improving a bound of Trevor Green that had stood since 2000, with the same bound for \(s(18)\) as a corollary. The proof deforms Green's 16-point scaffold along its unit-circle constraint and charges an exact defect identity against a finite ledger: fourteen hash-pinned exact certificates plus a 634,562-row exact enumeration, with the algebraic spine formalized in Lean 4.
Three unit squares with pairwise disjoint interiors, rotated arbitrarily and independently, whose centers form a non-obtuse triangle, span a center triangle of area at least \(\tfrac12\) — and this is sharp. The proof reads first-order optimality conditions as a reciprocal force diagram. Fully machine-checked in Lean 4, with a second, independent machine-checked proof by a different route.
Studies \(N_{\max}(a,b)\), the maximum number of interior-disjoint unit squares whose centers lie in an \(a\times b\) rectangle. Proves \(N \le \operatorname{area}(K \oplus Q)\) for centers in any compact convex \(K\) (so \(N_{\max}(a,b)\le(a+1)(b+1)\), sharp at integers, machine-checked), an exact narrow-strip law, the exact three-center threshold, and a toolbox of sharp local bounds.
A 195-page textbook companion to the centre-area lemma paper, starting from first-year-undergraduate mathematics and building everything the proof needs: convex sets and support functions, separating branches, configuration-space calculus, compactness and first-order optimality, the Farkas lemma, and the reciprocal force diagram, ending with a full proof of the lemma. Each chapter has worked examples and exercises.