Promotion and Extension of General Escape-Covering Duality Relationship
Zhipeng Deng
math.MG
Oct 31, 2026 · v1
TL;DR
Includes a Lean 4/Mathlib companion file stating a named theorem for each manuscript result, exposing the dependency graph; explicitly not an end-to-end formalization.
Abstract
Bellman's lost-in-a-forest problem, Moser's worm problem, Lebesgue's universal covering problems, and the classical 'fits and covers' questions can be organized by a common obstruction principle: an object fits a region if some admissible group action places it in the region, whereas an escape object is one for which every placement fails to remain in the interior. In this paper, we develop a general theory of escape-covering duality for any dimension and explore several applications. For convex translation covers of all closed planar curves of Euclidean length one, we prove $ W \ge f(\sqrt3/9)+c_1>0.15545785378555,c_1=0.000009944944227372... $ Here $f(\sqrt3/9)$ is Wetzel's classical lower bound. For a rational polytopal Minkowski gauge and prescribed rational facet directions, we express universal closed-loop cover feasibility as a rational polyhedron in the facet offsets. After removing translations, minimum volume is attained at a vertex. Refining the facet directions gives explicit two-sided rational bounds for the unrestricted fixed-gauge worm constant. Four exact benchmarks recover known sharp values. The construction uses an elementary circuit–circumradius form of the established non-fitting-polygon and capacity theory. We supply its support and ledger derivation, the finite complete test family in arbitrary dimension, a cover vertex bound, and the resulting algebraicity statement. The surrounding escape–covering framework includes endpoint placement, attainment, gauge stability, and finite-to-continuum error bounds. For nonsymmetric gauges the objects are parametrized closed curves, so orientation-dependent length is retained. Through the published capacity identity, the improved Wetzel estimate gives a product volume–capacity factor below $1.023781939711102$ for every planar ellipsoidal gauge.
Problem
Bellman's lost-in-a-forest problem, Moser's worm problem, Lebesgue's universal covering problems, and fits-and-covers questions share a common obstruction principle. The work seeks a general escape-covering duality theory in any dimension. A specific target is the area of the smallest convex translation cover of all closed planar curves of length one.
Approach
A threshold identity relates escape objects to strict placements. Balanced supports, signed translation margins, and directed ledgers then give a centered circuit-circumradius formula. For rational polytopal gauges with fixed facet directions, cover feasibility becomes a rational polyhedron in facet offsets, and minimum volume is attained at a vertex. A width-deficit and tangency argument strengthens Wetzel's lower bound. A Lean 4/Mathlib companion file records a named theorem for each of the 80 proved results, making the logical dependency graph kernel-visible. Domain-specific bridge results are not fully formalized, and the numerical bound is not formally proved.
Results
The area of the cover satisfies W ≥ f(√3/9) + c₁ > 0.15545785378555, improving Wetzel's bound. The method gives explicit two-sided rational bounds for fixed-gauge worm constants and recovers four known sharp benchmarks. It also yields a volume-capacity factor below 1.023781939711102 for every planar ellipsoidal gauge.
