phi_not_finitely_simulable
plain-language theorem explainer
The theorem establishes that the ledger constant φ cannot equal any rational number. Researchers studying computational limits or simulation hypotheses in physics would cite it to show that exact RS reproduction requires real-number arithmetic. The proof is a one-line wrapper applying the prior result that no rational equals φ.
Claim. There does not exist a rational number $q$ such that $q = φ$ when viewed in the reals.
background
The module dissolves the simulation hypothesis by identifying the ledger with reality itself, so that no external substrate or outside computer can be distinguished. The constant φ is the self-similar fixed point arising in the forcing chain and the J-cost function. This theorem sits inside the IC-004 sequence on information structure.
proof idea
One-line wrapper that applies no_exact_phi_computation to the assumed rational q, using the fact that any rational differs from φ.
why it matters
It supplies IC-004.9, the statement that φ is not rational, which feeds the ic004_certificate establishing that any exact reproduction of RS dynamics must operate on reals. The result underscores that RS contains genuinely irrational facts and constrains possible simulation substrates, consistent with the ledger being the unique physical ground.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.