simulation_argument_dissolved

formal source

 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 :
 167    ∀ (u : RSUniverse) (s : SimulatedUniverse),
 168      (∀ n, s.events n = u.events n) →
 169      ∃ u' : RSUniverse, ∀ n, u'.events n = u.events n := by
 170  intro u s h
 171  exact ⟨⟨u.events, u.events_pos⟩, fun n => rfl⟩
 172
 173/-! ## VI. The Positive RS Alternative: Ledger as Self-Evident Reality -/
 174
 175/-- **THEOREM IC-004.9**: φ (the ledger constant) is not rational.
 176    This means RS reality contains genuinely irrational facts —
 177    no finite "simulation program" can exactly reproduce φ.
 178    If the universe were a finite simulation, φ-based physics would fail. -/
 179theorem phi_not_finitely_simulable : ¬ ∃ q : ℚ, (q : ℝ) = phi :=
 180  fun ⟨q, hq⟩ => no_exact_phi_computation q hq
 181
 182/-- **THEOREM IC-004.10**: Any universe that exactly reproduces RS dynamics
 183    (including the irrational φ) must operate on real numbers, not rationals.
 184    This constrains "simulation" substrates to real-number computers. -/
 185theorem simulation_substrate_must_be_real :
 186    ∀ (q : ℚ), (q : ℝ) ≠ phi := no_exact_phi_computation