The Center-Area Lemma

AI-generated research. This paper and page were produced with a mix of ChatGPT and Claude Fable and have not yet been adequately human reviewed. The headline theorem is machine-checked in Lean 4; treat everything else with appropriate skepticism.

← All papers · PDF · Repository

At a glance

Take three unit squares in the plane, each rotated however you like, with pairwise disjoint interiors. If the triangle formed by their centers has no obtuse angle, then that triangle has area at least \(1/2\). The bound is sharp — three axis-parallel squares centered at three corners of a unit square attain it — and the angle hypothesis is essential: obtuse center triangles can have arbitrarily small area. The difficulty is the independent rotations: the disjointness constraint between two tilted squares is nonconvex and depends on both orientations, so the problem is a minimization over a five-parameter family (two free centers, three angles) with no symmetry to exploit.

The result

Theorem. Let \(S_1,S_2,S_3\) be closed unit squares in the plane, rotated arbitrarily and independently, with pairwise disjoint interiors, and let \(P_1,P_2,P_3\) be their centers. If the triangle \(P_1P_2P_3\) is non-obtuse (every angle at most \(\pi/2\)), then \[ \operatorname{area}(P_1P_2P_3)\;\ge\;\tfrac12 . \]

Non-obtuseness is used in the squared-side-length form: for each vertex, the square of the opposite side is at most the sum of the squares of the adjacent sides. Without any angle hypothesis one still has \(\operatorname{area}(P_1P_2P_3)\ge\tfrac12\sin\theta\) for every angle \(\theta\) of the center triangle, an immediate consequence of the fact that two disjoint unit squares have centers at distance at least \(1\).

Why it matters

Lower bounds for square-packing problems — how small a square can contain \(n\) unit squares with disjoint interiors — are counting arguments over the centers of the packed squares, and their basic pairwise input is one-dimensional: two centers are at distance at least \(1\). The first genuinely two-dimensional constraint concerns triples of centers, and its natural quantitative form is a lower bound on the area of the center triangle; this paper proves the sharp such bound. The theorem is also exactly the hard part of a natural three-center threshold governing when three centers of disjoint unit squares fit in a \(w\times h\) rectangle: the wide branch of that threshold is equivalent to the lemma, so no first-principles proof of the threshold bypasses it.

How the proof works

The proof is by contradiction. Assume an admissible configuration whose non-obtuse center triangle has doubled area \(D_0 = 2\operatorname{area} < 1\). The strategy: replace the nonconvex disjointness constraints by three frozen linear inequalities, minimize area subject to those, and read off first-order optimality at the minimum as a mechanical equilibrium — three contact forces pressing the triangle inward, in balance. The equilibrium conditions are restrictive enough that a short case analysis forces \(D\ge1\), a contradiction.

1. Separating branches and the threshold \(H(t)\)

Two disjoint convex bodies admit a separating line; for two squares the separating-axis theorem says more. Form the Minkowski sum \(K\) of the two (centered) squares: it is a zonogon whose facet normals are the side normals — the axes — of the two squares. Disjointness of interiors says the center displacement lies outside the interior of \(K\), hence violates one of \(K\)'s facet inequalities. Concretely: there is a unit vector \(n\), which is an axis of one of the two squares (call that square the owner), with \[ \langle Q-P,\,n\rangle \;\ge\; w_F(n)+w_G(n), \] where \(P,Q\) are the centers and \(w_F(n), w_G(n)\) are the projected half-widths of the two squares in direction \(n\). Such an inequality is a branch: a single linear inequality in the centers that certifies disjointness using only one-dimensional projection data.

When \(n\) is an axis of its owner, the owner contributes half-width exactly \(\tfrac12\), and the other square contributes \(\bigl(|\langle n,m\rangle|+|\det(n,m)|\bigr)/2\ge\tfrac12\) for any axis \(m\) of its frame. Writing \(t\in[0,\pi/4]\) for the angle between the two squares' orientations reduced modulo quarter turns, the threshold of an owned branch is \[ H(t)\;=\;\frac{1+\cos t+\sin t}{2}\;\ge\;1, \] with equality exactly when the squares are parallel (\(t=0\)). Two facts about \(H\) drive everything: it is at least \(1\), and it depends only on the two frames — not on which of the two squares owns the branch.

