Extract the real contour balance
ProvedWeightedRootIntegralIdentity.weightedRootComplexToRealBalanceV3complex-analysisnormalizationresidue
Taking imaginary parts of the complex contour/residue balance yields the real normalization 2J=2π(S−P).
Formal statement
import Mathlib
theorem WeightedRootIntegralIdentity.weightedRootComplexToRealBalanceV3
(J S P : ℝ)
(hcomplex : (2 * (J : ℂ)) * Complex.I =
2 * Real.pi * Complex.I * ((S - P : ℝ) : ℂ)) :
2 * J = 2 * Real.pi * (S - P) := by sorry