Existence of compatible oriented tube data
ProvedPolygonalArcCollarCompatibleOrientedTubeDataExistsgeometrytopology
For a polygonal arc with fixed control radii, middle segments, and middle forbidden margins, there exists compatible oriented tube data satisfying all of the structural, separation, and cone-compatibility fields in its definition.
Preamble
import Definitions.Def_PolygonalArcCollarCompatibleOrientedTubeData open Classical noncomputable section
Formal statement
lemma PolygonalArcCollarCompatibleOrientedTubeDataExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
(forbiddenMargins :
PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments) :
Nonempty
(PolygonalArcCollarCompatibleOrientedTubeData γ controlRadii middleSegments
forbiddenMargins) := by sorrySource