phi_computable
The golden ratio φ satisfies the computability predicate, so an algorithm exists producing rational approximations to any prescribed precision. Researchers auditing constructive foundations of Recognition Science cite this when verifying that derived constants remain algorithmically accessible. The proof is a one-line wrapper invoking the type-class instance for the Computable predicate on φ.
claimThe golden ratio φ is computable: there exists a function f : ℕ → ℚ such that ∀ n ∈ ℕ, |φ − f(n)| < 2^{−n}.
background
The module resolves the distinction between classical proof machinery and constructive output by defining the Computable class as the existence of an approximating algorithm for a real number: there exists f : ℕ → ℚ with |x − f n| < 2^{−n} for all n. The Constants structure from LawOfExistence bundles the fundamental parameters including φ. The upstream for structure records the structural properties required for meta-realization of self-reference axioms.
proof idea
The proof is a one-line wrapper that applies infer_instance to discharge the Computable predicate for Constants.phi, relying on the known Fibonacci approximation sequence for φ.
why it matters in Recognition Science
This declaration establishes computability of φ and is used directly by the downstream theorem log_phi_computable to obtain computability of ln φ. It fills the constructive note in the meta module, confirming that Recognition Science constants remain algorithmically accessible despite classical proof techniques. It aligns with T6 where phi is forced as the self-similar fixed point and supports the claim that outputs such as α^{-1} are computable reals.
scope and limits
- Does not supply an explicit algorithm, only existence via type class.
- Does not address computability of arbitrary reals or non-derived constants.
- Does not resolve the use of classical logic in the broader proof system.
- Does not claim that all theorems in the library are constructively provable.
Lean usage
theorem log_phi_computable : Computable (Real.log Constants.phi) := by have hphi : Computable Constants.phi := phi_computable; have hpos : Constants.phi > 0 := Constants.phi_pos; exact computable_log hphi hposformal statement (Lean)
88theorem phi_computable : Computable Constants.phi := by infer_instance
proof body
Term-mode proof.
89
90/-- Helper: 2^n > 0 for any integer n -/