phi_computable
The golden ratio φ is a computable real, so an algorithm exists that produces rational approximations to any dyadic precision. Researchers defending the algorithmic character of Recognition Science constants cite this result to separate proof machinery from output computability. The proof is a one-line instance resolution that invokes the Fibonacci-ratio approximation property of φ.
claimThere exists a function $f : ℕ → ℚ$ such that for every $n ∈ ℕ$, $|φ - f(n)| < 2^{-n}$, where $φ$ is the golden ratio.
background
The Computable class on reals requires a witness function that, for each precision index n, returns a rational within distance 2^{-n}. This module separates classical proof steps from the computability of derived outputs to address critiques of Recognition Science foundations. Upstream, the Constants structure from LawOfExistence bundles the CPM parameters that include φ, while the for structure from UniversalForcingSelfReference records the meta-realization axioms needed for self-reference.
proof idea
The proof is a one-line wrapper that applies infer_instance to the Computable typeclass for Constants.phi. The instance is supplied by the classical Fibonacci approximation sequence whose error bound decays exponentially, as recorded in the module comment on F_{n+1}/F_n convergence.
why it matters in Recognition Science
This supplies the computability of φ required by the downstream theorem log_phi_computable. It fills the constructive gap in the meta layer, confirming that the self-similar fixed point φ (T6 in the forcing chain) yields algorithmically accessible constants even when proofs employ classical logic. The result supports the broader claim that all RS-derived reals remain computable.
scope and limits
- Does not establish that the proof logic itself is constructive.
- Does not supply an explicit approximation algorithm or code.
- Does not extend computability to constants outside the RS set without further instances.
- Does not address physical interpretations or forcing-chain steps beyond φ.
Lean usage
have hphi : Computable Constants.phi := phi_computableformal 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 -/