exists_rat_near
plain-language theorem explainer
The density of the rationals in the reals guarantees that for any real t and positive ε a rational q lies within distance ε of t. Analysts extending Lipschitz maps from ℚ to ℝ via the McShane construction cite this fact as the bridge from discrete to continuous data. The proof is a one-line wrapper that invokes the library lemma placing a rational between t−ε and t+ε and then checks the absolute-value bound by linarith.
Claim. For every real number $t$ and every $ε>0$, there exists a rational number $q$ such that $|t-q|<ε$.
background
The Galerkin Equicontinuity module combines a Lipschitz constant for Fourier coefficients with rational approximation to obtain a dense extension via the McShane upper extension. The local setting is the fully proved development of equicontinuity for Galerkin approximations of the Navier-Stokes equations inside the Recognition Science ledger and phi-forcing structures, with no axioms or sorry statements remaining. This lemma supplies the elementary density step presupposed by the Mathlib import and used to pass from rational data to continuous real functions.
proof idea
The proof obtains a rational q between t−ε and t+ε by calling the library lemma exists_rat_btwn on the open interval produced by linarith. It then rewrites the target inequality with abs_lt and applies linarith to both sides of the resulting conjunction.
why it matters
The result is invoked directly by lipschitz_dense_extension, which constructs the McShane extension of an L-Lipschitz function on the rationals to all reals while preserving the constant and passing to the limit of uniformly Lipschitz sequences. In the Recognition Science framework it completes the rational-approximation step required for the equicontinuity argument in the Galerkin treatment of Navier-Stokes, sitting between the phi-ladder structures and the final dense-extension theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.