LocalMeromorphicWitness
A data structure that records a center in the complex plane, an integer order, a positive radius, and a nonvanishing analytic regular factor on the closed disk of that radius. Researchers extracting phase data from the Riemann zeta reciprocal or Euler factorizations cite it to convert meromorphic orders into concrete local witnesses. The definition is a direct record with field proofs for analyticity and nonvanishing; the shrinkRadius helper follows from monotonicity of closed-ball membership under radius restriction.
claimA local meromorphic witness at a point $ρ ∈ ℂ$ of order $n ∈ ℤ$ consists of a radius $r > 0$ and a function $g : ℂ → ℂ$ that is analytic at $ρ$, differentiable on the closed disk of radius $r$ centered at $ρ$, and satisfies $g(z) ≠ 0$ for all $|z − ρ| ≤ r$.
background
The module bridges Mathlib meromorphic-order machinery to the Recognition Science annular cost framework. A meromorphic function $f$ with meromorphicOrderAt $f$ $ρ$ = $n$ admits the local factorization $f(z) = (z − ρ)^n · g(z)$ where $g$ is analytic at $ρ$ and $g(ρ) ≠ 0$, by Mathlib's meromorphicOrderAt_eq_int_iff. On a small circle around $ρ$, the factor $(z − ρ)^n$ carries phase charge −$n$, the regular factor $g$ carries charge 0, and the product carries charge −$n$. For the RS/RH application, the reciprocal zeta function has order −$m$ at a zero of multiplicity $m$, so its phase charge equals $m$, matching DefectSensor.charge.
proof idea
This is a structure definition that directly assembles the center, order, radius, and regular factor with the required analyticity, differentiability on the closed ball, and non-vanishing properties. The shrinkRadius method is a one-line wrapper that reuses the original regularFactor while restricting the ball via Metric.mem_closedBall.mpr and le_trans on the radii.
why it matters in Recognition Science
The structure supplies the basic data type for local factorizations appearing in zetaReciprocal_local_factorization and eulerQuantitativeFactorization_center, which feed eulerQuantitativeFactorization_order and meromorphic_phase_charge. It provides the analytic regular factor needed for phase-charge extraction and for the perturbation lemmas that control ε_j increments on sampled rings in the annular cost model. It touches the open question of uniform summability of linear-plus-quadratic errors across refinement depth N.
scope and limits
- Does not supply a global factorization over the whole plane.
- Does not include bounds on the logarithmic derivative of the regular factor.
- Does not presuppose that the center is a zero of zeta.
- Does not address behavior outside the given disk.
formal statement (Lean)
51structure LocalMeromorphicWitness where
52 center : ℂ
53 order : ℤ
54 radius : ℝ
55 radius_pos : 0 < radius
56 regularFactor : ℂ → ℂ
57 regularFactor_analytic : AnalyticAt ℂ regularFactor center
58 regularFactor_diff : DifferentiableOn ℂ regularFactor (Metric.closedBall center radius)
59 regularFactor_nz : ∀ z ∈ Metric.closedBall center radius, regularFactor z ≠ 0
60
61/-- Restrict a local meromorphic witness to any smaller positive radius. -/
62def LocalMeromorphicWitness.shrinkRadius
63 (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r ≤ w.radius) :
64 LocalMeromorphicWitness where
65 center := w.center
proof body
Definition body.
66 order := w.order
67 radius := r
68 radius_pos := hr
69 regularFactor := w.regularFactor
70 regularFactor_analytic := w.regularFactor_analytic
71 regularFactor_diff := by
72 refine w.regularFactor_diff.mono ?_
73 intro z hz
74 exact Metric.mem_closedBall.mpr <|
75 le_trans (Metric.mem_closedBall.mp hz) hrw
76 regularFactor_nz := by
77 intro z hz
78 exact w.regularFactor_nz z <| Metric.mem_closedBall.mpr <|
79 le_trans (Metric.mem_closedBall.mp hz) hrw
80
81/-- Extract a genuine local meromorphic factorization from Mathlib's
82`meromorphicOrderAt_eq_int_iff`. The regular factor `g` is the actual
83analytic nonvanishing part from the Weierstrass factorization, not a
84dummy constant. -/