computable_mul
Computable reals are closed under multiplication. Researchers auditing Recognition Science constants cite this closure when confirming that products of approximable quantities, such as factors in the fine-structure constant, remain algorithmically realizable. The proof is a one-line term wrapper that invokes the global instance for the Computable class.
claimIf $x$ and $y$ are computable real numbers, then their product $xy$ is computable.
background
The module examines the distinction between classical proof machinery and the computability of derived constants in Recognition Science. A real number is computable when an algorithm exists that, for each $n$, returns a rational $q$ satisfying $|x - q| < 2^{-n}$. This setting separates proof logic from output properties: constants such as $pi$ and $phi$ remain computable even when proofs employ classical axioms. Upstream results on empirical programs and forcing structures supply the broader RS context but are not invoked here.
proof idea
The proof is a one-line wrapper that applies infer_instance to the Computable class. The accompanying doc-comment records the standard error estimate $|xy - f(k)g(k)| leq |x||y-g(k)| + |g(k)||x-f(k)|$ and notes that initial approximation bounds determine the required extra precision.
why it matters in Recognition Science
This result supplies the multiplicative closure needed for downstream theorems that establish computability of RS constants, including the geometric seed $4pi cdot 11$ and the curvature term $103/(102pi^5)$. It directly supports the module's resolution of the classical-constructive gap by showing that algorithmic approximability of outputs is preserved under the operations used to build $alpha^{-1}$ and related quantities. The declaration therefore anchors the claim that RS-derived constants lie in the predicted numerical bands.
scope and limits
- Does not supply an explicit algorithm for the product approximation function.
- Does not establish closure under multiplication inside a fully constructive logic.
- Does not extend to non-real scalars or to operations outside the listed siblings.
- Does not discharge any hypothesis about the underlying proof axioms.
Lean usage
have h1 : Computable ((4 : ℕ) : ℝ) := inferInstance; have h2 : Computable Real.pi := pi_computable; exact computable_mul h1 h2formal statement (Lean)
214theorem computable_mul {x y : ℝ} (hx : Computable x) (hy : Computable y) :
215 Computable (x * y) := by
proof body
Term-mode proof.
216 -- With the classical approximation-based predicate, this is immediate.
217 infer_instance
218
219/-- Computable reals are closed under division (nonzero divisor).
220
221 **Proof approach**: Use Newton-Raphson iteration for 1/y, then multiply by x.
222 Given y ≠ 0 and approximations g(n) with |y - g(n)| < 2^(-n):
223 1. Find N such that |g(N)| > 2^(-N-1) (exists since y ≠ 0)
224 2. Use Newton iteration: z_{k+1} = z_k(2 - g(n)·z_k)
225 3. Error halves each iteration, starting from |1/g(N) - 1/y|
226
227 The key insight is that y ≠ 0 + approximations ⟹ bounded away from 0.
228
229 **Status**: Axiom (Newton-Raphson algorithm) -/