module module high

`IndisputableMonolith.Information.SimulationHypothesisStructure`

This module defines the formal structure for the simulation hypothesis in Recognition Science, introducing RSUniverse as the type of all recognition events together with SimulatedUniverse and IsSimulation predicates. Researchers in foundational physics and information-theoretic derivations cite it when examining whether physical processes admit simulation within the RS framework. The module organizes definitions and lemmas that draw directly from the imported Constants, Cost, and Church-TuringPhysicsStructure without containing proofs.

claimThe module introduces the RS physical universe as a type representing all recognition events, together with a simulated-universe type and predicates capturing simulation relations and unprovability of simulation.

background

Recognition Science treats the physical universe as built from recognition events whose costs are measured by the J-function and organized on the phi-ladder. The module sits in the Information domain and imports the fundamental time quantum τ₀ = 1 tick, the cost structure, and the RS derivation of the Physical Church-Turing Thesis, which asserts that every physical process is simulable by a Turing machine.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the type and relation infrastructure that supports downstream claims such as simulation_hypothesis_from_ledger, rs_exists_iff_zero_cost, and ledger_self_grounding. It thereby contributes to the framework's treatment of the outer universe as the RS universe and to the self-grounded character of the ledger.

scope and limits

Does not prove that the physical universe is simulated.
Does not derive quantitative physical predictions from the simulation predicates.
Does not address multi-level or infinite-regress simulations.
Does not incorporate measurement postulates beyond the imported Church-Turing extension.

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