Existence of polygonal-arc collar vertex-local piece data
ProvedPolygonalArcCollarVertexLocalPieceDataExistscrossing-consequencesgeometrypolygonal
For a polygonal arc with control radii, middle-segment data, forbidden margins, and separated tube data, there exists a vertex-local-piece datum. The datum supplies the vertex disks, endpoint pieces, left and right local pieces, attachment sets, and their structural interface fields.
Preamble
import Definitions.Def_PolygonalArcCollarVertexLocalPieceData open Classical noncomputable section set_option maxHeartbeats 1200000
Formal statement
lemma PolygonalArcCollarVertexLocalPieceDataExists (γ : PolygonalArc) {η : ℝ}
(controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
(forbiddenMargins :
PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
(separatedTubes :
PolygonalArcCollarSeparatedTubeData γ controlRadii middleSegments
forbiddenMargins) :
Nonempty
(PolygonalArcCollarVertexLocalPieceData γ controlRadii middleSegments
forbiddenMargins separatedTubes) := by sorrySource