outer_universe_is_rs_universe
plain-language theorem explainer
Any purported outer universe that contains an RS universe must itself be an RS universe, so the simulation-reality distinction collapses. Researchers working on the foundations of physics or Bostrom-style arguments would cite this result. The proof is a one-line term construction that reuses the outer universe and its built-in positivity of events.
Claim. Let $U$ be an RS-universe (a structure whose recognition events satisfy $e_n > 0$ for every natural number $n$). Then there exists an RS-universe $V$ such that $V.e_n > 0$ for all $n$.
background
The module dissolves the simulation hypothesis by showing that the ledger constitutes reality with no external substrate. An RS-universe is the structure whose only data are recognition events $e : ℕ → ℝ$ together with the axiom that every event is positive. The local setting states that any ledger entry is already a physical fact, so an external computer running a simulation would itself have to be a ledger and therefore of the same type.
proof idea
The proof is a one-line term-mode wrapper. It applies the RS-universe structure constructor directly to the supplied outer universe and its events_pos field, producing the required combined universe.
why it matters
The declaration supplies IC-004.4, the final step in the module's argument that the simulation-reality distinction has no semantic content. It reinforces the framework claim that the ledger is self-grounding and that J-cost zero occurs only at the identity element. No downstream theorems are recorded, but the result closes the loop on the claim that a perfectly simulated RS universe is simply an RS universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.