genuineRegularFactorPhaseAt_logDerivBound
plain-language theorem explainer
The theorem states that the logarithmic derivative bound on the genuine regular factor phase extracted at level n from a quantitative local factorization equals the factorization's own bound scaled by its radius divided by n plus one. Researchers controlling phase perturbations in meromorphic expansions for the Recognition Science annular cost framework would invoke this identity to scale Lipschitz constants across refinement levels. The proof reduces immediately to the definition of the phase extraction via reflexivity.
Claim. Let $Q$ be a quantitative local factorization of a meromorphic function. For each natural number $n>0$, the logarithmic derivative bound of the genuine regular factor phase at level $n$ satisfies $M_n = M_Q · (R_Q / (n+1))$, where $M_Q$ is the uniform bound on $|g'/g|$ supplied by $Q$ and $R_Q$ is the radius of the disk in $Q$.
background
QuantitativeLocalFactorization extends LocalMeromorphicWitness by adding a real number logDerivBound together with positivity and a perturbation-regime hypothesis that keeps the product of the bound and radius at most 1. This structure supplies the uniform control on the logarithmic derivative of the regular factor g in the local factorization f(z) = (z-ρ)^n g(z). The definition genuineRegularFactorPhaseAt extracts from this input a RegularFactorPhase object whose logDerivBound field is set to the scaled quantity appearing on the right-hand side. The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the RS annular-cost framework, using phase-charge additivity on circles around zeros of ζ^{-1}.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of genuineRegularFactorPhaseAt. That definition constructs the phase object by scaling the input logDerivBound by radius over (n+1) and placing the result directly into the logDerivBound field of the returned RegularFactorPhase structure.
why it matters
This identity supplies the precise scaling that converts the analytic input logDerivBound of QuantitativeLocalFactorization into the Lipschitz constant required at each refinement level n for the phase-perturbation witnesses. It therefore enables the discharge of the linear-plus-quadratic error bounds needed by canonicalDefectSampledFamily_ringPerturbationControl. In the Recognition Science setting the result keeps regular-factor contributions inside the log-phi scale on sampled circles, consistent with the annular-cost framework and the local factorization of ζ^{-1} at its zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.