Simultaneous polygonal approximation of finite curve families

Finite families of closed AC curves admit endpoint-preserving polygonal approximations with uniform and derivative L¹ convergence on each curve's own parameter interval. The total integer-weighted winding weight converges in L¹. All traces eventually remain in a common open field domain and the total index still vanishes outside it, even when individual indices cancel in holes.

theorem TauCeti.Green.exists_polygonal_approximation_winding_sum {ι : Type u_1} {s : Finset ι} {γ : ι → ℝ → ℂ} {a b : ι → ℝ} {w : ι → ℤ} {U : Set ℂ} (hab : ∀ i ∈ s, a i < b i) (hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i)) (hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i)) (hU : IsOpen U) (htrace : ∀ i ∈ s, γ i '' Set.uIcc (a i) (b i) ⊆ U) (hindex : ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * Contour.windingNumber (γ i) (a i) (b i) z = 0) : ∃ (γn : ℕ → ι → ℝ → ℂ), (∀ (n : ℕ), ∀ i ∈ s, IsPolygonalOnInterval (γn n i) (a i) (b i) ∧ AbsolutelyContinuousOnInterval (γn n i) (a i) (b i) ∧ γn n i (a i) = γ i (a i) ∧ γn n i (b i) = γ i (b i) ∧ γn n i (a i) = γn n i (b i)) ∧ (∀ i ∈ s, TendstoUniformlyOn (fun (n : ℕ) => γn n i) (γ i) Filter.atTop (Set.Icc (a i) (b i))) ∧ (∀ i ∈ s, Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a i..b i, ‖deriv (γn n i) t - deriv (γ i) t‖) Filter.atTop (nhds 0)) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |∑ i ∈ s, ↑(w i) * windingWeight (γn n i) (a i) (b i) z - ∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z|) Filter.atTop (nhds 0) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (∀ i ∈ s, γn n i '' Set.uIcc (a i) (b i) ⊆ U) ∧ ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * Contour.windingNumber (γn n i) (a i) (b i) z = 0

Closed AC curves admit simultaneous polygonal approximations preserving their own endpoints, all three analytic convergences, and total-index vanishing outside a common field domain. Individual indices may be nonzero outside that domain.