SimulatedUniverse
plain-language theorem explainer
SimulatedUniverse defines a structure of positive real events generated by a computational process matching observable outcomes of an RS universe. Researchers working on Bostrom-style arguments inside Recognition Science cite this definition to formalize the simulation side of the ledger. The declaration is a pure structure with two fields and no proof content.
Claim. A simulated universe is a map $e : ℕ → ℝ$ equipped with the condition $e(n) > 0$ for all $n ∈ ℕ$, representing a computational process that produces the same sequence of events as a Recognition Science universe.
background
Module IC-004 dissolves the simulation hypothesis by treating the ledger as the sole physical substrate. No external computer or separate reality exists; any faithful reproduction of ledger events is itself a ledger. The structure SimulatedUniverse is introduced to model the computational side of Bostrom's argument so that later theorems can equate it with RSUniverse.
proof idea
Structure definition. It declares the type with the events map and the positivity predicate; no lemmas or tactics are invoked.
why it matters
The definition is the modeling step that feeds simulated_rs_is_rs and simulation_reduces_to_tautology. Those theorems show a perfect simulation of an RS universe is an RS universe, closing IC-004.2 and reinforcing that the ledger/reality distinction is empty. It aligns with the framework claim that the ledger is the unique substrate and that the simulation question reduces to a tautology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.