rational_computable
plain-language theorem explainer
Every rational number embedded in the reals admits a trivial computable approximation by the constant function returning that same rational at every precision. Researchers auditing the constructive foundations of Recognition Science cite this to confirm that rational-derived constants remain algorithmically approximable. The instance is a one-line wrapper supplying the constant approximant and invoking positivity of powers of two to bound the zero error.
Claim. For every rational $q$, the real number $q$ is computable: there exists a function $f : ℕ → ℚ$ such that for all $n$, $|q - f(n)| < 2^{-n}$.
background
The Computable class states that a real $x$ is computable when an algorithm exists returning, for each precision $n$, a rational $f(n)$ with $|x - f(n)| < 2^{-n}$. This module separates proof machinery (classical logic in Lean) from output computability, showing that derived RS constants remain algorithmically accessible even when proofs use noncomputable keywords. The helper lemma two_zpow_pos establishes that $2^n > 0$ for any integer $n$, which is used to verify error bounds.
proof idea
One-line wrapper that constructs the constant function returning $q$ for every input and applies two_zpow_pos to confirm the zero error satisfies the strict inequality.
why it matters
This instance supports the module's resolution of the classical-versus-constructive objection by establishing that all rationals are computable reals. It underpins closure properties for arithmetic on computable numbers and reinforces that RS constants (phi, pi, alpha inverse) remain algorithmically approximable regardless of proof style. The declaration fills the formal statement that derived constants of RS are computable reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.