\(N_{\max}(a,b)\) is the maximum number of interior-disjoint unit squares, each in an arbitrary orientation, whose centers lie in the rectangle \([0,a]\times[0,b]\). The squares may protrude from the rectangle; only the centers are constrained; boundary contact between squares is allowed.
Constraining centers rather than whole squares is the right object for impossibility arguments. A computer search proving that \(n\) unit squares do not fit in some region works by splitting the region into cells and asking how many square-centers each cell can host; a bound on \(N_{\max}\) over a cell is exactly the pruning rule such a search needs, and it must hold for squares in every orientation independently, which is where the difficulty lives. The classical quantity \(S_{\max}(a,b)\) (squares contained in the rectangle) transfers in one line: \(S_{\max}(a,b)\le N_{\max}(a-1,b-1)\) and \(N_{\max}(a,b)\le S_{\max}(a+\sqrt2,\,b+\sqrt2)\), since a contained square's center is at distance \(\ge 1/2\) from each side and a center at distance \(\ge 1/\sqrt2\) from each side leaves room for the square in every orientation.
Throughout, \(Q_0=[-\tfrac12,\tfrac12]^2\), \(d=\sqrt{1-w^2}\), \(\tau=(\sqrt2-1)/2\), and \(\xi=(4\sqrt2-2\sqrt3)/5\) (the smaller root of \(\sqrt{4-w^2}+2w=2\sqrt2\), with \(\xi<1/\sqrt2\)).
Fix the rectangle \(R=[0,a]\times[0,b]\). If all squares were axis-parallel, each square \(c_i+Q_0\) would be an area-1 subset of \(R\oplus Q_0\), and area comparison gives \((a+1)(b+1)\) at once. A tilted square centered in \(R\) escapes \(R\oplus Q_0\), so this argument dies under rotation — and no replacement of tilted squares by axis-parallel ones preserves both centers and disjointness. The fix is to stop asking where the square is and start asking what it costs. Charge each unit square \(Q\) the score
\[ \sigma_R(Q) \;=\; \operatorname{area}(Q\cap R)\;+\;\tfrac12\,\operatorname{length}(Q\cap\partial R)\;+\;\tfrac14\,\#\{\text{vertices of }R\text{ in }\operatorname{int}Q\}. \]
Interior area counts in full, boundary trace at weight \(\tfrac12\), covered corners at weight \(\tfrac14\).
One-square lemma: if \(c(Q)\in R\) then \(\sigma_R(Q)\ge1\). The proof runs in four moves. (i) General position. Push each side of \(R\) outward by a generic \(\varepsilon\); the score can only drop in the limit (losses in the limit are boundary or corner terms already present in \(\sigma_R\)), so it suffices to treat configurations where no side line of \(R\) contains a side of \(Q\) and no vertex sits on \(\partial Q\). (ii) Product measure. Translate \(c(Q)\) to the origin and write \(R=[-\alpha,\beta]\times[-\gamma,\delta]\). With \(\mu_{[u,v]}=\lambda_{[u,v]}+\tfrac12\delta_u+\tfrac12\delta_v\) (Lebesgue plus half-atoms at the endpoints), one checks \[ \sigma_R(Q)=\bigl(\mu_{[-\alpha,\beta]}\otimes\mu_{[-\gamma,\delta]}\bigr)(Q): \] \(\lambda\otimes\lambda\) is the area term, atom \(\times\) \(\lambda\) gives half the boundary trace on each side, atom \(\times\) atom gives \(\tfrac14\) at each covered corner. The odd-looking weights \(\tfrac12\) and \(\tfrac14\) are thus not ad hoc: they are what makes the score a product measure. (iii) Quadrant split. The axes carry no atoms (all four side parameters are positive after the perturbation), so the four quadrants at the center contribute additively, and it suffices to show each contributes \(\ge\tfrac14\). (iv) One quadrant. The part of \(Q\) in the closed positive quadrant is a quadrilateral \(OABC\) of area exactly \(\tfrac14\) (shoelace), for every angle \(\theta\in[0,\pi/4]\). If the window corner \((u,v)\) lies in \(P=OABC\), the corner atom alone pays \(\tfrac12\cdot\tfrac12=\tfrac14\). Otherwise the pieces of \(P\) clipped off by the window lines \(x=u\), \(y=v\) are triangles whose base is the clipping slice and whose extent perpendicular to it is at most \(1/(2\cos\theta)\le\sqrt2/2<1\); so each lost triangle has area at most half its base — precisely the \(\tfrac12\)-weighted credit the score grants on that slice. The clipped area is repaid, and the quadrant keeps its \(\tfrac14\).
Summing. For interior-disjoint \(Q_1,\dots,Q_N\) with centers in \(R\): the area terms total at most \(\operatorname{area}(R)=ab\); the boundary traces have disjoint relative interiors (each lies in its own open square), so the edge terms total at most \(\tfrac12\cdot2(a+b)=a+b\); each vertex of \(R\) is interior to at most one square, so corners total at most \(1\). Hence \[ N\;\le\;ab+(a+b)+1\;=\;(a+1)(b+1). \]
Why arbitrary independent rotations survive. The budget \(ab+(a+b)+1\) is a property of \(R\) alone; orientation enters only through the one-square lemma, which is proved for every angle \(\theta\) separately. Nothing couples the orientations of different squares — disjointness is used only to make the three global sums subadditive. The whole difficulty is compressed into the quadrant computation, where the two facts that hold uniformly in \(\theta\) are: the quadrant slice has area exactly \(\tfrac14\), and every clipping direction sees the square with extent \(<1\). For integer \(a,b\) the grid construction meets the bound, so nothing is lost.
To replace the rectangle by an arbitrary compact convex \(K\), replace the score by a payment schedule with three currencies. For a rectifiable curve let \(P_1(\Gamma)=\int_\Gamma(|dx|+|dy|)\) be its \(\ell^1\) length, and for convex \(C\) let \(\kappa_C\) be the exterior-turning measure on \(\partial C\), total mass \(2\pi\) (for a polygon: an atom at each vertex equal to the exterior angle).
Clipping lemma. If \(S\) is a unit square, in any orientation, with center \(o\in C\), then \[ \operatorname{area}(S\setminus C)\;\le\;\tfrac12\,P_1(\partial C\cap\operatorname{int}S)\;+\;\frac{\kappa_C(\operatorname{int}S)}{2\pi}. \] Whatever the region fails to contain of the square, it pays for in anisotropic boundary length and turning inside the square.
How the loss is charged. Work first with a convex polygon \(C\) transverse to \(S\). Each component \(U\) of \(S\setminus C\) has as free boundary one crossing arc \(\Gamma\subset\partial C\) with endpoints \(p,q\in\partial S\). Since \(p,q\in C\), the chord \([p,q]\subset C\) is the full chord of \(S\) on its line, so \(U\) lies strictly on one side of that line, and there are two cases according to where the center sits.
General compact convex \(C\) follows by outer polygonal approximation plus a dilation \(C_\lambda=o+\lambda(C-o)\) centered at \(o\), which confines all limit boundary mass to compact subsets of \(\operatorname{int}S\).
Summing, and why the budget matches term for term. Sum the clipping inequality, in the form \(\operatorname{area}(S_i\cap K)+\tfrac12P_1(\partial K\cap\operatorname{int}S_i)+\kappa_K(\operatorname{int}S_i)/2\pi\ge1\), over the packing. Three measures appear — area on \(K\), \(\ell^1\) length on \(\partial K\), turning on \(\partial K\) — each evaluated on the pairwise-disjoint open squares, so each sum is bounded by its total mass: \[ N\;\le\;\operatorname{area}(K)\;+\;\tfrac12P_1(\partial K)\;+\;1. \] Around a closed convex curve each coordinate rises along one arc between its extremes and falls along the other, so \(P_1(\partial K)=2w_x(K)+2w_y(K)\), giving \(N\le\operatorname{area}(K)+w_x+w_y+1\). And by Cavalieri (sum \(K\) with a horizontal then a vertical unit segment), \(\operatorname{area}(K\oplus Q_0)=\operatorname{area}(K)+w_x+w_y+1\) exactly. The correspondence with the rectangle score is term for term: on an axis-parallel boundary the \(\ell^1\) length is ordinary length, so \(\tfrac12P_1\) is the \(\tfrac12\)-weighted edge term; each rectangle corner carries turning \(\pi/2\), hence normalized mass \(\tfrac14\), the corner weight; and the totals reproduce \(ab+(a+b)+1=(a+1)(b+1)\). The clipping lemma restricted to rectangles is the one-square lemma — the score was the clipping budget all along.
Lower bound, for any \(w,h\): tilt all squares so a side direction points along the rectangle's diagonal and chain them edge to edge — \(\lfloor D\rfloor+1\) centers with \(D=\sqrt{w^2+h^2}\). The content is the matching upper bound for \(w\le\tau=(\sqrt2-1)/2\). Order the centers by height and let \(\ell\) be the line through the lowest and highest, at distance \(c\le D\) apart. Consecutive vertical gaps are \(\ge d\), so every middle center's triangle with the two ends is thin: its distance to \(\ell\) is at most \(w\le\tau\). The short-offset chord lemma says a line at distance \(\le\tau\) from a unit square's center cuts a chord of length \(\ge1\) in it (the corner-cutting case minimizes at \((u-u^2+1)/2\ge\tau\) with \(u=\cos\theta+\sin\theta\)). Since \(\ell\) is closer than \(\tfrac12\) to every center, it contains no side of any square, so the chords' relative interiors lie in disjoint open squares; packing \(n-2\) unit chords between two half-chords of length \(\tfrac12\) along \(\ell\) gives \(c\ge n-1\), hence \(n\le\lfloor D\rfloor+1\).
Beyond \(\tau\), the tool becomes the rounded neighbourhood \(K=Q\oplus D(0,\tfrac12)\) of a square \(Q\): a support-function argument shows no center of a square interior-disjoint from \(Q\) can lie in \(\operatorname{int}K\) (rounded exclusion), and every line at distance \(x\le1/\sqrt2\) from \(c(Q)\) crosses \(K\) in a segment of length \(\ge\nu(x)=\min\{2,\,2\sqrt2-2x\}\) (rounded chord). A third center near two others must therefore straddle a long excluded segment, which yields three positional obstructions (same-side, staircase, opposite-corner) and, by a corner-counting assembly, the extension of the exact law to all \(w\le\xi\) in the regime \(w^2+h^2<4\), plus the first two branches of \(T_3\).
Two interior-disjoint unit squares contained in the quarter plane \([0,\infty)^2\) cannot both have centers in \([0,C]^2\) unless \(C\ge C_*=1+\frac{1}{2\sqrt2}\), and \(C_*\) is attained. Sketch: with \(f(t)=\cos t+\sin t\) and frame deviations \(\alpha_A,\alpha_B\in[0,\pi/4]\), containment forces each center's coordinates to be at least \(f(\alpha_i)/2\), and a separating side normal \(u\) of square \(A\) has \(\|u\|_1=f(\alpha_A)\) while the two supports along \(u\) sum to \((1+f(\delta))/2\) for frame distance \(\delta\). Chaining \( (1+f(\delta))/2 \le \|u\|_1\,\|c_B-c_A\|_\infty \) yields \(C\ge F(\alpha,\beta)=\tfrac{f(\beta)}2+\tfrac{1+f(\alpha-\beta)}{2f(\alpha)}\); \(F\) is concave in \(\beta\) (\(\partial^2(2F)/\partial\beta^2=-f(\beta)-f(\alpha-\beta)/f(\alpha)<0\)), so the minimum is at an endpoint, where \(F(\alpha,0)=1+\frac1{2f(\alpha)}\ge C_*\) and \(F(\alpha,\alpha)\ge\sqrt2\) by AM–GM. Sharpness: the axis-parallel square at \((\tfrac12,\tfrac12)\) and the \(45^\circ\) square at \((C_*,C_*)\) touch along a common supporting line — the diagonal center gap \((C_*-\tfrac12)\sqrt2=(\sqrt2+1)/2\) is exactly the sum of the diagonal supports.
The wide branch \(T_3(w)=1/w\) for \(1/\sqrt2\le w<1\) reduces to the center-area lemma (three interior-disjoint unit squares with non-obtuse center triangle have center-triangle area \(\ge\tfrac12\)): an obtuse center triple in a width-\(w\) strip has vertical span \(\ge1/w\) by an elementary two-page estimate, and an acute one has area \(\ge\tfrac12>wh/2\); conversely, the paper shows that given the narrow branches, the \(1/w\) law is equivalent to the center-area lemma, and the exact band structure \(\tau_{2r+1}=r/w\), \(\tau_{2r+2}=r/w+d\) follows by applying the threshold to consecutive center triples and matching it with two sheared-lattice constructions.
Machine-checked in Lean 4 (Lean v4.29.1 over mathlib, 8,367 build jobs, no sorry, axioms propext, Classical.choice, Quot.sound only; last full rebuild 2026-08-09):
SquareFacts.CenterBound.card_le_of_rotated_unit_square_centers, with the one-square lemma carried out in full as a product-measure statement (RotatedSquare, QuadrantScore, RectangleScore and supporting files, about 4,600 lines) — including every fiddly quadrant case the prose defers.Sharpness), assembled with the bound into the exact value \(N_{\max}(a,b)=(a+1)(b+1)\) for integers as PaperProofs.Nmax.paper_nmax_rectangle_integer; the bound alone is wrapped as paper_rectangle_center_bound.SquareFacts.WideStrip.nmaxValue_very_narrow_strip, wrapped as paper_very_narrow_strip_law.axisAlignedCentralCompactBranch_from_imported (namespace SquareFacts.ElementaryObstructions, file CenterAreaBridge) imports CenterAreaLemma.center_area_lemma and discharges the geometric hypothesis, so these are unconditional in Lean too.Not formalized: the convex Minkowski bound and the cubical clipping lemma behind it, the \(\xi\)-extension of the strip law, the middle branch of \(T_3\), and the entire toolbox. These rest on the prose proofs plus an independent numerical audit: referee.py runs 63 checks over every closed-form constant and inequality in the paper, all passing. Two steps of the rounded-chord lemma remain semi-numerical (a kink inequality verified symbolically only at its endpoint angles, with numerical margin above 0.007 in between, and one coarse-but-rigorous interval bound); interval arithmetic would close both mechanically.
The file papers/nmax/LEAN-CHECK.md in the repository records a statement-by-statement audit of the paper against the Lean sources and the numerical referee, including three drift fixes it made (a misnamed bridge theorem, an overstated line count, an overstated numerical margin). Human review of the paper is incomplete; the bibliography still carries deliberate [CHECK] placeholders where volume and page data were not verified against sources.