local_meromorphic_factorization
plain-language theorem explainer
The theorem extracts from Mathlib's meromorphicOrderAt_eq_int_iff a concrete local factorization of a meromorphic f at ρ into (z-ρ)^n times an analytic nonvanishing regular factor g, packaged inside the LocalMeromorphicWitness structure. Number theorists applying Recognition Science to the Riemann hypothesis cite it when building phase-charge witnesses around zeros of zeta. The proof obtains the analytic factor g together with two balls, halves the minimum radius to guarantee the closed-disk conditions, and assembles the witness record.
Claim. Let $f:ℂ→ℂ$ be meromorphic at $ρ∈ℂ$ with integer order $n$. Then there exists a witness $w$ such that $w.center=ρ$, $w.order=n$, $w.radius>0$, the regular factor $g$ of $w$ is analytic at $ρ$, differentiable on the closed disk of radius $w.radius$ centered at $ρ$, and nowhere zero on that closed disk.
background
LocalMeromorphicWitness is the structure that records a center $ρ$, integer order $n$, positive radius, and the regular factor $g$ together with the three analyticity and nonvanishing certificates needed for annular cost calculations. The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the RS annular-cost framework by converting the Weierstrass factorization $f(z)=(z-ρ)^n g(z)$ into phase-charge statements: the pole part contributes charge $-n$ while the regular factor contributes charge 0. Upstream, meromorphicOrderAt_eq_int_iff supplies the existence of $g$ analytic and nonvanishing at $ρ$; the module then uses this witness to feed DefectPhasePerturbationWitness and zetaReciprocal_local_factorization.
proof idea
Apply meromorphicOrderAt_eq_int_iff to obtain the analytic nonvanishing $g$. Extract a ball on which $g$ is analytic and a second ball on which $g$ is nonzero. Take half the minimum of the two radii. Construct the witness record with this radius, set regularFactor to $g$, and discharge the differentiability and nonvanishing obligations by restricting the ball inclusions and applying linarith.
why it matters
The declaration supplies the local factorization required by zetaReciprocal_local_factorization and by genuineZetaDerivedPhasePerturbationWitness. It therefore closes the step that converts meromorphic order $-m$ of $ζ^{-1}$ at a zero of multiplicity $m$ into the phase charge $m$ demanded by DefectSensor. In the Recognition framework this supplies the concrete analytic input for the perturbation bounds that keep phiCost increments summable on rings around hypothetical zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.