pith. machine review for the scientific record. sign in
structure definition def or abbrev

SimulatedUniverse

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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". -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.