rs_dynamics_beyond_rational
Recognition Science dynamics require exact values of the golden ratio φ in φ-ladders for mass formulas and ledger transitions; since φ is irrational, exact RS computations cannot be performed by finite rational algorithms and fall outside classical Turing machines. Physicists deriving discrete ledger states or mass spectra from the forcing chain would cite this to separate exact from approximable cases. The proof is a one-line term wrapper that applies the no_exact_phi_computation lemma to any assumed rational equality.
claim$φ$ is irrational: there does not exist a rational $q$ such that $q = φ$ holds in the reals.
background
The module derives the Physical Church-Turing Thesis from the discrete ledger structure of Recognition Science: each ledger entry is a ratio in ℝ governed by the 8-tick operator on a finite phase space, with J-cost minimization mapping finite states via continuous functions. Upstream, no_exact_phi_computation (from ComputationLimitsStructure) establishes that φ cannot equal any rational, while PhiForcingDerived.of supplies the structure of J-cost and the self-similar fixed point φ. Related upstream results include LedgerFactorization.of for the (ℝ₊, ×) calibration and SpectralEmergence.of for the forced gauge and generation content.
proof idea
The proof is a one-line term-mode wrapper: it takes the assumed pair ⟨q, hq⟩ where q is rational and hq asserts equality to φ, then directly invokes the no_exact_phi_computation lemma on those arguments.
why it matters in Recognition Science
This fills IC-003.12 in the Church-Turing derivation, showing exact RS dynamics exceed Turing machines while approximate ones remain inside them. It feeds the downstream ic003_certificate that assembles the full status summary including phase_space_finite and phase_functions_finite. The result anchors the separation between exact φ-ladder computations and rational approximations, consistent with the eight-tick octave and the irrationality forced by T5 J-uniqueness in the unified forcing chain.
scope and limits
- Does not prove that RS dynamics are uncomputable in the approximate sense.
- Does not address halting or undecidability for specific ledger problems.
- Does not claim that all physical processes reduce to Turing machines.
- Does not extend to hypercomputation or non-approximable real computations.
formal statement (Lean)
158theorem rs_dynamics_beyond_rational : ¬ ∃ q : ℚ, (q : ℝ) = phi :=
proof body
Term-mode proof.
159 fun ⟨q, hq⟩ => no_exact_phi_computation q hq
160
161/-- **THEOREM IC-003.13**: However, RS dynamics can be approximated to arbitrary
162 precision by rational arithmetic (since ℝ is the completion of ℚ).
163 This places approximate RS computations within Turing-machine computation. -/