logDeriv_circle_integral_zero
plain-language theorem explainer
Researchers in Recognition Science cite this result to confirm zero phase charge for holomorphic nonvanishing functions on enclosing circles. The statement asserts that the contour integral of the logarithmic derivative f'/f over the circle vanishes when f is differentiable and nonvanishing on the closed disk and f'/f is continuous there. The proof invokes the general holomorphic contour integral zero theorem after a local argument establishes differentiability of the quotient at interior points via the quotient rule.
Claim. Let $f:ℂ→ℂ$ be differentiable on the closed disk of radius $R>0$ centered at $c$, with $f(z)≠0$ everywhere in the disk, and suppose $f'/f$ is continuous on the closed disk. Then the contour integral $∮_{|z-c|=R} (f'/f)(z) dz = 0$.
background
The Circle Phase Lift module supplies continuous phase assignments Θ for nonvanishing functions on circles, bridging Mathlib complex analysis to the AnnularRingSample cost framework. ContinuousPhaseData is the structure packaging a continuous real phase function whose net change Θ(2π)−Θ(0) equals −2π times the integer charge (winding number). The upstream holomorphic_circle_integral_zero states: if f is holomorphic on the closed disk (possibly off a countable set), the contour integral of f vanishes, citing circleIntegral_eq_zero_of_differentiable_on_off_countable.
proof idea
This is a tactic proof that applies holomorphic_circle_integral_zero after supplying a local proof that the log-derivative is differentiable inside the ball. The local argument first obtains DifferentiableAt for f and for deriv f at each interior point, then uses the quotient rule to conclude differentiability of (deriv f)/f.
why it matters
This result supplies the contour-integral form of zero winding for holomorphic nonvanishing functions, directly supporting holomorphic_nonvanishing_zero_charge and the charge definitions in the phase lift. It connects to the eight-tick Phase space and winding abstraction in Ribbons, confirming absence of net phase accumulation consistent with the Recognition framework's zero-charge requirement for analytic nonvanishing fields. The doc-comment notes the explicit link charge = −(2πi)⁻¹ ∮ f'/f dz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.