log_phi_computable
plain-language theorem explainer
The natural logarithm of the golden ratio φ is a computable real. Researchers examining constructive foundations for Recognition Science cite this to confirm that derived constants remain algorithmically approximable. The argument applies the computable_log lemma once φ is known to be computable and positive.
Claim. $ln φ$ is computable, where $φ$ is the golden ratio constant from the Recognition Science constants bundle and computability means there exists an algorithm producing rationals $q_n$ with $|x - q_n| < 2^{-n}$ for each $n$.
background
The module addresses the distinction between classical proof machinery and the computability of output constants in Recognition Science. A real $x$ is computable when an algorithm exists that, given $n$, returns a rational $q$ satisfying $|x - q| < 2^{-n}$. The local setting separates proof logic from the algorithmic status of quantities such as $ln φ$ and $π$ even when noncomputable keywords appear in Lean definitions.
proof idea
One-line wrapper that applies computable_log after obtaining Computable φ from phi_computable and the positivity fact Constants.phi_pos.
why it matters
The result forms part of the computability chain inside Meta.ConstructiveNote that supports the claim that RS-derived constants remain computable reals. It aligns with the framework landmark that φ is the self-similar fixed point (T6) whose logarithm appears in mass formulas and the phi-ladder. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.