IsSimulation
plain-language theorem explainer
IsSimulation defines a predicate on an RS universe asserting existence of an outer universe whose event sequence differs at every natural-number index. Researchers formalizing the simulation hypothesis inside Recognition Science cite this when dissolving Bostrom-style arguments into ledger self-identity. The definition is a direct existential quantification over distinct event functions with no additional lemmas.
Claim. Let $u$ be a universe whose recognition events form a function $e_u : ℕ → ℝ$ with all values positive. The predicate holds for $u$ precisely when there exists another such universe $v$ satisfying $e_v(n) ≠ e_u(n)$ for every natural number $n$.
background
RSUniverse is the structure whose sole data is an event function from naturals to positive reals; the module records that any two universes agreeing on all events are identical, so the ledger constitutes the entire physical content. The surrounding IC-004 section states that the simulation hypothesis is meaningless in Recognition Science because every ledger entry is the reality itself and no external substrate can be distinguished. Upstream structures supply the J-cost calibration and ledger factorization that fix the event values, but the predicate itself only compares two such event sequences.
proof idea
Direct definition: the body is the existential statement over an outer RSUniverse whose event function differs pointwise from the input.
why it matters
The definition supplies the formal predicate that the sibling theorem simulation_unprovable then shows cannot be proved inside any RS universe, thereby closing the IC-004 dissolution of the simulation hypothesis. It encodes the module claim that the ledger is the unique physical substrate and that any purported outer computer would itself be another ledger entry. The construction touches the self-grounding of the ledger and the absence of an external observer required by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.