2. Freeze one branch per pair, then minimize

For each of the three pairs, pick one owned branch and one owner, and freeze them: frames, normals \(n_1,n_2,n_3\), thresholds \(H_1,H_2,H_3\), and owners are constants from now on. Orienting the normals cyclically, the frozen system reads \[ \langle d_i,\,n_i\rangle\;\ge\;H_i \qquad (i=1,2,3), \] where \(d_1=P_2-P_1\), \(d_2=P_3-P_2\), \(d_3=P_1-P_3\) are the cyclic edges of the center triangle. The squares themselves never move again; only the centers vary. The frozen system remains sufficient for disjointness as the centers move, because a branch certifies separation from the frozen frames' projection data alone. So we may minimize the doubled area \(D\) over center triples satisfying the three linear inequalities, non-obtuseness, and \(D\le D_0\).

The minimum exists. Cauchy–Schwarz gives \(\|d_i\|\ge\langle d_i,n_i\rangle\ge H_i\ge1\), so every feasible triangle has sides at least \(1\); an elementary lemma about non-obtuse triangles with long sides and doubled area below \(1\) then bounds every side by \(\sqrt2\) and shows the triangle is strictly acute. The feasible set is nonempty (the original configuration is in it), compact, and the minimizer satisfies \(0<D\le D_0<1\) and is acute. Acuteness matters later: it makes the angle constraints strictly slack, so first-order analysis only ever sees the three branch constraints.

3. Every branch is active at the minimum

Call a frozen branch active if its inequality holds with equality at the minimizer. (This is equality in a linear inequality on centers — it does not say the squares touch, and no square is ever moved.) Claim: all three branches are active.

The tool is single-vertex variation. When one vertex \(P\) moves, \(D\) is affine in \(P\) with gradient \(g\) equal to the quarter-turn of the opposite edge, so \(\|g\|\ge1\). If some vertex had no active incident branch, we could slide it down the gradient: the incident branches have slack, the third branch doesn't involve \(P\), and acuteness and \(D>0\) are open — a strictly better feasible point, contradiction. If a vertex had exactly one active incident branch with (locally oriented) normal \(n\), minimality over the half-plane of allowed velocities \(\{v:\langle n,v\rangle\ge0\}\) forces the gradient onto the normal ray: \(g=\mu n\) with \(\mu\ge1\). But the affine function \(X\mapsto D(X)\) vanishes when \(P\) is placed at either other vertex (the triangle degenerates), which yields \(\langle g, P-Q\rangle = D\) for the neighbor \(Q\) across the active branch, and then \[ D=\mu\,\langle n, P-Q\rangle=\mu H\ \ge\ 1, \] contradicting \(D<1\). A graph on three vertices in which every vertex has degree \(2\) is complete: all three branches are active.

4. First-order optimality as a force balance

Now use all three constraints at once. Normalize \(P_1=0\) and work in \(x=(P_2,P_3)\in\mathbb{R}^4\). The branch functions are linear in \(x\) (this is what the normalization buys), with constant gradients \[ a_1=(n_1,0),\qquad a_2=(-n_2,n_2),\qquad a_3=(0,-n_3). \] Minimality says: any velocity \(v\) that weakly preserves all three constraints, \(\langle a_i,v\rangle\ge0\), cannot decrease the area, \(\langle g,v\rangle\ge0\), where \(g\) is the area gradient. A finite Farkas lemma converts this into multipliers: \(g=\lambda_1a_1+\lambda_2a_2+\lambda_3a_3\) with \(\lambda_i\ge0\). (The Farkas lemma needs the generated cone to be closed; the paper gets this from a strict dual vector, and the minimization supplies one for free — the dilation direction \(w=x\) itself, since \(\langle a_i,x\rangle=H_i\ge1>0\) at contact.)

