Existence of compact centerline separation data
ProvedPolygonalArcCollarCenterlineSeparationDataExistscompactnessdecompositiongeometrypolygonal-collar
Given the parameter package for a polygonal arc collar, there exist positive initial, terminal, and successive separation functions. They bound the distance between the trimmed centerline portions and their neighboring segments or centerline portions.
The conclusion preserves the original control-radius parameter intervals exactly. This is the compactness and positive-separation interface used to choose a tube width that remains away from all nonincident geometric pieces.
Preamble
import Definitions.Def_PolygonalArcCollarCenterlineSeparationData import Theorems.Thm_PositiveSeparation open Classical noncomputable section -- compact centerline/PositiveSeparation phase.
Formal statement
theorem PolygonalArcCollarCenterlineSeparationDataExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
(forbiddenMargins :
PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
(parameters :
PolygonalArcCollarParameterData γ controlRadii middleSegments forbiddenMargins) :
Nonempty
(PolygonalArcCollarCenterlineSeparationData γ controlRadii middleSegments
forbiddenMargins parameters) := by sorrySource