pith. machine review for the scientific record. sign in
theorem proved term proof

simulation_implies_church_turing

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 140theorem simulation_implies_church_turing (h : simulation_hypothesis_from_ledger) :
 141    church_turing_physics_from_ledger := h

proof body

Term-mode proof.

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

depends on (15)

Lean names referenced from this declaration's body.