spectrum_gap_persistence
plain-language theorem explainer
Converging real sequences with distinct limits eventually preserve strict order: if λ_N → Λ and μ_N → Μ with Λ < Μ, then λ_N < μ_N for all large N. Spectral analysts in the QG Phase 4 campaign cite this to keep curved eigenvalue branches separated after discretization. The proof is a one-line application of the filter eventually-less-than lemma for sequential limits.
Claim. Let $(\lambda_N)_{N\in\mathbb{N}}$ and $(\mu_N)_{N\in\mathbb{N}}$ be real sequences with $\lambda_N\to\Lambda$ and $\mu_N\to M$. If $\Lambda < M$, then eventually $\lambda_N < \mu_N$ (i.e., there exists $N_0$ such that $\lambda_N < \mu_N$ for all $N\ge N_0$).
background
This module is the Phase 2a spectral-convergence toolkit for the QG full-theory campaign: quantitative eigenvalue limits that later phases consume branch by branch. Sibling results give explicit rates for discrete sine eigenvalues (the flat TT Discrete-Lichnerowicz spectrum) and a squeeze lemma that turns a $C/N^2$ eventual bound into ordinary convergence.
The local objects here are two real sequences indexed by discretization size $N$, thought of as eigenvalue branches of a discrete operator, together with their continuum limits $\Lambda$ and $M$. No operator structure is required: only sequential convergence in $\mathbb{R}$ and a strict inequality of limits.
The module status note records that every lemma below is axiom-clean (no sorry). A planned Courant-Fischer transport lemma was deferred because Mathlib's Hermitian API lacks a min-max characterization; nothing in this file depends on it.
proof idea
One-line term wrapper. Apply the Mathlib filter lemma Tendsto.eventually_lt to the two given Tendsto hypotheses and the strict inequality of limits. That lemma already encodes: if $f\to a$, $g\to b$, and $a<b$, then eventually $f<g$ along the filter. Instantiating the filter as atTop on $\mathbb{N}$ yields the claimed eventual separation.
why it matters
Phase 4 (curved operator convergence) must keep distinct continuum eigenvalue branches from crossing under discretization noise. The module doc names this result as the separation tool: "converging eigenvalue branches with distinct limits eventually separate." Without it, a quantitative rate bound on each branch alone does not guarantee that the discrete spectra remain ordered.
In the broader Recognition gravity stack this sits under the SevenGaps / DiscreteLichnerowicz line: flat TT eigenvalues already have a proved continuum limit, and the toolkit upgrades that to rates plus gap persistence so curved perturbations can be controlled without branch collapse. It does not itself invoke the forcing chain (T0-T8), RCL, or the phi-ladder; it is pure analysis infrastructure those later gravity arguments rely on.
No downstream consumers are wired yet in the graph (used_by empty); the intended landing site is the Phase 4 curved-branch separation argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.