Green's theorem for finite integer-weighted AC families

The field is localized using every trace and the support of the total winding weight. Only the total index must vanish outside the domain: individual indices may cancel. Simultaneous polygonal approximation preserves the total index outside the domain. The actual polygonal identities pass to the family through boundary and total-weight L¹ convergence.

theorem TauCeti.Green.green_ac_winding_sum {ι : Type u_1} {s : Finset ι} {γ : ι → ℝ → ℂ} {a b : ι → ℝ} {w : ι → ℤ} {U : Set ℂ} {P Q : ℂ → ℝ} (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) (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) (hindex : ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * Contour.windingNumber (γ i) (a i) (b i) z = 0) : (∀ i ∈ s, IntervalIntegrable (circulationFun P Q (γ i)) MeasureTheory.volume (a i) (b i)) ∧ MeasureTheory.IntegrableOn (fun (z : ℂ) => (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P Q z) U MeasureTheory.volume ∧ ∑ i ∈ s, ↑(w i) * ∫ (t : ℝ) in a i..b i, circulationFun P Q (γ i) t = ∫ (z : ℂ) in U, (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P Q z

Green's theorem for a finite integer-weighted family of closed AC curves. The domain condition concerns the total index, permitting cancellation between curves.