← All papers
First page of Packing Tails of Reciprocal Rectangles into Squares of Equal Area

Packing Tails of Reciprocal Rectangles into Squares of Equal Area

Yu Jiang

cs.DM Sep 23, 2026 · v1 math.CO
The final packing statements of the tail rectangle-packing theorem were checked in Lean 4.
The Meir–Moser rectangle-packing problem asks whether all rectangles with side lengths \(1/n\) and \(1/(n+1)\), for \(n\ge1\), can be packed into the unit square with pairwise disjoint interiors. We establish a tail version of this problem. Let \(R_n\) denote the rectangle with these side lengths. We prove that there exists an integer \(m_0\) such that, for every \(m\ge m_0\), the family \(\{R_n:n\ge m\}\) admits a packing, by translations and right-angle rotations, into a square of side length \(m^{-1/2}\), with pairwise disjoint interiors. The area of the square equals the sum of the areas of all the rectangles. The geometric construction recursively decomposes rectangular gaps, while local randomized quotas and random permutations assign subsequent integer indices. We separately control the total area of waiting gaps and the assignment load at each index. The proof is organized in six steps: a finite-prefix reduction, geometric row decompositions, an area bootstrap, a sharp source-load estimate, control of the actual adaptive construction, and a compactness limit. For every finite time horizon, the probability of failure has a bound that is independent of the horizon and can be made arbitrarily small. The adaptive step uses a permanent load ledger, actual fresh height queries, and a one-sided comparison with a frozen source experiment. Compactness then yields an infinite packing. The final packing statements have been checked in Lean 4. A sufficient threshold is \(m_0=10^{1000}\). This result applies only to sufficiently late tails and does not resolve the original Meir–Moser rectangle-packing problem for the full sequence starting at \(n=1\), which remains open.

The Meir–Moser problem asks whether all rectangles with side lengths 1/n and 1/(n+1) can be packed into the unit square with disjoint interiors. This remains open for the full sequence starting at n=1.

A tail version is established: for every m above a threshold m_0, the rectangles {R_n : n≥m} pack into a square of side m^{-1/2} whose area equals the total rectangle area. The construction recursively decomposes rectangular gaps and uses local randomized quotas and random permutations to assign integer indices, separately controlling waiting-gap area and assignment load. The proof proceeds in six steps: finite-prefix reduction, geometric row decompositions, area bootstrap, source-load estimate, adaptive construction control, and a compactness limit. The final packing statements were checked in Lean 4.

An equal-area tail packing is proven with a sufficient threshold m_0 = 10^{1000}. For every finite horizon the failure probability admits a horizon-independent bound that can be made arbitrarily small, and compactness yields an infinite packing. The result does not resolve the original problem starting at n=1.