LocalMeromorphicWitness
plain-language theorem explainer
LocalMeromorphicWitness packages the center, integer order, positive radius, and analytic non-vanishing regular factor of a local Weierstrass factorization around a point in the complex plane. Number theorists extracting phase charges from meromorphic orders of zetaReciprocal cite the structure to feed EulerInstantiation and RingPerturbationControl. The definition is assembled directly from Mathlib's meromorphicOrderAt_eq_int_iff plus an explicit closed-ball analyticity witness.
Claim. A local meromorphic witness at a point consists of a center $ρ ∈ ℂ$, an integer order $n$, a radius $r > 0$, and a function $g:ℂ→ℂ$ such that $g$ is analytic at $ρ$, differentiable on the closed disk of radius $r$ centered at $ρ$, and $g(z) ≠ 0$ for all $z$ in that disk.
background
The module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. A meromorphic function $f$ with meromorphicOrderAt $f$ $ρ$ = $n$ admits the factorization $f(z) = (z-ρ)^n g(z)$ where $g$ is analytic and $g(ρ) ≠ 0$. The witness records exactly this data on a closed disk so that phase charge of the pole term is $-n$ while the regular factor contributes zero charge.
proof idea
The structure is a plain record definition. The shrinkRadius operation reuses the same regularFactor, copies analyticity, and restricts differentiability and non-vanishing by monotonicity of closed balls together with le_trans on the radius comparison.
why it matters
The witness supplies the concrete factorization data consumed by zetaReciprocal_local_factorization, eulerQuantitativeFactorization_center, eulerQuantitativeFactorization_order, and meromorphic_phase_charge. It thereby links Mathlib's meromorphicOrderAt_eq_int_iff to the phase-charge calculation that matches DefectSensor.charge for ζ^{-1} at a zero of multiplicity m, closing the local input required for canonicalDefectSampledFamily_ringPerturbationControl.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.