computable_log
plain-language theorem explainer
The theorem establishes that the natural logarithm of any positive computable real remains computable. Researchers verifying algorithmic approximability of Recognition Science constants would cite it when confirming that logarithmic derivations preserve computability. The proof is a one-line wrapper invoking a global classical instance.
Claim. If $x$ is a computable real and $x > 0$, then the natural logarithm of $x$ is computable.
background
The module resolves the objection that classical proof machinery undermines Recognition Science's algorithmic claims by separating proof logic from output computability. A real number is computable when an algorithm exists that, for any $n$, returns a rational $q$ satisfying $|x - q| < 2^{-n}$. The local setting stresses that constants such as $φ$ and $π$ remain computable reals even when proofs rely on classical axioms.
proof idea
The proof is a one-line wrapper that applies the global classical instance for the logarithm on positive reals.
why it matters
This result is invoked by log_phi_computable to conclude that ln φ is computable. It supports the module's formal statement that derived RS constants are computable regardless of classical proof steps. The declaration closes part of the classical-versus-constructive gap while aligning with the framework's requirement that constants like φ remain algorithmically accessible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.