Existence of polygonal arc collar parameter data
ProvedPolygonalArcCollarParameterDataExistsdecompositiongeometrypolygonal-collar
For a polygonal arc with fixed control radii, middle segments, and forbidden margins, there exists a coherent parameter package for every segment. It supplies the left and right normalized parameters, a segment-length scale, a positive slack, lower and upper tube parameters, and the positively oriented normal.
The package includes the exact identities with the control-radius formulas and the inequalities needed to place the interval strictly inside the segment parameter range, together with the orthogonality and norm relations for the normal. It is the parameter-phase interface used by the subsequent compact-separation and tube-construction phases.
Preamble
import Definitions.Def_PolygonalArcCollarParameterData import Theorems.Thm_PlanarRot90Norm import Theorems.Thm_PlanarRot90Orthogonal open Classical noncomputable section
Formal statement
theorem PolygonalArcCollarParameterDataExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
(forbiddenMargins :
PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments) :
Nonempty
(PolygonalArcCollarParameterData γ controlRadii middleSegments forbiddenMargins) := by sorrySource