simulation_substrate_must_be_real
plain-language theorem explainer
Recognition Science dynamics depend on the irrational golden ratio φ, so any exact reproduction requires real-number substrates rather than rationals. Researchers analyzing simulation hypotheses in physics would cite this to constrain possible computational realizations of the ledger. The proof is a one-line application of the established result that no rational equals φ.
Claim. For every rational number $q$, the corresponding real number differs from the golden ratio: $q ≠ ϕ$.
background
The module dissolves the simulation hypothesis by identifying the ledger with reality itself: no external substrate or outside computer exists, as any such entity would itself be a ledger entry. This theorem IC-004.10 follows from the irrationality of φ, which enters RS through the J-cost function and the self-similar fixed point on the phi-ladder. It rests on the upstream theorem IC-002.7: 'There is no finite-precision algorithm that exactly computes φ in the sense that any rational number differs from φ.'
proof idea
one-line wrapper that applies no_exact_phi_computation, which itself reduces to the irrationality of phi via Set.mem_range.
why it matters
The result fills IC-004.10 in the dissolution of Bostrom-style simulation arguments, showing that exact RS reproduction (including constants such as ħ = φ^{-5}) forces real arithmetic. It aligns with the forcing chain where T5 and T6 fix φ as the unique self-similar point, and it closes one path in the information-structure module with no further downstream uses recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.