Read mechanically: the minimizer is a structure in equilibrium. Each active branch presses on the triangle along its frozen normal with force magnitude \(\lambda_i\); the multiplier equation says the net generalized force of the area objective is exactly balanced by the three contact forces. Define the forces \(f_i=\lambda_i n_i\). Resolving the \(\mathbb{R}^4\) multiplier equation into its two plane components, and writing \(J_\sigma\) for the quarter-turn in the triangle's orientation, gives \[ J_\sigma d_1=f_2-f_3,\qquad J_\sigma d_2=f_3-f_1,\qquad J_\sigma d_3=f_1-f_2 . \] The three force endpoints \(f_1,f_2,f_3\) form a triangle whose sides are the sides of the center triangle rotated a quarter turn, while each vertex \(f_i\) is pinned to the ray through the frozen normal \(n_i\), at distance \(\lambda_i\) from the origin. This is a reciprocal diagram in Maxwell's classical sense: the force polygon of a frame in equilibrium closes, and here it closes into a congruent, quarter-turned copy of the center triangle itself. All the remaining work is extracting scalar consequences from this one picture.

5. The Euler identity: forces convert to area

The objective (doubled area) is homogeneous of degree \(2\) in \(x\); the branch functions are homogeneous of degree \(1\). Euler's identity pairs the gradient with the position: \(\langle g,x\rangle=2D\), while \(\langle a_i,x\rangle=H_i\) at contact. Hence \[ 2D\;=\;\lambda_1H_1+\lambda_2H_2+\lambda_3H_3 . \] Think of it as virtual work under uniform dilation: inflating the configuration does work \(2D\) against the area and work \(\lambda_iH_i\) against each contact. Since \(D<1\), the entire remaining task is one inequality: \[ \lambda_1H_1+\lambda_2H_2+\lambda_3H_3\;\ge\;2 . \]

6. The sine system, and one case that dies immediately

Dotting the reciprocal equations with the normals produces three scalar equations in the oriented sines \(s_1=\sigma\det(n_1,n_2)\), \(s_2=\sigma\det(n_2,n_3)\), \(s_3=\sigma\det(n_3,n_1)\): \[ H_1=\lambda_2s_1+\lambda_3s_3,\qquad H_2=\lambda_3s_2+\lambda_1s_1,\qquad H_3=\lambda_1s_3+\lambda_2s_2 . \] If some sine is nonpositive, the system is over-rigid: say \(s_3\le0\); dropping that term from the first equation gives \(1\le H_1\le\lambda_2\), and bounding both sines by \(1\) in the second gives \(1\le H_2\le\lambda_1+\lambda_3\). So \(\sum\lambda_i\ge2\), hence \(\sum\lambda_iH_i\ge2\), done. From here on all three sines are positive, which means the three normals occur in positive cyclic order around the circle.

7. The ownership tournament

Each frozen branch has a fixed owner: the square whose axis supplies the normal. Direct each edge of the center triangle away from its owner. The result is a tournament on three vertices, and every such tournament is either a directed \(3\)-cycle or transitive (a source owning two branches, a middle, and a sink). The eight possible owner assignments reduce to these two geometries by relabeling; the paper fixes the bookkeeping once (cyclic shifts preserve everything; a transposition flips the orientation \(\sigma\), reverses all branch normals, and swaps \(s_1\leftrightarrow s_2\)). Ownership carries no metric information — the threshold is the same whichever square owns the branch — but it carries one discrete fact that decides the endgame: two branches with the same owner have normals drawn from the axes of a single frame, hence parallel or perpendicular.

8. Cyclic owners: winding and a symmetric inequality

