computable_mul
plain-language theorem explainer
Computable reals are closed under multiplication: if x and y each admit an algorithm producing rationals within 2^(-n), then xy does as well. Researchers auditing the computability of Recognition Science constants cite this closure property when assembling products such as 4 pi 11. The proof is a one-line wrapper that invokes the global classical instance for the approximation predicate.
Claim. Let $x, y$ be real numbers. If there exist algorithms $f, g : ℕ → ℚ$ such that $|x - f(n)| < 2^{-n}$ and $|y - g(n)| < 2^{-n}$ for all $n$, then there exists an algorithm $h$ such that $|xy - h(n)| < 2^{-n}$ for all $n$.
background
The module addresses Gap 2 between classical proof machinery and the claim that RS outputs are algorithmic. It separates proof logic from output computability: classical axioms in Lean do not prevent derived constants from being computable reals. The central definition is the Computable class: a real admits an algorithm that, on input n, returns a rational q with absolute error less than 2^{-n}. This predicate is inherited from Mathlib's classical approximation theory and is used uniformly for constants such as pi and phi.
proof idea
The proof is a term-mode one-liner. It applies infer_instance to the global classical instance that the product of two computable reals remains computable under the approximation predicate. The accompanying comment notes that the error bound |xy - f(k)g(k)| ≤ |x||y - g(k)| + |g(k)||x - f(k)| is handled automatically by the instance once initial approximations exist.
why it matters
This closure result supplies the algebraic step needed to certify that RS-native constants remain computable. It is invoked directly by alpha_seed_computable to establish that 4 pi 11 is computable, by curvature_computable for the 103/(102 pi^5) term, and by the companion theorems for division and exponentiation. In the framework it closes the constructive gap identified in the module: the derived constants of RS (including those entering the alpha band and the phi-ladder) are algorithmically approximable even though the surrounding proofs employ classical logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.