rs_dynamics_approximable
plain-language theorem explainer
The theorem shows that the golden ratio phi, central to RS dynamics, can be approximated to arbitrary precision by rationals. Researchers deriving the physical Church-Turing thesis from Recognition Science ledger structures would cite it to confirm that continuous J-cost transitions stay within Turing-machine bounds. The proof is a direct term-mode application of the density of rationals via the exists_rat_btwn lemma on the symmetric interval around phi.
Claim. For every real number $ε > 0$ there exists a rational $q$ such that $|φ - q| < ε$, where $φ$ denotes the golden ratio arising as the self-similar fixed point of the Recognition Science forcing chain.
background
In the Recognition Science derivation of the physical Church-Turing thesis, the module starts from a discrete ledger whose entries are real ratios updated by an 8-tick operator on a finite phase space of eight phases. Each transition minimizes a J-cost functional that maps finite states continuously, hence approximably by rational arithmetic. The golden ratio phi enters as the fixed point forced by self-similarity in the T0-T8 chain, governing the scaling of mass and energy ladders.
proof idea
The term proof introduces ε and the positivity hypothesis, invokes exists_rat_btwn on the open interval (phi - ε, phi + ε), then packages the resulting rational with the abs_lt characterization of the strict inequality to discharge the existential goal.
why it matters
This result supplies the final approximability step inside the IC-003 certificate, confirming that RS dynamics remain Turing-computable once the ledger is discretized to Fin 8 phases and J-cost steps are continuous. It directly supports the module claim that physical processes lie in BQP and inherit undecidability only from the classical halting problem, without allowing hypercomputation. The placement closes the loop from the discrete ledger structure to rational arithmetic simulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.