In the cyclic case each square supplies exactly one normal. Let \(\gamma_i\) be the directed gap from \(n_i\) to \(n_{i+1}\); positivity of the sines puts each \(\gamma_i\) in \((0,\pi)\), so the three gaps sum to exactly \(2\pi\): the normals wind once around the circle. In half-angle cotangent coordinates \(u=\cot(\gamma_1/2)\), \(v=\cot(\gamma_2/2)\), \(w=\cot(\gamma_3/2)\) (all positive), the winding constraint becomes the single algebraic relation \[ uv+vw+wu=1 . \] Each threshold becomes a value of one rational function: \(H_i=F(q)\) with \(F(q)=\frac{(1+q)\max\{1,q\}}{1+q^2}\) at \(q=u,v,w\). Substituting the sine system into a weighted sum of the thresholds, each \(\lambda_i\) collects the constant coefficient \(2\) — the pairing of weights to thresholds is rigid and forced — giving the weighting identity \[ 2(\lambda_1+\lambda_2+\lambda_3)=H_1(u+w)+H_2(u+v)+H_3(v+w). \] The case then reduces to a self-contained scalar fact: for \(u,v,w>0\) with \(uv+vw+wu=1\), \[ F(u)(u+w)+F(v)(u+v)+F(w)(v+w)\;\ge\;4 . \] Its proof (the paper's appendix) splits on whether some variable exceeds \(1\) — at most one can — and uses an Engel-form Cauchy–Schwarz estimate in one case and three termwise estimates ending in \(u+1/u\ge2\) in the other. So \(\sum\lambda_i\ge2\) and hence \(\sum\lambda_iH_i\ge2\).

9. Transitive owners: rigidity and a dual certificate

In the transitive case the source owns two branches, so \(n_1\) and \(n_3\) are both axes of the source's frame: parallel or perpendicular. Parallel would force \(s_3=0\), excluded; so \(n_1\perp n_3\) and \(s_3=1\). Expanding \(n_2\) in the orthonormal basis \((n_1,n_3)\) gives \(s_1^2+s_2^2=1\), so the whole configuration collapses to one parameter: \(s_1=\cos t\), \(s_2=\sin t\) for some \(t\in(0,\pi/2)\). Writing \(A,B,C\) for the three thresholds (the identification uses the owner-independence of \(H\)), the sine system becomes \[ A=c\lambda_2+\lambda_3,\qquad B=c\lambda_1+s\lambda_3,\qquad C=\lambda_1+s\lambda_2, \] with \(c=\cos t\), \(s=\sin t\) and \(A=(1+c+s)/2\) determined by the source geometry.

Two ingredients close it. First, a triangle inequality among thresholds: \(G=H-1\) is increasing, concave, and vanishes at \(0\), hence subadditive, and the metric triangle inequality on the frame circle \(\mathbb{R}/(\pi/2)\mathbb{Z}\) gives the frame excess bound \(A+1\le B+C\). Second, an explicit dual certificate: in the rational parametrization \(r=\tan(t/2)\in(0,1)\), there are explicit rational functions \(\alpha,\beta,K\ge0\) with \[ A\lambda_1+\lambda_2+\lambda_3-2 =\alpha\,(C-1)+\beta\,(B+C-A-1)+K \] identically, given the system. The right side is a nonnegative combination of the two known-nonnegative slacks plus a nonnegative constant, so \(A\lambda_1+\lambda_2+\lambda_3\ge2\), and since \(B,C\ge1\), \(\sum\lambda_iH_i=A\lambda_1+B\lambda_2+C\lambda_3\ge2\). The certificate is not an accident: \((\alpha,\beta)\) is the solution of the \(2\times2\) linear system that cancels the multiplier dependence — the dual solution of a small linear program — and \(K\) is the leftover constant, which happens to be nonnegative on \((0,1)\).

10. Assembly

The three cases — some sine nonpositive, all positive with cyclic owners, all positive with transitive owners — are exhaustive, and each gives \(\lambda_1H_1+\lambda_2H_2+\lambda_3H_3\ge2\). By the Euler identity, \(2D\ge2\), so the minimizer has doubled area \(D\ge1\). But the minimizer was constrained to \(D\le D_0<1\). No counterexample exists.

Sharpness and limits

Equality. Axis-parallel unit squares centered at \((0,0)\), \((1,0)\), \((0,1)\): interiors pairwise disjoint (two shared edges, one shared corner), center triangle right isosceles with legs \(1\), area exactly \(\tfrac12\).

The angle hypothesis is necessary. Axis-parallel squares centered at \((0,0)\), \((1,\varepsilon)\), \((2,0)\) are disjoint with center-triangle area \(\varepsilon\), arbitrarily small; the middle angle is obtuse. Without any angle hypothesis the correct bound is \(\operatorname{area}\ge\tfrac12\sin\theta\) for every angle \(\theta\) of the triangle.

No four-center analogue. Four centers in strict convex position can span convex hulls of arbitrarily small positive area, even for axis-parallel squares pairwise disjoint as closed sets: centers \((0,0)\), \((L,\varepsilon)\), \((2L,-\varepsilon)\), \((3L,0)\) give hull area \(3L\varepsilon\to0\).

Verification status

The main theorem is machine-checked in Lean 4 over mathlib, twice, by unrelated proofs.

To repeat the banner: the formal verification covers the headline theorem, but the paper's prose, the sharpness section, and this page have not yet been adequately human reviewed.