Improved bounds for universal convex covers of unit arcs
En palabras de los autores
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 , reducing the gap between the previous refereed bounds by over . 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 . For the upper bound, we construct a quadrilateral of area 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.
Apareció: lunes, 21 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: 22 pages, 9 figures. Lean 4 formalization, code, and certificates available at https://github.com/ethan-keller/moser-worm-improved-bounds