simulation-undecidability

A machine-verified refutation of the final inference in Faizal–Krauss–Shabir–Marino, "Consequences of Undecidability in Physics on the Theory of Everything" (J. Holography Appl. Phys. 5(2), 2025; arXiv:2507.22950) — the widely reported "the universe cannot be a simulation" result.

Their chain: Gödel/Tarski/Chaitin undecidability → no fully algorithmic Theory of Everything → any simulation is algorithmic → therefore the universe cannot be a simulation. This repository grants everything up to the last arrow and proves, in Lean 4 over mathlib with zero sorries and zero non-standard axioms, that the last arrow is invalid. Undecidability constrains the completeness of theories. Undecidability of complete truth does not, by itself, imply that a world's evolution or observation stream is uncomputable: a simulator generates observations and never needs to decide truths.

The three theorems

• T1 (Separation) — separation, simulation_exists: every r.e. theory has a computable generator of its complete theorem stream — every theorem emitted, only theorems emitted — even when, as machine-checked (Gödel–Rosser) for the whole relevant class, provability is undecidable and the theory is incomplete. Generating the sentence stream and deciding it come apart.
• T2 (Witness) — univ_computable … worldTruth_not_re: an explicit computable universal world carrying a sound, incomplete r.e. theory about its own machines, whose history contains, for every candidate algorithmic ToE, the certificate refuting it (inside_refutation_refutes). The world induces a bivalent semantic truth set that is undecidable and not even recursively enumerable, without computing its characteristic function, and an explicit sentence true in the world but unprovable (true_but_unprovable).
• T3 (Scope) — fksm_truth_inference_invalid: noncomputability of complete world-truth does not imply noncomputability of world-evolution — the antecedent holds and the consequent fails for one and the same world. The published arrow, rendered per D2/D3 (the rendering is defended in FIDELITY.md), is exactly the hidden premise P* ("if the phenomena can be generated, the theory can be decided"): pstar_iff_inference; P* is false on the entire relevant class (pstar_fails); the countermodel form displayed in the public announcement is fksm_inference_invalid.

Verify it yourself

git clone https://github.com/jrslotkin/simulation-undecidability
cd simulation-undecidability/lean
lake exe cache get   # optional: prebuilt mathlib; skip = ~10 min from-source build
lake build

A successful build certifies the claims directly: it runs a binding axiom audit (#assert_standard_axioms, lean/SimulationRefutation/AxiomAudit.lean) that fails compilation if any of the 39 audited theorems depends on a sorry or any axiom beyond Lean's standard three (propext, Classical.choice, Quot.sound).

Read the statements: lean/SimulationRefutation/{Separation,Witness,Scope}.lean (top of each file), mapped one-to-one to prose in THEOREMS.md. The strawman defense is FIDELITY.md; exact reproduction details and the complete machine-checked-vs-prose ledger are in VERIFICATION.md; the modeling choices are in ASSUMPTIONS.md. Development notes are in LOG.md; TASK.md is the commissioning brief.

Priority and related work

The objection has been made before. The closest prior statements of the thesis formalized here:

• Evan Redden, "Provability vs. Execution: A Comment on 'Consequences of Undecidability in Physics on the Theory of Everything'" (arXiv:2512.11807) — distinguishes epistemic incompleteness (limits on what a formal system can prove) from ontological incompleteness (limits on what can exist or be computed), argues via Turing-complete examples (Conway's Game of Life) that undecidability constrains provability, not execution, and observes that FKSM's conclusion would need evidence of hypercomputation in nature. T1/T3 can be read as a machine-checked proof of Redden's central claim; his hypercomputation burden corresponds to the P* analysis here.
• Micah Blumberg, "Undecidability Does Not Kill Simulation" (SVGN.io) — argues that limits on prediction, certification, and classification have been mistaken for limits on dynamical generation: undecidability constrains what can be decided or proven about a process, not whether the process can run. The same distinction generation_without_decision makes formal; his statement is earlier and informal.

Related published work:

• Aatif Kaisar Khan — a published exchange in the same journal: Khan 2026 (J. Holography Appl. Phys. 6, 126–132) and the FKSM reply 2026 (J. Holography Appl. Phys. 6, 119–124).
• Henry Arellano-Peña, "Timeless Projection and Counterspace: Why 'Undecidability' Does Not Debunk All Notions of Simulation" (preprint) — a different escape route: even granting FKSM a prohibition on stepwise algorithmic computation of all truths, projection-based notions of simulation (phenomena realized from a timeless source, within his counterspace framework) survive the argument. Complementary to the present work: he widens "simulation" beyond the algorithmic, while the theorems here keep the narrow algorithmic sense and show that it survives.

Further published criticism in the same direction: V. Khomyakov ("Reassessment of the Undecidability Argument Against Simulation"); Vopson and Moreno's "category error" remarks in press coverage.

As far as could be determined, no machine-verified refutation existed prior to this one. The contribution is the formal isolation of the hidden premise (P* as a theorem-level equivalence) and the machine-checked proofs, which turn the Redden/Blumberg thesis into a verified theorem and reduce the remaining dispute to a question of definition fidelity. Reports of prior formal work are welcome as issues; the priority claim is limited to this paragraph.

About

Built with Claude Code — the formalization, proofs, and documentation were done by Claude (Anthropic), directed by the repository owner. MIT licensed (LICENSE).