RegularFactorPhase
plain-language theorem explainer
RegularFactorPhase packages a continuous phase function on a circle together with a positive Lipschitz constant and the requirement that the total winding charge is zero. Researchers constructing shared circle families or quantitative local factorizations cite it when isolating holomorphic nonvanishing factors from meromorphic ones in the annular cost model. The declaration is introduced directly as a structure extending ContinuousPhaseData; the zero-charge field follows from the argument principle while the Lipschitz field records a bound on |
Claim. A structure extending ContinuousPhaseData (center $c$, radius $R>0$, continuous phase function $Θ:ℝ→ℝ$, integer charge $m$ satisfying $Θ(2π)-Θ(0)=-2π m$) by a positive real $M>0$ such that $|Θ(θ₂)-Θ(θ₁)|≤M|θ₂-θ₁|$ for all real $θ₁,θ₂$, together with the requirement that charge $m=0$.
background
The Circle Phase Lift module supplies continuous phase data that converts the argument of a nonvanishing function on a circle into a real-valued function Θ whose net change over one period encodes the winding number. ContinuousPhaseData records the circle parameters, the continuous lift Θ, and the integer charge together with the exact winding equality. RegularFactorPhase specializes this data for holomorphic nonvanishing functions inside the disk, where the argument principle forces charge zero and the supremum of |g'/g| on the circle supplies the Lipschitz constant M via the chain rule.
proof idea
The declaration is a structure definition that extends ContinuousPhaseData by adjoining the four fields logDerivBound, logDerivBound_pos, the universal Lipschitz inequality on phase, and charge_zero. No lemmas are invoked; the fields are simply declared with their types and the zero-charge condition is asserted directly.
why it matters
RegularFactorPhase supplies the zero-charge phase type consumed by mkSharedCirclePair when building carrier families that separate regular factors from defects, and by genuineRegularFactorPhaseAt together with qlf_regularFactorPhase when extracting phase data from a QuantitativeLocalFactorization. It therefore closes the regular-factor half of the circle-phase infrastructure needed to sample AnnularRingSample costs while respecting the eight-tick phase periodicity and the holomorphic nonvanishing zero-charge result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.