simulation_reduces_to_tautology
plain-language theorem explainer
In Recognition Science any structure that exactly reproduces the sequence of recognition events is itself an RS universe, so the simulation hypothesis reduces to the tautology that a faithful copy of the ledger is the ledger. Foundational physicists and philosophers of physics would cite this when dissolving Bostrom-style arguments. The proof is a one-line term that reuses the events function and positivity witness from the given RSUniverse to witness the existential.
Claim. For any RS universe $u$ (a map from natural numbers to positive reals) and any simulated universe $s$ (a map from natural numbers to positive reals), if $s(n)=u(n)$ for every $n$, then there exists an RS universe $u'$ such that $u'(n)=u(n)$ for every $n$.
background
RSUniverse is the structure whose only data are a function events : ℕ → ℝ together with the positivity axiom events n > 0 for all n; the module states that any two such structures with identical events are identical, formalizing that the ledger is reality. SimulatedUniverse carries the same signature but is introduced to represent a computational process that produces the same observable outcomes. The local setting, from the module header, treats the simulation hypothesis as a category error: there is no external substrate separate from ledger entries, so the distinction between simulation and reality has no semantic content once events coincide.
proof idea
The proof is a term-mode one-liner. It applies the RSUniverse constructor to the events map and positivity witness already present in u, then uses reflexivity to satisfy the universal quantifier over n.
why it matters
This is theorem IC-004.8 in the module on the simulation hypothesis. It supplies the formal step that any faithful reproduction of RS events is an RS universe, which the module uses to reach the positive claim that the ledger is self-grounded. The result sits inside the broader dissolution of the simulation question (IC-004) and precedes the irrationality statement IC-004.9 on φ. It touches the framework landmark that the ledger is the unique physical substrate with no external computer possible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.