computable_log
plain-language theorem explainer
The natural logarithm preserves computability on positive reals. Workers verifying that Recognition Science constants remain algorithmically approximable cite this when confirming that logs of derived quantities stay inside the computable reals. The proof is a one-line wrapper invoking a global instance for the logarithm operation.
Claim. If a real number $x > 0$ admits an algorithm that, for every $n$, produces a rational $q$ with $|x - q| < 2^{-n}$, then the same holds for $ln x$.
background
The Computable class, defined in this module, states that a real admits a sequence of rational approximations with error less than $2^{-n}$. The module addresses the distinction between classical proof machinery and output computability for Recognition Science constants. It notes that quantities such as $pi$ and $phi$ remain computable even when proofs use classical logic, and that the derived constants satisfy the algorithmic approximation property regardless of the logic employed in their derivation.
proof idea
One-line wrapper that applies infer_instance to the global classical instance for Real.log on positive reals.
why it matters
This theorem is invoked directly by log_phi_computable to establish that ln phi is computable. It supports the module's resolution of the classical-versus-constructive objection by confirming that logarithms of RS-native constants remain algorithmically accessible. The result aligns with the framework's emphasis on computable outputs for constants such as hbar = phi^{-5} and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.