SimulatedUniverse

formal source

  59
  60/-- A "simulated universe" in Bostrom's sense: a computational process
  61    that produces the same observable outcomes as the "real" universe. -/
  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". -/
  71theorem simulated_rs_is_rs (u : RSUniverse) (s : SimulatedUniverse)
  72    (h : ∀ n, s.events n = u.events n) :
  73    ∃ u' : RSUniverse, ∀ n, u'.events n = s.events n :=
  74  ⟨⟨s.events, s.events_pos⟩, fun n => rfl⟩
  75
  76/-! ## II. The Simulation Question is Semantically Empty -/
  77
  78/-- The "simulation predicate": is universe u "really" a simulation? -/
  79def IsSimulation (u : RSUniverse) : Prop :=
  80  ∃ (outer : RSUniverse), ∀ n, outer.events n ≠ u.events n
  81
  82/-- **THEOREM IC-004.3**: The simulation predicate is not provably true for any RS universe.
  83    This formalizes: "there is no fact of the matter" about simulation in RS.
  84    Any "outer-universe" would itself be an RS universe with the same structure. -/
  85theorem simulation_unprovable :
  86    ∀ u : RSUniverse, ¬ (∀ (outer : RSUniverse), ∀ n, outer.events n ≠ u.events n) := by
  87  intro u h
  88  -- Take outer = u itself
  89  have := h u
  90  -- Then for all n, u.events n ≠ u.events n — contradiction
  91  exact absurd rfl (this 0)
  92