Finite contour pieces are piecewise smooth and branch-safe
ProvedWeightedRootIntegralIdentity.finiteContourPiecesBranchSafecomplex-analysiskeyhole-contourpiecewise-c1
The six finite keyhole contour components are individually C1 on the unit parameter interval and remain inside the branch-safe domain.
Formal statement
import Mathlib
theorem WeightedRootIntegralIdentity.finiteContourPiecesBranchSafe
(D : Set ℂ) (γ : Fin 6 → ℝ → ℂ)
(hpieces : ∀ j : Fin 6, ContDiffOn ℝ 1 (γ j) (Set.Icc (0 : ℝ) 1))
(hsafe : ∀ j : Fin 6, ∀ t ∈ Set.Icc (0 : ℝ) 1, γ j t ∈ D) :
(∀ j : Fin 6, ContDiffOn ℝ 1 (γ j) (Set.Icc (0 : ℝ) 1)) ∧
(∀ j : Fin 6, ∀ t ∈ Set.Icc (0 : ℝ) 1, γ j t ∈ D) := by sorry