meromorphic_phase_charge
plain-language theorem explainer
The theorem states that any LocalMeromorphicWitness encoding a local Weierstrass factorization with integer order n at center ρ yields a ContinuousPhaseData on every smaller circle whose charge equals -n. Researchers building defect phase families from zeta zeros for the Recognition Science Riemann hypothesis argument cite this result to lift meromorphic orders to winding charges. The proof is a one-line wrapper that invokes the explicit zpow_phase_charge construction on the monomial factor.
Claim. Let $w$ be a local meromorphic witness with center $ρ$, order $n$, and radius $R>0$. For any real $r$ with $0<r<R$, there exists a continuous phase datum on the circle of radius $r$ centered at $ρ$ whose charge equals $-n$, i.e., the total phase change over one full traversal satisfies $Θ(2π)-Θ(0)=-2π n$.
background
A LocalMeromorphicWitness packages a center $ρ$, integer order $n$, radius $R$, and a regular analytic factor $g$ that is nonvanishing on the closed ball of radius $R$. This encodes the local factorization $f(z)=(z-ρ)^n g(z)$ supplied by Mathlib's meromorphicOrderAt_eq_int_iff. ContinuousPhaseData records a continuous argument function $Θ:ℝ→ℝ$ on the circle together with its integer charge, defined so that $Θ(2π)-Θ(0)=-2π·$charge.
proof idea
The proof is a one-line wrapper that applies zpow_phase_charge to the center, radius, and order of the witness. The regular factor contributes zero charge by the nonvanishing holomorphic property already recorded in the witness structure, so the total charge is carried exactly by the monomial factor.
why it matters
This supplies the phase charge for every local meromorphic witness and is invoked by zetaDerivedPhaseData_charge to equip defect phase families derived from zeta zeros with the correct charge. It also supports phaseIncrementEpsilonBound_decreasing when controlling perturbations on successive rings. In the framework it realizes the local step of the argument principle for $ζ^{-1}$, where the order at a zero of $ζ$ produces positive charge matching the defect sensor, consistent with the eight-tick phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.