RSUniverse
plain-language theorem explainer
RSUniverse encodes the physical universe in Recognition Science solely as a sequence of positive real recognition events. Researchers formalizing the dissolution of the simulation hypothesis cite this structure to equate the ledger with reality and eliminate any external substrate. The declaration is a bare structure definition with no proof obligations or reduction steps.
Claim. An RS universe consists of a map $e : ℕ → ℝ$ together with the condition that $e(n) > 0$ for every natural number $n$.
background
In the module Information.SimulationHypothesisStructure the RS universe is introduced to dissolve Bostrom's simulation argument. The structure captures the ledger of recognition events, which by definition constitute all physical content with no separate substrate. The module states that the ledger IS reality, no outside exists, and the simulation/reality distinction collapses into a category error.
proof idea
The declaration is a structure definition with no proof body. It directly introduces the events field and the positivity constraint events_pos without tactics, reductions, or lemma applications.
why it matters
RSUniverse is the base type for the IC-004 theorems, including rs_universe_determined_by_events, simulated_rs_is_rs, and simulation_unprovable. It realizes the claim that any faithful simulation of an RS universe is itself an RS universe, aligning with the Recognition Composition Law and the forcing chain landmarks T5–T8. The structure closes the scaffolding for the statement that the simulation hypothesis has no semantic content in RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.