sum_inv_succ_mul_succ_sq_le_one
plain-language theorem explainer
The inequality shows that the sum over the first N terms of 1/((n+1)(n+2)^2) never exceeds 1. Researchers working on phase perturbation bounds in meromorphic families cite it to control quadratic error accumulation. The proof reduces the squared-denominator sum to its linear counterpart by termwise comparison and applies the known telescoping result.
Claim. For every natural number $N$, $$sum_{n=0}^{N-1} 1/((n+1)(n+2)^2) leq 1.$$
background
The MeromorphicCircleOrder module adapts Mathlib meromorphic-order tools to the Recognition Science annular-cost setting. A function with meromorphic order n at rho factors as (z-rho)^n g(z) with g holomorphic and nonzero at rho; the phase charge contributed by the pole factor is then -n. The present bound supplies a uniform majorant for summed quadratic increments that appear when regular factors g are sampled on circles around rho.
proof idea
A calc first replaces each term 1/((n+1)(n+2)^2) by the strictly larger 1/((n+1)(n+2)) via field_simp and nlinarith on the positive denominators. The resulting sum is then bounded by 1 by direct appeal to the upstream telescoping lemma sum_inv_succ_mul_succ_le_one.
why it matters
The bound closes the quadratic-term estimate inside genuineZetaDerivedPhasePerturbationWitness and is invoked by mkSharedCirclePair_carrier_excess_bounded to show that regular-phase contributions remain controlled under the phi-cost metric. It thereby supplies the analytic input required for canonical defect sampling on rings around zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.