rs_dynamics_beyond_rational
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.