QuantitativeLocalFactorization
plain-language theorem explainer
QuantitativeLocalFactorization augments a LocalMeromorphicWitness with a positive real bound M on the logarithmic derivative of the regular factor, together with the regime condition that M times radius is at most 1. Researchers applying annular cost comparisons to hypothetical zeros of zeta cite it to guarantee that phase perturbations remain small enough for the phiCost bounds to apply. The declaration is a structure extension that directly encodes the uniform analytic control needed for sampled increments on circles.
Claim. A quantitative local factorization consists of a center $w$, integer order $n$, positive radius $r$, and analytic regular factor $g$ nonvanishing on the closed disk of radius $r$ around $w$, equipped with a positive real $M$ such that $M r ≤ 1$ and $M$ bounds $|g'/g|$ uniformly on that disk.
background
LocalMeromorphicWitness supplies the base data for a local factorization of a meromorphic function: center, integer order, positive radius, and regular factor that is analytic and nowhere zero inside the closed ball. The module on Meromorphic Circle Order uses this to connect Mathlib meromorphic-order results to the Recognition Science annular-cost setting, where the pole part contributes a pure winding charge while the regular factor contributes a controlled perturbation.
proof idea
The declaration is a structure extension of LocalMeromorphicWitness. It adds the three fields logDerivBound (the real M), its positivity proof, and the inequality logDerivBound * radius ≤ 1. No lemmas or tactics are applied; the structure simply packages the uniform bound on the logarithmic derivative of the regular factor.
why it matters
It supplies the analytic input required by mkSharedCirclePair and the carrier-defect comparison theorems that appear in CarrierBudgetComparison. Those results in turn support the honest phase-budget bridges and the (deprecated) rh_from_single_axiom. Within the Recognition framework the structure closes the gap between meromorphic order and the perturbation control needed to separate defect annular costs from carrier budgets on shared circles, directly feeding the argument-principle application to zeta inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.