SimulatedUniverse
The SimulatedUniverse structure encodes a Bostrom-style simulation as a positive real sequence of events. Foundations researchers cite it when formalizing that perfect reproduction of RS events collapses any simulation-reality distinction. The declaration is a direct structure definition with an events map and a positivity constraint.
claimA simulated universe is a pair consisting of a function $e : ℕ → ℝ$ together with a proof that $e(n) > 0$ for every natural number $n$.
background
Recognition Science dissolves the simulation hypothesis by equating the ledger with physical reality, so no external substrate remains. The module states that any computational process producing identical observables is operationally indistinguishable from the ledger itself. Upstream ledger factorization supplies the event structure while the integration gap fixes the active edge count per tick at A = 1.
proof idea
The declaration is a structure definition that directly introduces the two fields events and events_pos.
why it matters in Recognition Science
It supplies the type used by the parent theorems simulated_rs_is_rs and simulation_reduces_to_tautology, which establish that any faithful simulation of an RS universe is itself an RS universe. This fills IC-004 by rendering the simulation question a tautology, consistent with the ledger being the unique substrate and the phi-ladder grounding all event sequences.
scope and limits
- Does not model any internal computational steps of the simulation.
- Does not assert existence of any simulated universe.
- Does not address imperfect or approximate simulations.
- Does not engage with physics outside the RS ledger framework.
formal statement (Lean)
62structure SimulatedUniverse where
63 /-- The simulation's events (what it generates). -/
64 events : ℕ → ℝ
65 /-- The simulation's events are also positive. -/
66 events_pos : ∀ n, events n > 0
67
68/-- **THEOREM IC-004.2**: A simulated universe that perfectly reproduces
69 all events of an RS universe IS an RS universe.
70 There is no difference between "simulated RS" and "RS". -/