module module moderate

`IndisputableMonolith.Information.SimulationHypothesisStructure`

This module defines the formal structure for the simulation hypothesis within Recognition Science, centering on RSUniverse as the type of all recognition events and introducing SimulatedUniverse together with the IsSimulation relation. It extends the physical Church-Turing thesis to establish self-grounding properties and unprovability results for any simulation. Researchers working on foundational information theory or RS derivations of simulation arguments would cite the module when formalizing how the physical universe remains internally RS.

claimLet $RSUniverse$ denote the type of all recognition events. A $SimulatedUniverse$ satisfies the $IsSimulation$ predicate relative to an outer universe, yielding the unprovability of simulation, self-grounding of the ledger, and the equivalence $rs_exists_iff_zero_cost$.

background

The module sits in the Information domain and imports the RS time quantum from Constants, the cost framework from Cost, and the Church-Turing physics structure whose doc-comment states that the Physical Church-Turing Thesis follows from the RS derivation. It introduces RSUniverse as the type representing all recognition events and builds sibling definitions for SimulatedUniverse, IsSimulation, and ledger self-grounding. These rest on the imported constants and the extension of Turing simulability to physical processes.

proof idea

This is a definition module whose argument proceeds by successive type definitions and direct constructions. It defines RSUniverse and SimulatedUniverse, then proves supporting lemmas such as rs_universe_determined_by_events, simulation_unprovable, outer_universe_is_rs_universe, ledger_is_self_grounded, and simulation_hypothesis_from_ledger by applying the imported Church-Turing results and cost axioms.

why it matters in Recognition Science

The module supplies the structural backbone for discussing the simulation hypothesis inside Recognition Science and feeds the Information domain. It directly extends the Church-Turing physics structure (IC-003) to formalize self-grounding and unprovability, placing the simulation question inside the RS forcing chain and the recognition composition law without introducing new external hypotheses.

scope and limits

Does not decide whether the physical universe is simulated.
Does not supply any concrete simulation algorithm or implementation.
Does not address multi-level or infinite-regress simulations.
Does not derive numerical predictions beyond the imported constants.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Information.ChurchTuringPhysicsStructure module_import

declarations in this module (19)

structure RSUniverse L48
theorem rs_universe_determined_by_events L56
structure SimulatedUniverse L62
theorem simulated_rs_is_rs L71
def IsSimulation L79
theorem simulation_unprovable L85
theorem outer_universe_is_rs_universe L96
def ledger_is_self_grounded L105
theorem ledger_self_grounding L109
theorem rs_exists_iff_zero_cost L115
theorem has_ct_structure L129
def simulation_hypothesis_from_ledger L133
theorem simulation_hypothesis_structure L136
theorem simulation_implies_church_turing L140
def simulation_argument_dissolved L156
theorem simulation_reduces_to_tautology L166
theorem phi_not_finitely_simulable L179
theorem simulation_substrate_must_be_real L185
def ic004_certificate L190