def definition def or abbrev

`simulation_argument_dissolved`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 156def simulation_argument_dissolved : String :=

proof body

Definition body.

 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. -/

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
simulated_rs_is_rs in IndisputableMonolith.Information.SimulationHypothesisStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use