sum_epsilon_abs_bound
plain-language theorem explainer
The theorem bounds the summed absolute phase perturbations from the regular analytic factor over 8(n+1) angular samples at refinement level n+1. Researchers controlling error terms in zeta-derived phase families within Recognition Science cite it when establishing summable linear-plus-quadratic perturbations. The proof applies the per-sample bound epsilon_abs_bound to obtain a uniform constant B, sums over the finite index set, and simplifies the resulting expression by field arithmetic.
Claim. Let $M$ be the logarithmic-derivative bound and $R$ the radius of a QuantitativeLocalFactorization. For each $n$, the sum of absolute sample increments of the regular factor phase at level $n+1$ satisfies $$sum_{j=0}^{8(n+1)-1} |ε_j| ≤ M R · 2π / (n+2),$$ where each $ε_j$ is the phase increment at angular spacing $2π/(8(n+1))$.
background
The MeromorphicCircleOrder module translates Mathlib meromorphic-order data into the Recognition Science annular-cost setting. A QuantitativeLocalFactorization extends LocalMeromorphicWitness by a uniform bound $M$ on $|g'/g|$ for the regular factor $g$ in the local factorization $f(z)=(z-ρ)^k g(z)$, together with a perturbation-regime condition $M R ≤ 1$. This supplies the analytic control on phase increments $ε_j$ sampled on circles around a zero or pole. The module records that for $ζ^{-1}$ the meromorphic order $-m$ produces phase charge $m$, matching the DefectSensor.charge convention. The immediate upstream lemma epsilon_abs_bound supplies the individual estimate $|ε_j| ≤ M · (R/(n+2)) · (2π/(8(n+1)))$.
proof idea
The proof defines an auxiliary real $B = M · (R/(n+2)) · (2π/(8(n+1)))$. It invokes epsilon_abs_bound via simpa to show every sample increment is at most $B$. The sum is then bounded by $8(n+1)·B$ using Finset.sum_le_sum. Algebraic reduction with positivity lemmas, field_simp and ring converts the product back to the target $M R 2π/(n+2)$.
why it matters
The result is used by genuineZetaDerivedPhasePerturbationWitness to certify that the perturbation terms of the genuine zeta-derived phase family remain small in the log-φ scale. It supplies the uniform summability needed for the linear and quadratic error controls inside RingPerturbationControl. In the broader framework it closes the analytic step that lets meromorphic order at a zero translate directly into the phase-charge input for defect-phase families, consistent with the eight-tick octave and J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.