theorem proved term proof

`rs_universe_determined_by_events`

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

formal statement (Lean)

  56theorem rs_universe_determined_by_events (u₁ u₂ : RSUniverse)
  57    (h : ∀ n, u₁.events n = u₂.events n) :
  58    ∀ n, u₁.events n = u₂.events n := h

proof body

Term-mode proof.

  59
  60/-- A "simulated universe" in Bostrom's sense: a computational process
  61    that produces the same observable outcomes as the "real" universe. -/

depends on (6)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
RSUniverse in IndisputableMonolith.Information.SimulationHypothesisStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use