simulated_rs_is_rs
plain-language theorem explainer
A simulated universe whose event sequence exactly matches that of an RS universe is itself an RS universe. Researchers examining Bostrom-style arguments in foundational physics would cite this to show the simulation/reality distinction carries no content. The proof is a direct term-mode construction that repackages the simulation's events and positivity witness into an RSUniverse structure.
Claim. Let $U$ be an RS universe with event map $e_U : ℕ → ℝ$ and let $S$ be a simulated universe with event map $e_S : ℕ → ℝ$ such that $e_S(n) = e_U(n)$ for every natural number $n$. Then there exists an RS universe $U'$ whose event map satisfies $e_{U'}(n) = e_S(n)$ for every $n$.
background
In this module an RSUniverse is the structure whose sole content is an event map from natural numbers to positive reals together with the positivity witness. A SimulatedUniverse carries an identical structure but is introduced to represent a putative computational process that reproduces the same observable ledger. The local theoretical setting is the dissolution of the simulation hypothesis: the ledger constitutes reality with no external substrate, so any process that reproduces the events is indistinguishable from the original RS universe.
proof idea
The proof is a one-line term-mode wrapper. It constructs an RSUniverse instance by pairing the simulation's event function with its positivity proof and then uses reflexivity to obtain the required event equality.
why it matters
This result is a core step in IC-004, which dissolves Bostrom's simulation argument by showing that any faithful reproduction of RS events yields another RS universe. It is invoked by the certificate ic004_certificate and the dissolution summary simulation_argument_dissolved. In the Recognition framework it reinforces that the ledger is self-grounded, with no external base reality possible, consistent with the claim that the simulation question is semantically empty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.