epsilon_abs_bound
plain-language theorem explainer
The theorem bounds the absolute value of each sampled phase perturbation increment ε_j at level n by M R 2π over 8n(n+1) for a quantitative local factorization. Analysts controlling summable linear and quadratic errors in annular phi-cost under ring perturbation cite the result. The argument is a direct one-line application of the increment_bound property attached to the genuine regular factor phase family.
Claim. Let M and R be the logarithmic derivative bound and radius of a quantitative local factorization. For positive integer n and index j in Fin(8n), the sampled phase increment satisfies |ε_j| ≤ M · (R/(n+1)) · (2π/(8n)).
background
QuantitativeLocalFactorization extends a local meromorphic witness with a positive bound M on |g'/g| for the regular factor g and the regime condition M R ≤ 1. This controls the size of the phase perturbation ε_j contributed by g on circles centered at the pole. The module translates Mathlib meromorphic order results into the Recognition Science setting. A function with meromorphic order n at ρ factors locally as (z-ρ)^n g(z) with g holomorphic and nonzero at ρ. The phase charge of the pole term is -n while the regular factor contributes zero charge, so the total matches the defect charge for the inverse zeta function at its zeros. Upstream lemmas from the eight-tick foundation supply the discrete sampling at angles kπ/4 and the genuine regular factor phase family that isolates the pure winding increment from the ε perturbation.
proof idea
The proof is a one-line wrapper that applies the increment_bound lemma from the genuineRegularFactorPhaseAt construction. That lemma converts the log-derivative bound M into an arc-length estimate on the circle of radius R/(n+1) with angular step 2π/(8n).
why it matters
The bound is invoked by the epsilon_log_phi_small theorem to obtain |log φ · ε| ≤ 1 and by the sum_epsilon_abs_bound and sum_epsilon_sq_bound results that establish uniform summability of the perturbation errors. It therefore supplies the missing analytic estimate for the ring perturbation control lemma in the meromorphic circle order module. The construction relies on the eight-tick octave for its sampling density and advances the Recognition Science derivation of the Riemann hypothesis via controlled phi-cost perturbations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.