Contacts when attaching split fans to exterior routes

Every contact between an interior spoke and an exterior cut route is its own boundary port, at the corresponding actual route end. Distinct edge-end occurrences remain separate, including the two cut ends of a target loop.

theorem Cslib.Complexity.Graph.PolygonalDrawing.contractionLift_vertex_contractedIndex (G : Graph) (u v : ℕ) (e : Fin G.edges.length) (side : Bool) : (RotationSystem.contractionLift G u v ((contractedIndex G u v) e, side)).vertex = Dart.vertex (e, side)

The lifted original end of a retained contracted occurrence has its original name.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.split_spoke_contact {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) {ρ : ℝ} (hρ : 0 < ρ) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (f : ℂ →ᵃ[ℝ] ℝ) (hsep : f b < f a) (hpa : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = u → f a < f (D.cutPort ρ ↑d)) (hpb : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = v → f (D.cutPort ρ ↑d) < f b) (d e : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }) (hde : d ≠ e) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap (D.restoredVertex a b (RotationSystem.contractionLift G u v ↑d).vertex) (D.cutPort ρ ↑d)) s = (AffineMap.lineMap (D.restoredVertex a b (RotationSystem.contractionLift G u v ↑e).vertex) (D.cutPort ρ ↑e)) t) : s = 0 ∧ t = 0

The automatically separated fans meet only at their own centers, including the two distinct ends of one target loop. Opposite fan assignments cannot meet.

theorem Cslib.Complexity.Graph.PolygonalDrawing.split_spoke_connector_contact {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (f : ℂ →ᵃ[ℝ] ℝ) (hsep : f b < f a) (hpa : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = u → f a < f (D.cutPort ρ ↑d)) (hpb : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = v → f (D.cutPort ρ ↑d) < f b) (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap (D.restoredVertex a b (RotationSystem.contractionLift G u v ↑d).vertex) (D.cutPort ρ ↑d)) s = (AffineMap.lineMap a b) t) : s = 0 ∧ ((RotationSystem.contractionLift G u v ↑d).vertex = u ∧ t = 0 ∨ (RotationSystem.contractionLift G u v ↑d).vertex = v ∧ t = 1)

A split spoke meets the new connector only at its assigned center and the corresponding original source endpoint. Every real connector parameter is included.

theorem Cslib.Complexity.Graph.PolygonalDrawing.split_spoke_vertex_contact {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (f : ℂ →ᵃ[ℝ] ℝ) (hsep : f b < f a) (hpa : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = u → f a < f (D.cutPort ρ ↑d)) (hpb : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = v → f (D.cutPort ρ ↑d) < f b) (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }) (w : ℕ) (hw : w = u ∨ w = v) {s : ℝ} (hs : s ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap (D.restoredVertex a b (RotationSystem.contractionLift G u v ↑d).vertex) (D.cutPort ρ ↑d)) s = D.restoredVertex a b w) : s = 0 ∧ (RotationSystem.contractionLift G u v ↑d).vertex = w

A split spoke visits a restored source vertex only at its own original end.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.spoke_outsideRoute_contact {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) {a : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (d : G.Dart) (hd : d.vertex = v) (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (AffineMap.lineMap a (D.cutPort ρ d)) s = (D.outsideRoute v ρ e).eval i t) : s = 1 ∧ ∃ (side : Bool), d = (e, side) ∧ (D.outsideRoute v ρ e).AtEnd i t side

An interior spoke can meet an exterior route only at its own cut port and corresponding actual end. The radius's exterior-contact property is supplied by IsEmbedding.exists_restriction, rather than by a geometric drawing provider.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.outsideRoute_not_mem_ball {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (D.outsideRoute v ρ e).eval i t ∉ Metric.ball (D.vertex v) ρ

The exterior restriction is disjoint from the open replacement ball.

theorem Cslib.Complexity.Graph.PolygonalDrawing.outsideRoute_ne_center_of_contacts {G : Graph} (D : G.PolygonalDrawing) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hports : ∀ (d : G.Dart), d.vertex = v → dist (D.cutPort ρ d) (D.vertex v) = ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (D.outsideRoute v ρ e).eval i t ≠ D.vertex v

An exterior route cannot contain the old center of its replacement circle.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.outsideRoute_edge_contacts {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (e f : Fin G.edges.length) (hef : e ≠ f) (i : Fin (D.outsideRoute v ρ e).segments) (j : Fin (D.outsideRoute v ρ f).segments) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (D.outsideRoute v ρ e).eval i s = (D.outsideRoute v ρ f).eval j t) : ∃ (side : Bool) (tag : Bool), (D.outsideRoute v ρ e).AtEnd i s side ∧ (D.outsideRoute v ρ f).AtEnd j t tag ∧ Dart.vertex (e, side) = Dart.vertex (f, tag)

Contacts of two different exterior pieces are inherited from old common ends. Both real parameters are transported through the independent cut maps.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.outsideRoute_vertex_contacts {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (w : ℕ) (hw : w ∈ G.vertices) (heq : (D.outsideRoute v ρ e).eval i t = D.vertex w) : ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = w

A declared old vertex on an exterior piece remains at its own unchanged original end. The two independent cut maps preserve its endpoint occurrence.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.prepend_outsideRoute_simple {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) {a : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (e : Fin G.edges.length) (he : Dart.vertex (e, false) = v) (hp : (D.outsideRoute v ρ e).IsSimple) : (Polygonal.Route.prepend a (D.outsideRoute v ρ e)).IsSimple

Attach a new first spoke to an actual exterior piece, preserving full continuous simplicity. Its only contact with that piece is the intended first cut port.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.append_outsideRoute_simple {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) {b : ℂ} (hb : b ∈ Metric.ball (D.vertex v) ρ) (e : Fin G.edges.length) (he : Dart.vertex (e, true) = v) (hp : (D.outsideRoute v ρ e).IsSimple) : ((D.outsideRoute v ρ e).append b).IsSimple

Attach a new last spoke to an actual exterior piece. The old first end, if unmodified, is retained exactly.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.attach_outsideRoute_simple {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hcut : ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (e : Fin G.edges.length) (he₀ : Dart.vertex (e, false) = v) (he₁ : Dart.vertex (e, true) = v) (hp : (D.outsideRoute v ρ e).IsSimple) (hspokes : ∀ (s t : ℝ), s ∈ Set.Icc 0 1 → t ∈ Set.Icc 0 1 → (AffineMap.lineMap a (D.cutPort ρ (e, false))) s = (AffineMap.lineMap b (D.cutPort ρ (e, true))) t → s = 0 ∧ t = 0) : ((Polygonal.Route.prepend a (D.outsideRoute v ρ e)).append b).IsSimple

Reattach two independent ends of a cut route, permitting precisely the intended new loop closure. The spoke-contact premise is discharged by the internally constructed same-center fan or separated two-fan geometry, including reopened target loops.