no_exact_phi_computation
plain-language theorem explainer
No rational number equals the golden ratio φ in the reals. Researchers on computation limits and simulation hypotheses cite this to show that exact RS dynamics require irrational precision beyond finite rational arithmetic. The proof is a one-line wrapper that reduces equality to membership in the image of the rational-to-real coercion and invokes the established irrationality of φ.
Claim. For every rational number $q$, the real number obtained by coercing $q$ is not equal to the golden ratio $varphi$.
background
The module IC-002 derives computation limits in Recognition Science from temporal discreteness (tick τ₀ as minimum time quantum), irrational constants such as φ, and the Landauer erasure cost. φ appears as the self-similar fixed point forced by the J-uniqueness relation in the unified forcing chain. The upstream theorem phi_irrational establishes that φ is irrational by reduction to the irrationality of √5 via Mathlib's goldenRatio.
proof idea
The term-mode proof assumes (q : ℝ) = phi for contradiction. It applies the upstream theorem phi_irrational, which asserts Irrational phi, by exhibiting q as a witness via Set.mem_range.mpr.
why it matters
This result supplies the IC-002.7 step in the computation-limits structure and is invoked directly by rs_dynamics_beyond_rational and phi_not_finitely_simulable. It shows that φ-ladder states lie outside exact Turing-machine computation while remaining approximable, reinforcing the framework distinction between rational and real-number substrates. The theorem closes the irrational-constant source of limits listed in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.