computable_log
Computability of the natural logarithm holds for any positive computable real. Researchers confirming algorithmic status of Recognition Science constants cite this when logarithms appear in derived expressions. The argument is a one-line wrapper invoking a global instance for the logarithm on computable reals.
claimIf a real number $x$ admits an algorithm producing rationals $q_n$ with $|x - q_n| < 2^{-n}$ for every $n$ and satisfies $x > 0$, then $x$ admits such an algorithm for $x$ replaced by $ln x$.
background
The module resolves the distinction between classical proof steps and algorithmic output in Recognition Science by showing that derived constants remain computable reals even when proofs use classical logic. A real number is computable when there exists a map from natural numbers to rationals satisfying the error bound $2^{-n}$ at each precision level. This definition is local to the module and independent of the specific proof machinery employed upstream.
proof idea
The proof is a one-line wrapper that applies the global instance for preservation of computability under the real logarithm on positive arguments.
why it matters in Recognition Science
The result feeds the parent theorem establishing computability of $ln phi$, which in turn supports algorithmic verification of constants built from the self-similar fixed point. It directly addresses the module's resolution that output computability is unaffected by classical axioms in the proof, aligning with the framework's claim that quantities such as $phi$ and its logarithms remain constructively accessible.
scope and limits
- Does not construct or certify any explicit algorithm for the logarithm.
- Does not prove the claim inside strictly intuitionistic logic.
- Does not extend the statement to non-positive reals or complex arguments.
- Does not bound the computational resources required for the approximation.
Lean usage
have hphi : Computable Constants.phi := phi_computable; have hpos : Constants.phi > 0 := Constants.phi_pos; exact computable_log hphi hposformal statement (Lean)
261theorem computable_log {x : ℝ} (hx : Computable x) (hpos : x > 0) :
262 Computable (Real.log x) := by
proof body
Term-mode proof.
263 -- Immediate from the global classical instance.
264 infer_instance
265
266/-! ## RS Constants Are Computable -/
267
268/-- The geometric seed 4π·11 is computable. -/