Parameter classification for restored graph routes

Every parameter belongs either to the unchanged exterior piece, the new first spoke, or the new last spoke. Exact global positions distinguish the two end occurrences even for a restored loop. No simplicity or geometric provider is needed for these data laws.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute_eval_cases {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (i : Fin (D.restoredRoute ρ a b e).segments) (t : ℝ) : have p := D.outsideRoute v ρ ((contractedIndex G u v) e); have w₀ := Dart.vertex (e, false); have w₁ := Dart.vertex (e, true); (∃ (j : Fin p.segments), (D.restoredRoute ρ a b e).eval i t = p.eval j t ∧ (D.restoredRoute ρ a b e).position i t = ↑(attachmentCount u v w₀) + p.position j t) ∨ (w₀ = u ∨ w₀ = v) ∧ (D.restoredRoute ρ a b e).eval i t = (AffineMap.lineMap (D.restoredVertex a b w₀) (D.cutPort ρ ((contractedIndex G u v) e, false))) t ∧ (D.restoredRoute ρ a b e).position i t = t ∨ (w₁ = u ∨ w₁ = v) ∧ (D.restoredRoute ρ a b e).eval i t = (AffineMap.lineMap (D.cutPort ρ ((contractedIndex G u v) e, true)) (D.restoredVertex a b w₁)) t ∧ (D.restoredRoute ρ a b e).position i t = ↑p.segments + ↑(attachmentCount u v w₀) + t

Classify every actual parameter of a restored retained edge, recording its global position and retaining both independently attached end occurrences.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute_atEnd_of_exterior {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (i : Fin (D.restoredRoute ρ a b e).segments) (j : Fin (D.outsideRoute v ρ ((contractedIndex G u v) e)).segments) (t : ℝ) (side : Bool) (hpos : (D.restoredRoute ρ a b e).position i t = ↑(attachmentCount u v (Dart.vertex (e, false))) + (D.outsideRoute v ρ ((contractedIndex G u v) e)).position j t) (hat : (D.outsideRoute v ρ ((contractedIndex G u v) e)).AtEnd j t side) (hunchanged : ¬(Dart.vertex (e, side) = u ∨ Dart.vertex (e, side) = v)) : (D.restoredRoute ρ a b e).AtEnd i t side

An unchanged exterior endpoint retains its exact original end tag in the restored route. Positive attachments at the other end are counted explicitly.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute_atEnd_first {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (i : Fin (D.restoredRoute ρ a b e).segments) {t : ℝ} (hpos : (D.restoredRoute ρ a b e).position i t = t) (ht : t = 0) : (D.restoredRoute ρ a b e).AtEnd i t false

The initial spoke's zero parameter is the restored first end.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute_atEnd_last {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (i : Fin (D.restoredRoute ρ a b e).segments) {t : ℝ} (hactive : Dart.vertex (e, true) = u ∨ Dart.vertex (e, true) = v) (hpos : (D.restoredRoute ρ a b e).position i t = ↑(D.outsideRoute v ρ ((contractedIndex G u v) e)).segments + ↑(attachmentCount u v (Dart.vertex (e, false))) + t) (ht : t = 1) : (D.restoredRoute ρ a b e).AtEnd i t true

The final spoke's unit parameter is the restored last end.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute_trace_cases {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (i : Fin (D.restoredRoute ρ a b e).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (∃ (j : Fin (D.outsideRoute v ρ ((contractedIndex G u v) e)).segments), (D.restoredRoute ρ a b e).eval i t = (D.outsideRoute v ρ ((contractedIndex G u v) e)).eval j t ∧ (D.restoredRoute ρ a b e).position i t = ↑(attachmentCount u v (Dart.vertex (e, false))) + (D.outsideRoute v ρ ((contractedIndex G u v) e)).position j t) ∨ ∃ (side : Bool), ∃ s ∈ Set.Icc 0 1, (Dart.vertex (e, side) = u ∨ Dart.vertex (e, side) = v) ∧ (D.restoredRoute ρ a b e).eval i t = (AffineMap.lineMap (D.restoredVertex a b (Dart.vertex (e, side))) (D.cutPort ρ ((contractedIndex G u v) e, side))) s ∧ (s = 0 → (D.restoredRoute ρ a b e).AtEnd i t side)

A parameter lies on the exterior piece or on one outward-oriented split spoke. The zero outward parameter retains the corresponding actual source end.