← All papers
First page of Closed escape path of smallest diameter in forest: dual formulation of Lebesgue's universal covering problem

Closed escape path of smallest diameter in forest: dual formulation of Lebesgue's universal covering problem

Zhipeng Deng

math.MG Sep 26, 2026 · v1 math.OC
Theorems 1-7 on the Lebesgue universal covering duality are formalized in Lean 4 using Mathlib, defining rigid motions, covers, and constant-width bodies.
Lebesgue's universal covering problem asks for the minimum area convex planar region capable of containing a congruent copy of every planar set of diameter at most one. In this paper, we develop an exact dual formulation of this problem through a minimum diameter analogue of Bellman's lost-in-a-forest problem. For a compact convex forest $F$, we define the critical escape diameter $D(F)$ as the minimum diameter of a closed path whose trace cannot be placed, under any rigid motion, entirely in the interior of $F$. We prove attainment of this minimum and establish a diameter cover/escape duality showing that the normalized body $D(F)^{-1}F$ is a Lebesgue universal cover. Consequently, the Lebesgue universal covering constant admits the exact representation \[ \mathcal L=\inf_F\frac{\operatorname{Area}(F)}{D(F)^2}, \] where the infimum ranges over compact convex planar bodies with nonempty interior. By reversing the rigid motion, we further characterize escape as intersection of a fixed path with every oppositely transformed boundary of $F$, and derive equivalent continuous curve, convex body, and support function optimization formulations. To make the infinite dimensional problem computationally tractable while retaining rigorous control of approximation error, we discretize the compact configuration space by an $η_m$-net and formulate the resulting problem as a minimum diameter traveling salesman problem with neighborhoods; for polygonal forests, an exact mixed-integer second-order cone formulation is obtained. We prove the quantitative certification, which yields convergent, rigorously certified universal cover bounds. The framework replaces finite tests of prescribed constant width shapes by a unified optimization over the full configuration space and extends naturally to other congruent and translative universal cover problems.

Lebesgue's universal covering problem seeks the minimum-area convex planar region containing a congruent copy of every planar set of diameter one. Existing bounds rely on ad hoc geometric refinement over a few prescribed shapes.

A dual formulation is developed via a minimum-diameter analogue of Bellman's lost-in-a-forest problem, defining a critical escape diameter D(F) for compact convex forests. A diameter cover/escape duality shows D(F)^{-1}F is a universal cover, giving an exact representation of the covering constant as an infimum of Area(F)/D(F)^2. The infinite-dimensional problem is discretized via an eta_m-net into a minimum-diameter traveling salesman problem with neighborhoods, with a mixed-integer second-order cone formulation for polygonal forests. Theorems 1-7 are formalized in Lean 4 with Mathlib, encoding rigid motions, covers, support functions, and constant-width-one bodies.

The paper proves attainment of the minimum escape diameter and establishes the cover/escape duality, yielding convergent, rigorously certified universal cover bounds. The framework extends to other congruent and translative universal cover problems, and the Lean formalization certifies the main theorems.