eigenvalue_limit_of_uniform_bound
plain-language theorem explainer
A uniform eventual bound |λ_N − Λ| ≤ C/N² forces λ_N → Λ in the reals. Analysts in the QG spectral-convergence toolkit cite it whenever a quantitative eigenvalue rate is already in hand and only the qualitative limit is needed. The proof is a one-line squeeze: nonnegativity of distance, the given rate, and C/N² → 0.
Claim. Let $\lambda:\mathbb{N}\to\mathbb{R}$ and fix $\Lambda,C\in\mathbb{R}$ and $N_0\in\mathbb{N}$. If $|\lambda_N-\Lambda|\le C/N^2$ for every $N\ge N_0$, then $\lambda_N\to\Lambda$ as $N\to\infty$.
background
This lives in the Spectral Convergence toolkit (QG full-theory campaign, Phase 2a): a small library of quantitative eigenvalue limits used later by curved-operator and continuum-energy arguments. All results in the module are proved and axiom-clean.
The only nontrivial upstream ingredient is the helper that $C/N^2\to 0$ along the naturals (const_div_sq_tendsto_zero), obtained by composing $x\mapsto x^2\to\infty$ with reciprocal continuity at infinity. Distance on $\mathbb{R}$ is the absolute value, so the rate hypothesis is already a bound on $\mathrm{dist}(\lambda_N,\Lambda)$.
The doc-comment names the role explicitly: the lemma is "trivial, but it names the pattern Phase 4 applies to every curved eigenvalue branch." Downstream consumers (discrete sine eigenvalues, one-mode cylinder variances, Freudenthal witness energy) all produce a $C/N^2$ rate and then invoke this squeeze for the qualitative limit.
proof idea
Rewrite Tendsto as distance-to-limit tending to zero. Apply the squeeze theorem for filters: the distance is eventually nonnegative (always), eventually bounded above by $C/N^2$ (the hypothesis after filtering $N\ge N_0$), and $C/N^2\to 0$ by const_div_sq_tendsto_zero. Concretely: tendsto_iff_dist_tendsto_zero, then squeeze_zero' with Eventually.of_forall dist_nonneg, the rate helper, and filter_upwards on eventually_ge_atTop N₀ to discharge the bound via Real.dist_eq.
why it matters
Phase 2a reusable analysis: every quantitative spectral rate in the gravity campaign funnels through this named squeeze rather than re-proving Tendsto ad hoc. Downstream it discharges the qualitative half of the discrete-sine eigenvalue package (discrete_sine_eigenvalue_tendsto from the sharp expansion), the one-mode cylinder variance limit (modeVarianceReal_tendsto from the $1/6N^{-2}$ rate), and the Freudenthal witness closed-form energy limit (witness_closed_form_tendsto). It also feeds curvature-correction consistency (curvatureCorrectionConsistent_of_rateBound) and the EnergyLimitStatus bookkeeping for the continuum action limit.
In the campaign architecture this is the bridge from Phase-2a rates to Phase-4 curved branch convergence: once each branch has a uniform $C/N^2$ defect, this lemma yields $\lambda_N\to\Lambda$ and, with gap persistence, keeps branches separated. No Recognition landmark (T5–T8, RCL, $\phi$) is invoked; the content is pure real analysis supporting the discrete-to-continuum gravity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.