Theorems 4-8 characterizing support-function constraints for the triangular lost-in-a-forest problem are formalized in Lean 4 with Mathlib.
Abstract
In this paper, we present a general formulation to address the problems of covering curves and polygonal chains with triangle, and fitting these curves into triangle. These problems can be formulated as special cases of Bellman's lost-in-a-forest problem (escaping triangular forest) and Moser's worm problem (covered by triangle). We model and reformulate the problem by keeping the curve stationary while allowing the triangle to translate and rotate. Subsequently, we derive the functional minimization formulation with support function constraints to solve. We also prove the equivalence and convergence of the formulas. Finally, we employ numerical methods and present results for covering curves with arbitrary triangles of various angles. We also present some corollaries and variant results, including closed curves and closed polygonal chains.
Problem
Bellman's lost-in-a-forest problem and Moser's worm problem lack general solutions for arbitrary triangular forests. No generalized algorithmic solution or proof exists for covering curves and polygonal chains with arbitrary triangles.
Approach
The escape path is transformed by keeping the curve stationary while translating and rotating the triangle, reformulating the problem as a Traveling Salesperson Problem with Neighborhoods. A functional minimization formulation with support-function constraints is derived, and equivalence and convergence of the formulas are proved. The support-characterization theorems (Theorems 4-8) are formalized in Lean 4 using Mathlib.
Figure 1 : Proof concept for escaping from arbitrary triangle forest, and fitting worm into triangle
Results
Numerical results for triangle covering curves and polygonal chains are computed for base angles at 5-degree multiples. Isosceles-triangle results match Gibbs's earlier work, and results for arbitrary non-isosceles triangles are obtained for the first time.
