Scaling invariance for contour winding numbers

This file records the basic nonzero-scaling API for the generalized winding number. Multiplying both the curve and the distinguished point by the same nonzero complex number leaves the index principal value unchanged, so the winding number and null-homology are invariant. Scaling only reindexes the excision radius by the order-isomorphism ε ↦ ε / ‖c‖, so no principal-value existence hypothesis is needed.

These lemmas are bookkeeping for the roadmap's curve and cycle layer. The geometry of the generalized winding number is local at a crossing or sector; after translating the crossing point to the origin, finite-decomposition arguments also rescale the local model before applying the sector computation.

Main results

• Contour.hasCauchyPVAt_inv_sub_const_mul / Contour.cauchyPVExistsAt_inv_sub_const_mul — the index principal value transports under nonzero scaling of the curve and base point; these are exposed so downstream normalization steps can obtain the scaled HasCauchyPVAt / CauchyPVExistsAt fact and chain further principal-value APIs.
• Contour.windingNumber_const_mul — multiplying the curve and base point by the same nonzero complex number preserves the generalized winding number.
• Contour.IsNullHomologous.const_mul — null-homology is preserved by nonzero complex scaling of both the curve and the ambient set.

Provenance

This is routine API around the Hungerbühler--Wasem generalized winding number from the contour integration roadmap; no formal source is vendored.

theorem TauCeti.Contour.hasCauchyPVAt_inv_sub_const_mul {γ : ℝ → ℂ} {a b : ℝ} {z₀ c L : ℂ} (h : HasCauchyPVAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀ L) (hc : c ≠ 0) : HasCauchyPVAt (fun (t : ℝ) => c * γ t) a b (fun (w : ℂ) => (w - c * z₀)⁻¹) (c * z₀) L

Index principal value under nonzero scaling. Multiplying the curve and the base point by a nonzero complex number c transports the single-point Cauchy principal value of the winding kernel κ[z₀] about z₀ to that of κ[c * z₀] about c * z₀, with the same value. This specializes the general HasCauchyPVAt.const_mul_curve to the winding kernel, where the rescaled integrand z ↦ c⁻¹ * κ[z₀] (c⁻¹ * z) agrees with κ[c * z₀] along the scaled curve. Exposed so downstream normalization steps can chain further principal-value APIs from the scaled fact.

theorem TauCeti.Contour.cauchyPVExistsAt_inv_sub_const_mul {γ : ℝ → ℂ} {a b : ℝ} {z₀ c : ℂ} (h : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) (hc : c ≠ 0) : CauchyPVExistsAt (fun (t : ℝ) => c * γ t) a b (fun (w : ℂ) => (w - c * z₀)⁻¹) (c * z₀)

Existence form of hasCauchyPVAt_inv_sub_const_mul: nonzero scaling of the curve and base point preserves existence of the index principal value, exposed for the same downstream chaining.

theorem TauCeti.Contour.windingNumber_const_mul {γ : ℝ → ℂ} {a b : ℝ} {z₀ c : ℂ} (hc : c ≠ 0) : windingNumber (fun (t : ℝ) => c * γ t) a b (c * z₀) = windingNumber γ a b z₀

The generalized winding number is invariant under simultaneous multiplication of the curve and the base point by a nonzero complex number.

theorem TauCeti.Contour.IsNullHomologous.const_mul {γ : ℝ → ℂ} {a b : ℝ} {c : ℂ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (hc : c ≠ 0) : IsNullHomologous (fun (t : ℝ) => c * γ t) a b ((fun (z : ℂ) => c * z) '' Ω)

Null-homology is preserved by nonzero complex scaling of both the curve and the ambient set.