AI 中文总结
该论文证明了Meir-Moser矩形打包问题的尾部版本：存在阈值m0，使得从m0开始的倒数矩形族可平移旋转装入边长为m^{-1/2}的正方形，面积恰好相等，并给出六步构造证明，经Lean 4验证。
AI 中文摘要
Meir--Moser 矩形打包问题询问是否可以将所有边长分别为 \\(1/n\\) 和 \\(1/(n+1)\\)（其中 \\(n\ge1\\)）的矩形以两两不相交的内部装入单位正方形。我们建立了该问题的尾部版本。设 \\(R_n\\) 表示具有这些边长的矩形。我们证明存在一个整数 \\(m_0\\)，使得对于每个 \\(m\ge m_0\\)，族 \\(\{R_n:n\ge m\}\\) 通过平移和直角旋转，可以以两两不相交的内部装入边长为 \\(m^{-1/2}\\) 的正方形。该正方形的面积等于所有矩形面积之和。该几何构造递归地分解矩形间隙，而局部随机配额和随机排列分配后续整数索引。我们分别控制等待间隙的总面积和每个索引处的分配负载。证明分为六个步骤：有限前缀约简、几何行分解、面积自举、尖锐源负载估计、实际自适应构造的控制以及紧致性极限。对于每个有限时间范围，失败概率有一个独立于该范围且可以任意小的界。自适应步骤使用永久负载账本、实际的新鲜高度查询，以及与冻结源实验的单侧比较。紧致性随后产生无限打包。最终的打包陈述已在 Lean 4 中检查。充分阈值为 \\(m_0=10^{1000}\\)。此结果仅适用于足够晚的尾部，并未解决从 \\(n=1\\) 开始的完整序列的原始 Meir--Moser 矩形打包问题，该问题仍然开放。
英文摘要
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.
CommentsBlog is coming soon
