module module high

`IndisputableMonolith.Information.SimulationHypothesisStructure`

This module defines the formal structure for the simulation hypothesis in Recognition Science, introducing the RS physical universe as the type of all recognition events along with simulation predicates and grounding conditions. Physicists or philosophers examining the physical Church-Turing thesis and simulation arguments would cite these definitions when formalizing whether an RS universe can be embedded in another. The module assembles definitions from the constants, cost, and Church-Turing modules with no internal proofs.

claimLet $U$ be the type whose elements are recognition events comprising the RS physical universe. A simulated universe is a structure $S$ equipped with an embedding map into $U$ such that the embedding satisfies the zero-cost condition derived from the recognition composition law, with the predicate $IsSimulation$ expressing that $S$ is realized inside $U$.

background

The module sits in the Information domain and imports the RS time quantum $τ_0 = 1$ tick from Constants, cost functions from Cost, and the Physical Church-Turing Thesis extension from ChurchTuringPhysicsStructure. The upstream Church-Turing module states that every physical process can be simulated by a Turing machine as a direct consequence of Recognition Science. The supplied doc-comment identifies the central object as the RS physical universe, formalized as the type of recognition events, which supplies the base for all sibling declarations on simulation and ledger grounding.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the structural definitions required by the simulation hypothesis, including the zero-cost existence condition and self-grounding of the ledger that appear in sibling declarations. It extends the Church-Turing physics structure into the simulation setting and connects to the recognition composition law, providing the interface for later results on whether an RS universe can be shown to be simulated.

scope and limits

Does not prove the universe is simulated.
Does not derive numerical predictions or spectra.
Does not interface with the T0-T8 forcing chain.
Does not address computational resources of any simulation.

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