computable_mul
plain-language theorem explainer
Computable reals are closed under multiplication. A researcher verifying that Recognition Science constants remain algorithmically approximable would cite this closure when composing expressions such as the fine-structure seed. The proof is a one-line wrapper that invokes the global classical instance of the approximation predicate.
Claim. If $x, y : ℝ$ admit algorithms producing rationals $f(n), g(n)$ with $|x - f(n)| < 2^{-n}$ and $|y - g(n)| < 2^{-n}$ for every $n$, then there exists an algorithm producing rationals $h(n)$ with $|xy - h(n)| < 2^{-n}$ for every $n$.
background
The module resolves the objection that Recognition Science uses classical Lean machinery while claiming algorithmic foundations. It separates proof logic from output computability: constants such as π, φ and α^{-1} remain computable reals even when proofs invoke classical axioms. A real is computable when there exists f : ℕ → ℚ such that |x - f n| < 2^{-n} for all n (the class Computable). This theorem supplies the multiplicative closure needed to certify that composite RS expressions stay inside the computable reals.
proof idea
The proof is a one-line wrapper that applies infer_instance. The comment notes that the classical approximation-based predicate immediately yields the product bound |xy - f(k)g(k)| ≤ |x||y - g(k)| + |g(k)||x - f(k)| once initial approximations supply bounds on |x| and |y|.
why it matters
The result feeds the four downstream theorems that certify computability of the geometric seed 4π·11, the curvature term 103/(102π^5), and the division and power closures. It directly implements the module's claim that RS-derived constants are computable regardless of classical proof steps, aligning with the framework's requirement that α^{-1} lie inside (137.030, 137.039) and that all mass-ladder and forcing-chain quantities remain algorithmically accessible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.