Beyond the Abstraction Fallacy: Machine-Checked Proofs on Computation, Consciousness, and Self-Contained Reality

Lerchner (2026) argues that computational functionalism commits the “Abstraction Fallacy”: treating computation as an intrinsic physical process when it is in fact a mapmaker- dependent description requiring a prior experiencing agent. His analysis correctly identifies the simulation–instantiation distinction but relies entirely on philosophical argument. This pa- per shows that the core claims admit machine-checked formal proofs and, once proved, extend substantially further. Drawing on the NEMS (No External Model Selection) framework—a formal investigation into the structural limits and necessary properties of any self-contained system, comprising 94 machine-checked papers, 17 Lean 4 proof libraries, and over 100,000 lines of proof code, with zero sorry and zero custom axioms on all load-bearing results—we establish three formally verified results that subsume Lerchner’s philosophical claims: (1) syn- tax cannot exhaust semantics in any diagonally capable reflexive system; (2) the diagonal barrier: record-truth is not computably decidable under self-containment; (3) no-emulation: no total computable function can emulate internal adjudication. We then develop the positive theory that Lerchner’s paper lacks: transputation as a formally necessary non-algorithmic mode of adjudication, with a candidate realization architecture (DSAC); qualia as irreducible semantic ledger content; and the SIAM separation theorems giving a precise structural bound- ary for sentience. The same formal apparatus also derives physics consequences—the Born rule, the Standard Model gauge group, the arrow of time—establishing that the consciousness results and the physics results are structural consequences of one self-containment principle. We also identify and respond to the principal objections likely to be raised against this framework. All load-bearing claims correspond to named, independently verifiable Lean 4 theorems.