phi_computable
plain-language theorem explainer
The golden ratio φ is a computable real, so there exists an algorithm producing rationals within any 2^{-n} error. Researchers resolving the classical-constructive tension in Recognition Science cite this to separate proof machinery from output approximability. The proof is a one-line wrapper that invokes instance inference on the Computable class for Constants.phi.
Claim. The golden ratio satisfies computability: there exists a function $f : ℕ → ℚ$ such that $|φ - f(n)| < 2^{-n}$ for every natural number $n$.
background
The module resolves the objection that Recognition Science claims algorithmic foundations yet employs classical Lean axioms. It separates proof logic from the computability of derived constants, noting that π and φ remain approximable by algorithms even when proofs use classical reasoning. The Computable class encodes this via an approximating map from naturals to rationals with error less than 2^{-n}. Upstream, the Constants structure from LawOfExistence bundles φ among the CPM constants, while the self-reference axioms supply the structural setting in which φ arises as the fixed point.
proof idea
The proof is a one-line wrapper that applies infer_instance to discharge the Computable Constants.phi goal. Lean resolves the instance from the definition of the Computable class together with the known Fibonacci-ratio approximations to φ.
why it matters
This result anchors the claim that derived constants stay algorithmically accessible. It is invoked directly by the downstream theorem log_phi_computable establishing computability of ln φ. In the framework it confirms that the self-similar fixed point φ (T6) is computable, supporting the eight-tick octave and the phi-ladder mass formula without requiring constructive proof machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.