sum_inv_succ_mul_succ_le_one
plain-language theorem explainer
The inequality asserts that for any natural number N the sum from n=0 to N-1 of 1/((n+1)(n+2)) is at most 1. Analysts controlling error terms in meromorphic expansions or zeta-function phase perturbations cite this bound when summing increments over annular rings. The proof decomposes each summand via partial fractions into a telescoping difference, rewrites the Fin sum as a range sum, and closes with the closed form 1 minus a positive remainder.
Claim. For every natural number $N$, $$∑_{n=0}^{N-1} 1/((n+1)(n+2)) ≤ 1.$$
background
This result sits inside the MeromorphicCircleOrder module, which translates Mathlib meromorphic-order data into the Recognition Science annular-cost setting. The module shows that a meromorphic function with order n at ρ factors locally as (z−ρ)^n g(z) with g holomorphic and non-vanishing, so that the phase charge of ζ^{-1} at a zero of multiplicity m equals m and matches the DefectSensor.charge convention. The present bound supplies the uniform majorant needed for the linear-plus-quadratic error sums that appear in the perturbation witnesses for the genuine zeta-derived phase family.
proof idea
The argument first proves the partial-fraction identity 1/((k+1)(k+2)) = 1/(k+1) − 1/(k+2) by field_simp and ring. It rewrites the Fin-indexed sum as a Finset.range sum via Fin.sum_univ_eq_sum_range, applies the identity termwise with sum_congr, distributes the subtraction with sum_sub_distrib, and identifies the result as the telescoping difference 1 − 1/(N+1) via sum_range_sub' together with add_assoc. The final step invokes positivity of the remainder and linarith.
why it matters
The bound is invoked directly by genuineZetaDerivedPhasePerturbationWitness to guarantee that the regular-factor increments remain summable in the log φ scale, and it is the comparison step inside the stronger quadratic-denominator theorem sum_inv_succ_mul_succ_sq_le_one. In the Recognition Science framework it closes the error-control step required for the phi-cost perturbation bounds around meromorphic poles, ensuring that phase-charge increments stay controlled when sampling defects on circles of radius φ^{-k}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.