rs_universe_determined_by_events
plain-language theorem explainer
Any two RS universes that agree on their recognition events at every natural number have identical event sequences. Researchers working on the Recognition Science ledger as the complete physical substrate would cite this to close the simulation hypothesis. The proof is a one-line term that returns the input hypothesis directly.
Claim. Let $u_1$ and $u_2$ be RS universes. If $u_1.events(n) = u_2.events(n)$ for all $n$ in the natural numbers, then the same equality holds for all such $n$.
background
An RSUniverse is a structure whose sole data is a function events from natural numbers to positive real numbers. The module treats the ledger of these events as the complete physical reality, dissolving any substrate distinction required by Bostrom-style simulation arguments. Upstream definitions include the active-edge count A and the actualization operator A, which appear in the surrounding module but are not invoked by this theorem.
proof idea
The proof is a term-mode one-liner that returns the hypothesis h verbatim, establishing the required forall equality of events.
why it matters
This result supplies IC-004.1, the statement that the event ledger determines the universe with no extra structure. It supports the module's claim that the simulation/reality distinction collapses because any ledger is an RS universe. The theorem sits inside the Information domain and aligns with the Recognition Science view that the ledger is self-grounded, consistent with the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.