单位弧的通用凸覆盖的改进界
Improved bounds for universal convex covers of unit arcs
AI总结：
本研究改进 Moser 蠕虫问题的凸通用覆盖面积界至 [0.239, 0.24633]，通过有限细分证明下界和构造四边形证明上界，并用 Lean 4 形式化验证。
AI中文摘要：
Moser 蠕虫问题要求寻找一个面积最小的平面区域，使得它能包含每条单位弧的一个全等副本。我们证明了凸通用覆盖的下确界面积 $\alpha$ 满足 $0.239\le\alpha\le0.24633\ldots$，将先前经审阅的界之间的差距缩小了超过 $75\\%$。对于下界，我们选择四条单位折线弧，并通过有限细分证明，无论它们如何放置，其凸包的面积至少为 $0.239$。对于上界，我们构造了一个面积为 $0.24633\ldots$ 的四边形，并通过证明其支撑不等式迫使未被覆盖的弧长度大于 1 来证明覆盖的普遍性。完整证明已在 Lean 4 中形式化，并由 Lean 内核验证。代码和证书可在该 https URL 获取。
英文摘要：
Moser's worm problem asks for a planar region of least area containing a congruent copy of every unit arc. We show that the infimum area $α$ among convex universal covers satisfies $0.239\leα\le0.24633\ldots$, reducing the gap between the previous refereed bounds by over $75\%$. For the lower bound, we choose four unit polygonal arcs and prove by finite subdivision that, however they are placed, their convex hull has area at least $0.239$. For the upper bound, we construct a quadrilateral of area $0.24633\ldots$ and prove cover universality by showing that its support inequalities force uncovered arcs to have length greater than one. The full proof is formalized in Lean 4 and verified by the Lean kernel. Code and certificates are available at https://github.com/ethan-keller/moser-worm-improved-bounds.
