ContinuousPhaseData
plain-language theorem explainer
ContinuousPhaseData packages a continuous real-valued argument function on a circle together with its integer winding number. Researchers converting holomorphic data to discrete annular samples cite this structure when bridging complex analysis to the cost framework. The declaration is a structure definition whose seven fields directly encode center, radius, continuity, charge, and the winding equality.
Claim. A structure consisting of center $c ∈ ℂ$, radius $R > 0$, continuous phase function $Θ : ℝ → ℝ$, integer charge $m$, satisfying $Θ(2π) − Θ(0) = −2π m$.
background
The Circle Phase Lift module supplies continuous-phase infrastructure bridging Mathlib complex analysis to the discrete AnnularRingSample / AnnularMesh cost framework. Given a nonvanishing function on a circle, the phase is a continuous real function Θ : [0, 2π] → ℝ whose total change Θ(2π) − Θ(0) = −2π·m encodes the winding number m. Sampling Θ at 8n equispaced angles produces phase increments whose telescoping sum satisfies the winding_constraint of AnnularRingSample. The module imports AnnularCost and relies on circleMap, circleIntegral_eq_zero_of_differentiable_on_off_countable, and IsCoveringMap.liftPath from Mathlib.
proof idea
This declaration is a structure definition that directly assembles the seven fields center, radius with positivity proof, continuous phase, integer charge, and the winding equality phase_winding.
why it matters
ContinuousPhaseData is the base type extended by RegularFactorPhase and used in charge_additive, holomorphic_nonvanishing_zero_charge, logDeriv_circle_integral_zero, and zpow_phase_charge. It supplies the continuous phase lift that connects analytic nonvanishing functions (via the argument principle) to the discrete sampling framework, consistent with the eight-tick octave in the forcing chain. Downstream results quote the winding relation to obtain zero charge for holomorphic nonvanishing maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.