theorem
proved
simulation_hypothesis_structure
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Information.SimulationHypothesisStructure on GitHub at line 136.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
133def simulation_hypothesis_from_ledger : Prop := church_turing_physics_from_ledger
134
135/-- **THEOREM IC-004.7**: The simulation hypothesis structure holds. -/
136theorem simulation_hypothesis_structure : simulation_hypothesis_from_ledger :=
137 has_ct_structure
138
139/-- Church-Turing physics implies simulation-hypothesis structure. -/
140theorem simulation_implies_church_turing (h : simulation_hypothesis_from_ledger) :
141 church_turing_physics_from_ledger := h
142
143/-! ## V. Why the Simulation Question Dissolves -/
144
145/-- The simulation argument requires:
146 1. An external "base reality" R₀
147 2. A simulation R that faithfully reproduces R₀
148 3. Our universe might be R, not R₀
149
150 In RS, this fails because:
151 (a) The ledger IS R₀ — it requires no external substrate
152 (b) Any R that reproduces R₀ is an RS universe with the same structure
153 (c) The question "are we R or R₀?" reduces to "are we the ledger or the ledger?"
154
155 This is proved in theorem simulation_unprovable above. -/
156def simulation_argument_dissolved : String :=
157 "Bostrom's argument: Our universe might be R (simulation) not R₀ (base)\n" ++
158 "RS dissolution:\n" ++
159 " (a) Ledger IS R₀: no external substrate needed\n" ++
160 " (b) Any R = RS universe (theorem simulated_rs_is_rs)\n" ++
161 " (c) R vs R₀ has no observational content in RS\n" ++
162 "Conclusion: The simulation hypothesis is semantically vacuous in RS"
163
164/-- **THEOREM IC-004.8**: The question "is the universe simulated?" reduces to
165 a tautology in RS: any faithful simulation of RS IS RS. -/
166theorem simulation_reduces_to_tautology :