Simulation Invariance and Its Limits in Higher-Topos Computability
Anonymous. Version 1.0, 31 October 2026.
Abstract
We formalize Turing and lambda computation inside an explicit presheaf infinity topos and investigate whether effective semantics identifies real and simulated algorithms. The unrestricted claim is false: a computable provenance bit separates implementations with identical behavior. We prove an exact replacement. Faithful simulation preserves every predicate descending to the selected computational semantics, and descent is equivalent to invariance on the semantic kernel pair. Type-valued observations are transported coherently along semantic identifications, while arbitrary higher data need not be equivalent. Countermodels distinguish provenance, cost, and group actions. A relative Rice theorem separates semantic definability from uniform decidability. The contribution is an assumption-explicit synthesis and a sharp boundary for simulation invariance, not a new computability theorem or a proof that physical reality is a simulation.
Keywords: computability; lambda calculus; infinity topos; effective descent; realizability; simulation.
1. The claim and its quantifiers
Three statements must be distinguished: a formalism can represent every computation in a class; an adequate simulator preserves a selected behavior; every formal predicate is invariant under simulation. The last statement does not follow from the first two. It requires that the predicate disregard every distinction discarded by the selected semantics.
Our conclusion has the precise form
$$q(p)=q(\operatorname{sim}(p))\quad\Longrightarrow\quad D(q(p))\simeq D(q(\operatorname{sim}(p))),$$
where $q$ records behavior and $D$ is a predicate or family on behaviors. The premise is an adequacy theorem, not a consequence of naming one process a simulation. We characterize when a predicate on implementations factors through $q$ and show why arbitrary definitions of reality and simulation need not do so.
We use classical external mathematics and intuitionistic internal descent proofs. The foundations are standard [1-9]; no novelty or proof-assistant verification is claimed for them.
2. Effective universal interpretation
Definition 2.1. Fix an acceptable numbering $(\varphi_e)_{e\in\mathbb N}$ of unary partial recursive functions, a universal partial recursive evaluator $U(e,x)=\varphi_e(x)$, and a total computable specialization map $s$ satisfying
$$\varphi_{s(a,z)}(x)\simeq_{\rm par}\varphi_a(\langle z,x\rangle).$$
Partial equality means both sides diverge or both converge to the same value. Malformed encodings denote a fixed divergent program. Acceptability includes uniform specialization, not merely enumeration [3].
Theorem 2.2 (universal simulation). There is a total computable map $\operatorname{sim}:\mathbb N\to\mathbb N$ such that $\varphi_{\operatorname{sim}(e)}(x)\simeq_{\rm par}\varphi_e(x)$ for every $e,x$.
Proof. Choose an index $u$ that evaluates $U(e,x)$ on input $\langle e,x\rangle$ and set $\operatorname{sim}(e)=s(u,e)$. Specialization gives
$$\varphi_{\operatorname{sim}(e)}(x)\simeq_{\rm par}\varphi_u(\langle e,x\rangle)\simeq_{\rm par}U(e,x)\simeq_{\rm par}\varphi_e(x).$$
The interpreter halts exactly when the interpreted computation does, with the same result. Induction gives preservation by every finite iterate $\operatorname{sim}^k$. This proves nothing about an infinite tower or exact running time. $\square$
For lambda computation, fix deterministic weak call-by-value untyped terms with finite codes, effective substitution, and a fixed effective numeric input/output protocol. Terms are generated by variables, application, and abstraction; values are abstractions; reduction evaluates function and argument before contracting a beta redex and does not reduce under an abstraction. Natural numbers use a fixed Scott encoding. A noncanonical output can be assigned divergence by the numeric observation protocol.
We use the established effective translations between this numeric lambda presentation and Turing machines as an adequacy input. There are total computable $c,d$ with
$$\lambda_{c(e)}(x)\simeq_{\rm par}\varphi_e(x),\qquad \varphi_{d(a)}(x)\simeq_{\rm par}\lambda_a(x).$$
Mutual simulation with time bounds has been mechanized by Forster, Kunze, Smolka, and Wuttke [4]. We use only its computational adequacy, not its resource bounds, and do not claim a new compiler implementation here.
Proposition 2.3. The translations induce inverse maps between the two sets of program codes modulo equality of partial numeric behavior.
Proof. Adequacy makes the quotient maps well-defined and identifies the composites $dc$ and $cd$ with the identity modulo behavior. $\square$
Numeric behavioral equality need not be beta convertibility, equality of histories, or equivalence in reflective contexts.
3. A concrete higher ambient model
Let $\mathsf{Fin}$ be a small skeleton of finite sets and functions and put
$$\mathcal X=\operatorname{Fun}(\mathsf{Fin}^{\rm op},\mathcal S),$$
where $\mathcal S$ is the infinity category of spaces. This is a presheaf infinity topos [5]. The indexing category has effective finite codes and computable composition. Write $\Delta$ for constant presheaves, $N=\Delta\mathbb N$ for the natural-numbers object, and $P=N$ for codes. Nontruncated spaces such as $\Delta BG$ supply genuinely higher objects.
Choose a primitive recursive trace-verification predicate $T(e,x,y,t)$: the finite object coded by $t$ is a valid halting computation of $e$ on $x$ with output $y$. Internally set
$$G(e,x,y)=\left\|\sum_{t:N}T(e,x,y,t)\right\|_{-1}.$$
The truncation retains existence rather than a chosen trace. Determinism gives $G(e,x,y)\wedge G(e,x,z)\Rightarrow y=z$. This defines partial computation; it does not assert a total universal evaluator $N\times N\to N$.
Let $B\hookrightarrow\Omega^{N\times N}$ be the object of single-valued relations. Its elements need not all be computable. The graph map factors as
$$P\xrightarrow{q} A\hookrightarrow B,\qquad A=\operatorname{im}(G).$$
The categorical map $q$ is an effective epimorphism; this means it realizes its Cech nerve, not that equality in $A$ is algorithmically decidable. The object $A$ consists of behaviors locally represented by the chosen programs.
Proposition 3.1. In this model, $q\operatorname{sim}=q$, and the Turing and lambda presentations have the same behavioral image.
Proof. The numerical simulation identities give equal halting relations. Applying $\Delta$ gives equal constant relations and thus equal classifying maps into $B$. Their factors into $A$ agree because $A\hookrightarrow B$ is monic. The two compiler identities give the same conclusion. $\square$
This construction does not make every morphism computable: any set function $\mathbb N\to\mathbb N$ induces a transformation $\Delta\mathbb N\to\Delta\mathbb N$. We specify a computably presented semantics inside a higher topos. We do not claim a canonical construction called the effective infinity topos. For other interpretations, internal adequacy must be supplied; it is not automatically inherited from externally asserted arithmetic facts.
4. The exact descent theorem
Let $q:E\twoheadrightarrow A$ be any effective epimorphism in any infinity topos. Put $R=E\times_AE$ with projections $r_0,r_1$. Equalities are homotopical and range over generalized elements over every base, not only global points.
A predicate $Q\hookrightarrow E$ is behavioral if $Q=q^*\overline Q$ for a subobject $\overline Q\hookrightarrow A$. It is saturated if $r_0^*Q=r_1^*Q$ as subobjects of $R$.
Theorem 4.1 (exact predicate descent). Pullback gives a poset isomorphism
$$\operatorname{Sub}(A)\cong\{Q\in\operatorname{Sub}(E):r_0^*Q=r_1^*Q\}.$$
Thus dependence solely on the selected behavior is equivalent to invariance under every behaviorally equivalent pair of implementations. Descent is unique.
Proof. A pullback predicate is saturated because $qr_0=qr_1$. Conversely define
$$\overline Q(a)=\left\|\sum_{e:E}(q(e)=a)\times Q(e)\right\|_{-1}.$$
Given $Q(e_0)$, use $e_0$ and reflexivity to prove $\overline Q(q(e_0))$. Conversely, eliminate the displayed truncation into the proposition $Q(e_0)$. A witness $(e,p,u)$ determines an element of $E\times_AE$; saturation carries $u:Q(e)$ to $Q(e_0)$. Hence $q^*\overline Q=Q$.
If $q^*S=q^*S'$, effective epimorphy gives $\|\sum_e q(e)=a\|_{-1}$ for each $a$. Eliminate this truncation into the proposition $S(a)\leftrightarrow S'(a)$ and use the equality over $e$. Thus $S=S'$. The implication version proves order reflection. No global selection of representatives is used. $\square$
Corollary 4.2. If $f,g:C\to E$ satisfy $qf=qg$, then $f^*Q=g^*Q$ for every saturated $Q$. In particular, $q\operatorname{sim}=q$ implies $Q(e)\leftrightarrow Q(\operatorname{sim}(e))$.
Proof. Write $Q=q^*\overline Q$ and pull back along the equal composites. $\square$
Invariance under one chosen simulator is weaker than saturation under the whole kernel pair. Constancy along the simulator's orbits alone is insufficient.
Two invariant predicates also need not equal each other. If $R=q^*\overline R$ and $S=q^*\overline S$, then $R=S$ exactly when $\overline R=\overline S$. For example, “returns zero on input zero” and “returns one on input zero” are distinct behavioral predicates. Preservation of each definition under simulation does not equate different definitions.
5. Higher observations and coherence
Since $\Omega$ and $\mathbf2=1+1$ are 0-truncated,
$$\operatorname{Map}(A,\Omega)\simeq\operatorname{Map}(\tau_{\leq0}A,\Omega),$$
and similarly for $\mathbf2$. Propositional observation does not detect arbitrary higher homotopy, but the behavior object can still retain it.
Proposition 5.1. A family $F\to A$ transports an identification $a=a'$ into an equivalence $F_a\simeq F_{a'}$, coherently with composition and higher identifications. Consequently, an adequate simulation preserves every structured observation supplied as a family over $A$.
Proof. Pullback along identified maps yields naturally equivalent fibers; functorial pullback supplies all coherences. Internally this is path transport, reversed by transport along the inverse path. $\square$
Univalence can express this through a universe, but cannot produce an equivalence solely because both objects have computable presentations [6,7,10]. For an arbitrary family on $E$ to descend, one needs coherent descent data on the whole Cech nerve:
$$\mathcal X_{/A}\simeq\lim_{[n]\in\Delta}\mathcal X_{/E_n},\qquad E_n=E\times_A\cdots\times_AE.$$
For subobjects the compatibility data are unique when they exist. For general types they are not.
Example 5.2. Let $G=C_2$. The map $*\to BG$ is an effective epimorphism in spaces. Discrete families over $BG$ are $G$-sets. The two-point set with trivial action and the two-point set with swapping action have the same underlying fiber after pullback to $*$. They are not equivalent over $BG$: an equivariant bijection would send a fixed point to a fixed point, and the swapping action has none. The same example exists as constant higher data in the presheaf model. Moreover, $*$ and $BG$ have the same connected-component set but different fundamental groups. Higher semantics can preserve distinctions; it does not automatically erase them.
6. Explicit effective countermodels
Set $I=P\times\mathbf2$ with semantic map $d(e,b)=q(e)$. Define
$$\operatorname{direct}(e)=(e,0),\qquad \operatorname{virtual}(e)=(\operatorname{sim}(e),1),$$
$$\operatorname{Real}(e,b)\equiv(b=0),\qquad \operatorname{Simulated}(e,b)\equiv(b=1).$$
The labels declare provenance; a claim about every formal definition must cover them.
Theorem 6.1. Direct and virtual implementations have equal $d$-behavior, but are separated by a total computable Boolean observation. Real and Simulated are distinct complementary inhabited subobjects.
Proof. Adequacy gives $q(e)=q(\operatorname{sim}(e))$. The second projection returns 0 on the direct implementation and 1 on the virtual implementation. Coproduct disjointness gives $0\ne1$ in this nondegenerate model. Both fibers have witnesses. The predicates are not saturated and therefore do not descend. $\square$
The two fibers are isomorphic as bare objects to $P$, but not equal as classified subobjects of $I$. If “equivalent” means only equivalent as bare types, take three implementations with the same constant-zero behavior, designate one Real and two Simulated. Both predicates are decidable, but their fibers have cardinalities one and two.
An independent counterexample records time: a native machine returns zero in one transition; a fetch/decode/execute interpreter returns zero in three. They agree on output and differ on the effective observation (output, step count). Polynomial overhead is not equality of exact costs. Replacing $q$ by richer semantics $\widetilde q$ requires a fresh adequacy argument.
More radically, a schema identifying all predicates on an inhabited implementation object equates the constantly true and constantly false predicates. Pullback along a point forces $0\simeq1$. Such a schema is inconsistent with a nondegenerate topos.
7. Definability is not decidability
Theorem 7.1 (relative Rice obstruction). If $b:\mathbb N\to\{0,1\}$ is total computable and satisfies
$$\varphi_e\simeq_{\rm par}\varphi_f\Longrightarrow b(e)=b(f),$$
then $b$ is constant.
Proof. Suppose not. Complement $b$ if necessary so that it is zero on the nowhere-defined function, and choose $a$ with $b(a)=1$. Uniformly in $e$, construct a program $h_e(x)$ that first simulates $\varphi_e(e)$ and, if it halts, runs $\varphi_a(x)$. Specialization gives a total index map $k(e)$ for $h_e$. When $\varphi_e(e)$ diverges, $h_e$ is nowhere defined; when it halts, $h_e=\varphi_a$. Thus $b(k(e))$ decides the diagonal halting set, a contradiction. This is the classical Rice argument [8]. $\square$
This applies to a Boolean semantic classifier when its pullback to codes is total computable. It does not make all predicates constant. The extensional proposition
$$H(e)=\left\|\sum_{y,t:N}T(e,0,y,t)\right\|_{-1}$$
is nontrivial and definable but has no total computable characteristic function. General subobjects are classified by $\Omega$; decidable ones have Boolean characteristic maps. Conflating these notions would invalidate the argument.
The corresponding realizability calculation is concrete. In the standard category of assemblies over Kleene application, let $\mathsf{PC}$ have partial recursive functions as elements and $E(f)=\{e:\varphi_e=f\}$ as their nonempty realizer sets. A morphism $\mathsf{PC}\to\mathbf2$ has a tracker defined on every realizer. Every natural number is an index, so that tracker is total and extensional; Theorem 7.1 makes the underlying classifier constant. The code assembly paired with a Boolean tag nevertheless has a nonconstant tracked projection. Via the fully faithful assembly embedding, the same distinction is present in Hyland's effective topos [9].
This does not identify that elementary topos with the 0-truncation of our presheaf infinity topos. Nor do we claim that simplicial objects in any elementary topos automatically form a Grothendieck infinity topos. A specific higher-realizability model needs its own construction and adequacy results.
8. Scope and reproducibility
The descent theorem is valid in every infinity topos. The computation theorem requires an acceptable universal presentation or specified adequate translations. Restricted resource-bounded models need not support a simulator for their own class within the same budget. Oracle-relative presentations require relative computability. For interactive, probabilistic, concurrent, or reflective programs, partial numeric graphs can be too coarse: trace, contextual, or distributional semantics and their own adequacy proofs are required. Mutual representability does not automatically prove full abstraction for arbitrary contexts.
The companion PDF and LaTeX source give the extended exposition. A dependency-free Python artifact separately implements native and interpreted transitions: 100 terminating checks, 25 bounded runs without observed halts, and 630 cycle-boundary comparisons pass. Exhaustive checks find four saturated predicates among sixteen and no equivariant bijection between the two $C_2$-actions.
These finite checks do not prove general correctness, decide nontermination, or kernel-check the categorical theorems.
9. Conclusion and disclosure
A faithful interpreter is itself a computation and realizes the source algorithm's selected behavior. No predicate determined solely by that behavior can label one execution real and the other simulated. Provenance, cost, and other retained structure can distinguish them because they are additional information. Even two invariant predicates need not be the same predicate.
Claims about physical reality require a separately justified interpretation relating formal systems to physical observations, interventions, and resources. Computability, descent, and univalence alone provide no such interpretation. The proved statement is observation-relative simulation invariance, not universal equivalence of arbitrary definitions of reality and simulation.
Disclosure: Anonymous. Generative AI assisted with drafting, analysis, references, and examples. No affiliation, independent review, or proof-assistant verification is claimed. This is a prepared manuscript, not a publication receipt.
References
1. A. Church. “An unsolvable problem of elementary number theory.” American Journal of Mathematics 58(2), 345-363 (1936). Full text. 2. A. M. Turing. “On computable numbers, with an application to the Entscheidungsproblem.” Proceedings of the London Mathematical Society s2-42(1), 230-265 (1937; received 1936). DOI. 3. H. Rogers, Jr. Theory of Recursive Functions and Effective Computability. MIT Press, 1987 reprint of 1967 edition. Publisher. 4. Y. Forster, F. Kunze, G. Smolka, and M. Wuttke. “A mechanised proof of the time invariance thesis for the weak call-by-value lambda-calculus.” ITP 2021, LIPIcs 193, 19:1-19:20. DOI. 5. J. Lurie. Higher Topos Theory. Annals of Mathematics Studies 170 (2009), Chapters 5-6. Author's text. 6. M. Shulman. “All (infinity,1)-toposes have strict univalent universes” (2019). arXiv:1904.07004. 7. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics (2013), Chapters 2, 3, 6. Book. 8. H. G. Rice. “Classes of recursively enumerable sets and their decision problems.” Transactions of the AMS 74(2), 358-366 (1953). Full text. 9. J. M. E. Hyland. “The effective topos.” In The L. E. J. Brouwer Centenary Symposium, 165-216 (1982). Author's retypeset text. 10. E. Riehl. “On the infinity-topos semantics of homotopy type theory.” Bulletin of the London Mathematical Society (2024). DOI; arXiv:2212.06937.