log_phi_computable
plain-language theorem explainer
The theorem shows that the natural logarithm of the golden ratio is a computable real. Researchers auditing algorithmic properties of Recognition Science constants would cite it when separating proof machinery from output computability. The proof is a short term-mode sequence that invokes phi_computable and positivity, then applies the general computable_log result.
Claim. The natural logarithm of the golden ratio satisfies the computable predicate: there exists a function $f : ℕ → ℚ$ such that for every natural number $n$, $|ln φ - f(n)| < 2^{-n}$.
background
The module addresses the distinction between classical proof steps and the computability of derived constants in Recognition Science. A real number is computable when an algorithm produces rationals within any prescribed error bound, as defined by the Computable class: there exists $f : ℕ → ℚ$ with $|x - f(n)| < 2^{-n}$ for all $n$. The local setting separates proof style (which may use classical logic) from the Turing-computability of outputs such as $ln φ$, $π$, and $α^{-1}$. Upstream results include the structure Constants bundling framework values and the sibling theorem phi_computable establishing that $φ$ itself meets the predicate.
proof idea
The term-mode proof first obtains Computable Constants.phi from the sibling phi_computable. It then records the positivity fact Constants.phi_pos. The final step applies the general computable_log lemma to these two facts, yielding the result for the logarithm.
why it matters
This declaration confirms that $ln φ$ remains algorithmically approximable, reinforcing the framework claim that RS constants are computable reals even when proofs employ classical axioms. It directly supports the module's resolution of the classical-constructive objection by exhibiting a concrete case tied to the phi fixed point and J-uniqueness steps. No immediate downstream theorems are listed, yet the result aligns with broader computability statements for quantities on the phi-ladder and in the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.