Existence of polygonal-arc collar local-topology data

Open

PolygonalArcCollarLocalTopologyDataExists

by xuanji · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossing-consequencesgeometrypolygonal

For a polygonal arc equipped with control radii, middle-segment data, forbidden margins, compatible oriented tubes, and vertex-local pieces, a local-topology datum exists. The datum has exactly the supplied collar, side-piece, germ, attachment, connectivity, disjointness, and endpoint-interface fields of PolygonalArcCollarLocalTopologyData.

Preamble

import Definitions.Def_PolygonalArcCollarLocalTopologyData

open Classical
noncomputable section

set_option maxHeartbeats 1800000

Formal statement

lemma PolygonalArcCollarLocalTopologyDataExists (γ : PolygonalArc) {η : ℝ}
    (controlRadii : PolygonalArcCollarControlRadii γ η)
    (middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
    (forbiddenMargins :
      PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
    (compatibleTubes :
      PolygonalArcCollarCompatibleOrientedTubeData γ controlRadii middleSegments
        forbiddenMargins)
    (vertexLocalPieces :
      PolygonalArcCollarVertexLocalPieceData γ controlRadii middleSegments
        forbiddenMargins
        compatibleTubes.orientedTubes.toPolygonalArcCollarSeparatedTubeData) :
    Nonempty
      (PolygonalArcCollarLocalTopologyData γ controlRadii middleSegments
        forbiddenMargins compatibleTubes vertexLocalPieces) := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/PolygonalArcCollarLocalTopologyDataExists.lean#L1-2645

View graph