log_phi_computable
ln φ is shown to be computable as a real number. Workers on the constructive foundations of Recognition Science cite this when defending the algorithmic status of derived constants against critiques of classical proof machinery. The argument reduces immediately to the computable_log function applied to the known computability and positivity of φ.
claimThe real number $ln φ$ is computable: there exists a function $f:ℕ→ℚ$ such that for all $n$, $|ln φ - f(n)| < 2^{-n}$.
background
The module examines the distinction between proof machinery and output computability in Recognition Science. It clarifies that classical logic in Lean proofs does not preclude the computability of derived constants such as φ and its logarithm. The Computable class asserts the existence of an algorithmic approximation: for a real x, there is a sequence of rationals converging to within 2^{-n}. Constants.phi is the golden ratio fixed point from the forcing chain. This theorem relies on the upstream phi_computable result establishing the same property for φ itself.
proof idea
A term-mode proof that invokes phi_computable to obtain the hypothesis for computable_log, adds the positivity fact Constants.phi_pos, and discharges the goal by exact application of computable_log.
why it matters in Recognition Science
It contributes to the formal verification that RS constants remain computable reals, supporting the claim that the framework's outputs are algorithmic despite classical proof steps. The result aligns with the T5 J-uniqueness and T6 phi fixed point in the unified forcing chain. It closes one instance of the constructive note gap without introducing new scaffolding.
scope and limits
- Does not claim that the proof itself is constructive.
- Does not compute an explicit approximation sequence for ln φ.
- Does not extend to other transcendental functions of RS constants.
- Does not address computability in alternative foundations.
formal statement (Lean)
277theorem log_phi_computable : Computable (Real.log Constants.phi) := by
proof body
Term-mode proof.
278 have hphi : Computable Constants.phi := phi_computable
279 have hpos : Constants.phi > 0 := Constants.phi_pos
280 exact computable_log hphi hpos
281
282/-- The curvature term 103/(102π⁵) is computable. -/