Perturbing a path off a finite set (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §7). Every path with endpoints off a finite set S is homotopic (rel endpoints) to one whose whole range avoids S.

Main declarations:

• RS.nonempty_open_diff_finite — a nonempty open subset of a manifold minus a finite set is still nonempty.
• RS.exists_homotopic_avoiding_of_ball — the single-chart-ball base case (planar avoidance transported through the chart).
• RS.exists_homotopic_avoiding / RS.Loop.exists_homotopic_avoiding — the general theorem: any path (loop) with endpoints (basepoint) off a finite set S is homotopic rel endpoints to one avoiding S entirely.

theorem RS.nonempty_open_diff_finite {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (hU : IsOpen U) (hne : U.Nonempty) {S : Set X} (hS : S.Finite) : (U \ S).Nonempty

A nonempty open subset of X minus a finite set is still nonempty (through a chart, ℂ-minus-countable-is-dense).

theorem RS.exists_homotopic_avoiding_of_ball {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {a b : X} (γ : Path a b) {e : OpenPartialHomeomorph X ℂ} (_he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {c : ℂ} {r : ℝ} (hballsub : Metric.ball c r ⊆ e.target) (hγsrc : Set.range ⇑γ ⊆ e.source) (hγball : ∀ (t : ↑unitInterval), ↑e (γ t) ∈ Metric.ball c r) {S : Set X} (hS : S.Finite) (ha : a ∉ S) (hb : b ∉ S) : ∃ (γ' : Path a b), γ.Homotopic γ' ∧ Disjoint (Set.range ⇑γ') S

Base case: a path lying entirely inside one chart-ball (e, ball c r), with endpoints off a finite set S, is homotopic rel endpoints to a path whose range avoids S entirely.

Splitting a truncation at an intermediate time (design §7 step 0, risk R4)

γ|[c,e] ≃ γ|[c,d] ⬝ γ|[d,e] rel endpoints: the concatenation is the reparametrisation of γ.truncateOfLE : Path (γ.extend c) (γ.extend e) by the piecewise clock ρ u = if u ≤ 1/2 then min (2u) d else max (2u - 1) d, so Path.Homotopy.reparam applies.

The general (multi-chart) theorem

Downward induction along a ChartChain (design §7 steps 1–3). The invariant carried by exists_homotopic_avoiding_aux: given a "lead-in" path σ from a point q ∉ S to the chain breakpoint γ.extend (t k), lying entirely inside chart-ball k, the composite σ ⬝ γ|[t k, 1] is homotopic rel endpoints to an S-avoiding path. Each step splits off γ|[t k, t (k+1)] (via homotopic_truncateOfLE_trans), picks a fresh breakpoint q' ∉ S near γ.extend (t (k+1)) inside the image of the overlap of chart-balls k and k+1 (ℂ-minus-countable density through the chart, as in nonempty_open_diff_finite), connects it with an arc inside the overlap, perturbs the single-ball head via exists_homotopic_avoiding_of_ball, recurses on the tail, and glues with the groupoid-law homotopies (Path.Homotopic.trans_assoc/trans_symm/refl_trans).

theorem RS.exists_homotopic_avoiding {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {a b : X} (γ : Path a b) {S : Set X} (hS : S.Finite) (ha : a ∉ S) (hb : b ∉ S) : ∃ (γ' : Path a b), γ.Homotopic γ' ∧ Disjoint (Set.range ⇑γ') S

theorem RS.Loop.exists_homotopic_avoiding {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x₀ : X} (γ : Path x₀ x₀) {S : Set X} (hS : S.Finite) (hx₀ : x₀ ∉ S) : ∃ (γ' : Path x₀ x₀), γ.Homotopic γ' ∧ Disjoint (Set.range ⇑γ') S

Loop version (the blueprint's deliverable).