computable_mul
Computable reals are closed under multiplication. Researchers verifying that Recognition Science constants remain algorithmically approximable cite this closure when composing products such as the alpha seed. The proof is a one-line wrapper invoking the global instance for the approximation predicate.
claimIf a real number $x$ admits an algorithm producing rationals within $2^{-n}$ for every $n$, and likewise for $y$, then the product $xy$ admits such an algorithm.
background
The module resolves the objection that Recognition Science uses classical Lean proofs while claiming algorithmic foundations. It separates proof machinery from output computability: derived constants such as pi, phi, and alpha inverse remain computable reals even when proofs invoke classical logic. A real is computable when there exists a function from naturals to rationals satisfying the error bound |x - f(n)| < 2^{-n} for all n. The sibling class Computable encodes exactly this witness.
proof idea
One-line wrapper that applies the global instance for multiplication closure under the classical approximation predicate. The comment notes that the predicate makes the result immediate once the class is defined.
why it matters in Recognition Science
This closure feeds the four downstream theorems that establish computability of the alpha seed 4 pi 11, the curvature term 103 over 102 pi to the fifth, and the division and power operations needed for the full set of RS-native constants. It directly supports the module's claim that all derived constants of Recognition Science are computable reals regardless of classical proof steps. The result sits inside the eight-tick octave and phi-ladder constructions that require explicit algorithmic access to constants.
scope and limits
- Does not supply an explicit approximation function for the product.
- Does not extend the closure to non-real number systems.
- Does not address computability under limits or infinite sums.
- Does not replace the classical instance with a constructive extraction.
Lean usage
exact computable_mul (computable_mul h1 h2) h3formal 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) -/