holomorphic_circle_integral_zero
plain-language theorem explainer
The theorem states that the contour integral of a complex function over a circle vanishes when the function is continuous on the closed disk and differentiable at every interior point. Researchers building phase-lift arguments in Recognition Science cite it to confirm zero winding for holomorphic functions before sampling discrete phase increments. The proof is a one-line wrapper that applies the Mathlib lemma circleIntegral_eq_zero_of_differentiable_on_off_countable with the exceptional set taken to be empty.
Claim. If $f : ℂ → ℂ$ is continuous on the closed disk of radius $R$ centered at $c$ and differentiable at every point inside the open disk, then the contour integral ∮_{C(c,R)} f(z) dz = 0.
background
The Circle Phase Lift module supplies continuous-phase infrastructure that links Mathlib complex analysis to the discrete AnnularRingSample and AnnularMesh cost framework. Supporting definitions include ContinuousPhaseData, which encodes a continuous real phase function Θ on [0, 2π] whose net change encodes winding number, and RegularFactorPhase, which guarantees Lipschitz phase factors compatible with annular cost sampling. This theorem supplies the required Cauchy–Goursat statement for holomorphic functions on disks, enabling the zero-charge results that feed the winding_constraint of AnnularRingSample.
proof idea
The proof is a one-line wrapper that invokes circleIntegral_eq_zero_of_differentiable_on_off_countable, passing the radius non-negativity hypothesis, the empty exceptional set (which is countable), the continuity hypothesis on the closed ball, and a lambda that extracts interior differentiability from ball membership.
why it matters
This result is the base case invoked by logDeriv_circle_integral_zero, which in turn supports holomorphic_nonvanishing_zero_charge, zpow_phase_charge, and charge_additive inside the same module. It supplies the analytic prerequisite for zero winding in the phase-lift construction, directly enabling discrete sampling of phase increments that satisfy annular cost constraints. In the Recognition framework it anchors the continuous-to-discrete bridge at the level of T5 J-uniqueness and the eight-tick octave, ensuring holomorphic phases contribute no net charge to the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.