QuantitativeLocalFactorization
plain-language theorem explainer
Quantitative local factorization augments the local meromorphic witness with a positive bound M on the logarithmic derivative of the regular factor together with the regime condition M times radius at most 1. Researchers applying annular cost comparisons to hypothetical zeros of zeta cite this structure to control phase perturbations on sampled circles. The declaration is a structure extension that adjoins three fields to the base witness.
Claim. A quantitative local factorization consists of a local meromorphic witness (center $w$, integer order $n$, radius $r>0$, regular factor $g$ analytic at $w$ and non-vanishing on the closed disk of radius $r$) equipped with $M>0$ such that $M r ≤ 1$, where $M$ bounds $|g'/g|$ uniformly on that disk.
background
The referenced LocalMeromorphicWitness structure supplies center, order, radius, and regular factor $g$ that is analytic at the center, differentiable on the closed ball, and nowhere zero inside it. Module context bridges Mathlib meromorphic order at a point to the Recognition Science annular cost framework: a meromorphic $f$ factors as $(z-ρ)^n g(z)$ with $g$ holomorphic and non-vanishing, so the phase charge of $ζ^{-1}$ at a zero of multiplicity $m$ equals $m$. Upstream structures supply J-cost calibration and eight-tick phases used in the surrounding perturbation lemmas.
proof idea
This is a structure definition that directly extends LocalMeromorphicWitness by adjoining the three fields logDerivBound, its positivity, and the perturbation regime inequality.
why it matters
The structure supplies the analytic input required by mkSharedCirclePair and the carrier_defect_comparison_rh theorem in CarrierBudgetComparison; those results compare defect and carrier annular costs on shared circles to obtain cost divergence for nonzero charge. It thereby closes the quantitative control step for the honest phase budget bridge applied to $ζ^{-1}$. The definition touches the open question of whether the log-derivative bound can be made uniform across all hypothetical zeros inside the critical strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.