const_div_sq_tendsto_zero
plain-language theorem explainer
For any fixed real constant C, the sequence C/N² tends to 0 as N runs through the naturals to infinity. Spectral-analysis and discrete-to-continuum gravity arguments cite it as the rate that closes a squeeze. The proof is a short filter composition: N² → ∞ at infinity, then constant-over-that tends to 0.
Claim. For every real constant $C$, the map $N \mapsto C/N^2$ (with $N$ a natural number) tends to $0$ in the reals as $N \to \infty$.
background
This lives in the spectral convergence toolkit for the QG full-theory campaign (Phase 2a): reusable, axiom-clean analysis lemmas that turn quantitative eigenvalue bounds into ordinary limits. The module's main consumer pattern is: if a discrete eigenvalue branch satisfies $|\lambda_N - \Lambda| \le C/N^2$ eventually, then $\lambda_N \to \Lambda$.
The only analytic content needed here is the standard filter topology on $\mathbb{R}$ and $\mathbb{N}$: neighborhoods of 0, the filter atTop, and the fact that positive powers send atTop to atTop. No Recognition-Science cost functional, phi-ladder, or gravity operator enters the statement; those appear only in the lemmas that call this helper.
Downstream, the squeeze theorem packages this rate into eigenvalue_limit_of_uniform_bound, which Phase 4 applies branch-by-branch to curved discrete operators.
proof idea
Two steps. First, establish that $N \mapsto N^2$ tends to $+\infty$ along naturals: lift Mathlib's tendsto_pow_atTop (for the real map $x \mapsto x^2$, using $2 \ne 0$) and compose with tendsto_natCast_atTop_atTop. Second, apply tendsto_const_nhds.div_atTop to the constant sequence $C$ over that diverging denominator, which yields $C/N^2 \to 0$.
why it matters
The declaration is the named rate piece inside the squeeze that Phase 4 uses for every curved eigenvalue branch. Its sole direct parent is eigenvalue_limit_of_uniform_bound, whose doc-comment states: if $|\mathrm{lam}, N - \Lambda| \le C/N^2$ for all $N \ge N_0$, then $\mathrm{lam}, N \to \Lambda$. That parent is itself the glue between the sharp discrete-sine expansion $|4N^2\sin^2(\pi k/N) - (2\pi k)^2| \le ((2\pi k)^4/12)/N^2$ and the qualitative continuum limit of the Discrete Lichnerowicz flat TT spectrum.
In the broader campaign this is scaffolding for spectrum-gap persistence and curved-operator convergence, not a physics claim on its own. It does not touch T0–T8, the Recognition Composition Law, or the mass ladder; it is pure analysis that keeps the gravity spectral limits rate-controlled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.