has_computation_limits_structure
The theorem asserts that the irrationality of phi enforces computation limits on the Recognition Science ledger. Physicists deriving bounds on physical simulation from discrete dynamics would cite it when linking phi to Turing-computable processes. The proof is a one-line wrapper applying the prior structure theorem on phi irrationality.
claimThe irrationality of the golden ratio $phi$ enforces computation limits on the discrete ledger, ensuring that Recognition Science dynamics admit only computable transitions on a finite phase space.
background
The module derives the Physical Church-Turing Thesis from the discrete ledger structure: each entry is a ratio governed by the 8-tick operator on a finite phase space, with transitions via J-cost minimization that map finite states to finite states at bounded rate 1/tau_0. No hypercomputation is possible because the ledger processes only at that rate and cannot jump to infinity. Upstream, computation_limits_from_ledger is defined as the proposition Irrational phi, described as the core structural constraint requiring transcendental arithmetic for exact RS constants. The supporting theorem computation_limits_structure establishes this via the known irrationality of phi.
proof idea
The proof is a one-line wrapper that directly applies the theorem computation_limits_structure, which reduces the claim to the irrationality of phi.
why it matters in Recognition Science
This declaration carries the irrationality constraint forward to establish the Church-Turing physics thesis. It is invoked by church_turing_physics_structure, which states that physical processes in RS are computable because the phase space is finite (8 phases), transitions are computable functions on finite types, and the tick rate is bounded. The result fills IC-003 by showing that phi irrationality (IC-002.4) blocks hypercomputation while preserving computability of the dynamics. It connects to the eight-tick octave and the discrete ledger as the foundation for BQP-bounded physical simulation.
scope and limits
- Does not prove computability for physical models lacking the RS discrete ledger assumptions.
- Does not supply explicit Turing machine encodings of RS dynamics.
- Does not resolve the halting problem for arbitrary ledger sequences.
- Does not address continuous-space limits or approximation errors beyond the irrationality constraint.
formal statement (Lean)
93theorem has_computation_limits_structure : computation_limits_from_ledger :=
proof body
Term-mode proof.
94 computation_limits_structure
95
96/-- The Church-Turing physics property: physical processes are computable. -/