Quantitative Integral Comparison for Monotone Series I: The Tail of the p = 2 Series

Jefferson, Bob (2026).Quantitative Integral Comparison for Monotone Series: The Tail of the p = 2 Series.Version 1.1. Abstract This project studies the tail of the p-series at p=2p = 2p=2, R(N)=∑k>N1k2,R(N) = \sum_{k>N} \frac{1}{k^2},R(N)=k>N∑k21, and develops explicit quantitative bounds and structural properties for this quantity using integral comparison and discrete recurrence methods. The main results include: • Exact recurrence R(N)=1(N+1)2+R(N+1)R(N) = \frac{1}{(N+1)^2} + R(N+1)R(N)=(N+1)21+R(N+1) • Explicit global bounds (for N≥1N \ge 1N≥1) 1N+1≤R(N)≤1N+12\frac{1}{N+1} \le R(N) \le \frac{1}{N + \tfrac12}N+11≤R(N)≤N+211 • Monotonicity of the shifted quantity δ(N)=1R(N)−N\delta(N) = \frac{1}{R(N)} - Nδ(N)=R(N)1−N • Limit theorem N R(N)→1N\,R(N) \to 1NR(N)→1 The analysis emphasizes globally valid inequalities with explicit constants and avoids asymptotic expansions or heuristic error terms. A structural viewpoint based on the shifted quantity δ(N)\delta(N)δ(N) clarifies how integral comparison and the discrete recurrence interact to determine the asymptotic behaviour of the tail. All results are formally verified in Lean 4 using mathlib4. The formal development is modular and designed as reusable infrastructure for quantitative integral comparison arguments for monotone series. Repository contents The archive includes: • Lean 4 source files implementing the formal proofs• the accompanying paper (LaTeX source and compiled PDF)• build instructions and project metadata The development builds with Lean 4 and mathlib4. Scope This project lies at the intersection of: • classical analysis• analytic number theory• formal verification of mathematics and illustrates how explicit analytic inequalities and asymptotic statements can be formalized in a proof assistant while preserving clear mathematical structure.