ContinuousPhaseData
plain-language theorem explainer
ContinuousPhaseData packages a center, positive radius, continuous real phase function, and integer charge on a circle such that the total phase change equals minus 2 pi times charge. Complex analysts sampling holomorphic phases for annular cost models cite the structure when lifting continuous arguments to discrete 8n-point increments. It is introduced directly as a structure whose fields encode the winding condition and continuity requirement.
Claim. A structure consisting of a center $c \in \mathbb{C}$, radius $R > 0$, a continuous function $\Theta : \mathbb{R} \to \mathbb{R}$, and integer charge $m \in \mathbb{Z}$ satisfying $\Theta(2\pi) - \Theta(0) = -2\pi m$.
background
The CirclePhaseLift module supplies continuous-phase infrastructure that converts Mathlib complex analysis into the discrete AnnularRingSample framework. A nonvanishing function on a circle yields a continuous real argument $\Theta$ on $[0, 2\pi]$ whose net change encodes the winding number; sampling at 8n equispaced points produces increments whose sum recovers the winding constraint.
ContinuousPhaseData is the base structure extended by RegularFactorPhase, which adds a log-derivative Lipschitz bound and forces charge zero. Upstream results include the eight-tick phase definition (periodic with period $2\pi$) and the AnnularCost import that supplies the target sample type.
proof idea
Structure definition; fields are declared directly with the phase_winding field stating the total change condition and phase_continuous asserting continuity on the real line.
why it matters
ContinuousPhaseData is the common carrier for phase data that feeds charge_additive, holomorphic_nonvanishing_zero_charge, and the conversion to AnnularRingSample. It supplies the continuous lift required by the eight-tick octave sampling (T7) and the annular cost calculations that connect to the Recognition Composition Law. The definition closes the interface between analytic winding numbers and the discrete phi-ladder cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.