The Enter Calculus: A Computational Semantics for Quantum Measurement, with a Derived Born Rule and a Typed Resolution of the Frauchiger–Renner Paradox
We introduce the Enter calculus, a linear quantum lambda calculus in which measurement is represented by an explicit operation, Enter, that produces a classical record. Runtime qubit names refer to factors of a shared quantum state, allowing the operational semantics to represent entanglement without assigning separate state vectors to individual terms. We prove type preservation, progress, strong normalization, semantic no-cloning, circuit adequacy, internal no-signaling, and confluence up to outcome distributions. We then replace the probabilistic measurement rule by an abstract evaluation strategy. Composability, no-signaling, nullity, continuity, and a record-creation axiom uniquely determine Born probabilities and projective state updates. The role of the record axiom is isolated using structural results from a companion analysis of the corresponding record-free functional equation. Finally, we introduce a typed Suspendconstruct that compiles an agent’s protocol into coherent laboratory dynamics. This reflection mechanism supports a formal reconstruction of the Frauchiger–Renner protocol. The contradictory certainty chain is blocked because a record reading and an incompatible interference measurement require the same linear resources and therefore cannot occur in one well-typed observational context. The resulting account treats measurement records as perspective-bound while retaining single-history stochastic semantics for unsuspended agents.Keywords: quantum measurement; quantum lambda calculus; Born rule; linear types; Wigner’s friend; Frauchiger–Renner paradox; no-signaling; quantum programming languages
We introduce the Enter calculus, a linear quantum lambda calculus in which measurement is represented by an explicit operation, Enter, that produces a classical record. Runtime qubit names refer to factors of a shared quantum state, allowing the operational semantics to represent entanglement without assigning separate state vectors to individual terms. We prove type preservation, progress, strong normalization, semantic no-cloning, circuit adequacy, internal no-signaling, and confluence up to outcome distributions. We then replace the probabilistic measurement rule by an abstract evaluation strategy. Composability, no-signaling, nullity, continuity, and a record-creation axiom uniquely determine Born probabilities and projective state updates. The role of the record axiom is isolated using structural results from a companion analysis of the corresponding record-free functional equation. Finally, we introduce a typed Suspendconstruct that compiles an agent’s protocol into coherent laboratory dynamics. This reflection mechanism supports a formal reconstruction of the Frauchiger–Renner protocol. The contradictory certainty chain is blocked because a record reading and an incompatible interference measurement require the same linear resources and therefore cannot occur in one well-typed observational context. The resulting account treats measurement records as perspective-bound while retaining single-history stochastic semantics for unsuspended agents.Keywords: quantum measurement; quantum lambda calculus; Born rule; linear types; Wigner’s friend; Frauchiger–Renner paradox; no-signaling; quantum programming languages
The Enter calculus is a linear quantum lambda calculus in which runtime qubit names refer to factors of a shared quantum state, and measurement is represented by an explicit operation, Enter, that consumes quantum resources and returns classical records. This paper gives a unified formal development of the calculus. The core language satisfies type preservation, progress, strong normalization, semantic no-cloning, adequacy for finite quantum circuits, confluence up to terminal distributions, and internal no-signaling. The Born probabilities are then removed from the operational rule and replaced by an abstract evaluation strategy. Five operational requirements are imposed: composability, no-signaling, nullity, continuity, and observational equivalence between direct evaluation and coherent record creation followed by delayed readout. The central result is that diagonal anchoring is not an additional axiom; it follows from the first four requirements through a decohered fine-graining construction in which a within-block index is exported to an additional register. The record principle then yields the Born rule for arbitrary coherent states, and comparison with all later experiments determines the projective state update. The development includes quantitative stability estimates, mixed-state and adaptive formulations, rotated projective measurements, POVM outcome laws, and an affine extension for quantum instruments. A single-level reflection operation compiles an agent’s protocol into coherent laboratory dynamics. A compatibility theorem for sharp measurement contexts then isolates the obstruction in the Frauchiger–Renner certainty chain. Finally, a static record-free functional equation is classified by Walsh-parity slack fields, and its remaining positivity problem is distinguished from the operational Born theorem.
The Enter calculus is a linear quantum programming language in which measurement is represented by an explicit operation that consumes quantum resources and returns classical records. This paper studies abstract evaluation strategies for that operation. Five operational requirements are imposed: composability of measurements on disjoint subsystems, no-signaling, nullity of outcomes orthogonal to the state, continuity, and equivalence between immediate evaluation and coherent record creation followed by delayed readout. The main result is that these requirements determine both Born probabilities and projective state updates. The central step is a derivation of diagonal anchoring rather than an assumption of it. No-signaling first implies that a local outcome law depends only on the reduced density operator. Equal-amplitude states with distinct correlated labels are then shown to have uniform outcome laws. A naïve fine-graining argument fails because its refined register retains intra-block coherence. The repaired construction exports a within-block index to an additional register, producing distinct companion states for every refined label. Uniformity and fiber counting then determine all rational diagonal probabilities, while continuity extends the result to the general case. The record principle transfers this result to arbitrary coherent states, and comparison with all later experiments fixes the residual state. The results extend to mixed states, adaptive protocols, rotated projective measurements, POVM outcome laws, and, after adding explicit discard, quantum instruments. A restricted compatibility theorem for sharp contexts is applied to the Frauchiger–Renner protocol. The paper also distinguishes this operational result from the static functional equation studied in a companion work. Keywords: Born rule, quantum measurement, quantum programming languages, linear types, no-signaling, deferred measurement, quantum instruments, Frauchiger–Renner paradox.
Operational reconstructions of quantum theory are usually presented as mathematical arguments. Their assumptions, intermediate constructions, and failure modes are therefore difficult to exercise computationally, especially when the underlying language is resource-sensitive and measurement changes both the state and the available observations.We describe a computational methodology for turning such reconstructions into executable, claim-linked artefacts. The methodology separates a linear quantum language, its operational machine, abstract evaluation strategies, axiom checkers, domain-specific constructions, and falsification procedures. Type-directed generation produces strictly linear terms by inverting the typing rules, while property-based and randomized testing explore preservation, normalization, scheduler independence, no-signaling, and measurement-specific requirements.The methodology is instantiated in the Enter calculus, where runtime qubit names refer to factors of one shared quantum state and Enter consumes quantum names while returning classical records. The case study includes an executable decohered fine-graining construction, the associated four-qubit witness for weights one-third and two-thirds, record-based transfer to coherent states, tests of projective state update, generalized-measurement checks, and a sharp-context analysis of the Frauchiger–Renner protocol.A phase-sensitive non-Born strategy is included as a falsifier rather than merely testing positive examples. The accompanying artefact provides evidence against implementation errors and serves as a tool for finding counterexamples; it is not a machine-checked proof of the universal theorems. The resulting framework provides a reproducible interface between operational reasoning, quantum-program semantics, property-based testing, and computational practice in the foundations of physics.
The Enter calculus [EC] derives the Born rule and projective update from five operational requirements: composability, no-signaling, nullity, continuity, and records. This paper equips the calculus with a strictly linear resource geometry and develops its finite-resource meta-theory as a single coherent framework. An update grammar with four primitive moves makes every cut-indexed causal potential a conservation law, as stated in Theorem E, and derives scalar monotonicity rather than assuming it. A latent-active split turns monogamy of causal change into a typing invariant and reconciles token activation with monotone coarsening, as shown in Theorem F. Resourcerelative admissibility is downward closed along runs, as stated in Lemma 4.2; hence forcing is upward monotone in capacity and the forcing threshold is well defined. The minimal register cost of the decohered fine-graining construction is N_F^0(s, m⃗) = s + ceiling(log₂ M) + ceiling(log₂(max_k m_k)), as proved in Theorem H. The resulting realizable rational net strictly refines the dyadic mesh and improves the rigidity bound at capacity 4 from the vacuous value δ = 1 to δ⋆ = 1/6, as shown in Theorem C⋆. The central new result is a rigidity theorem: a multiplicative functional equation extracted from the sequential cocycle with one qubit of headroom forces every admissible strategy whose update diagonal is Lüders-faithful to agree exactly with the Born strategy on every sub-capacity configuration, for every capacity N ≥ 3, as established in Theorem I. The proof is domain-explicit: a witness state is constructed with specified amplitudes, normalisation, and Lüders weights; the cocycle is derived on its exact open domain of validity; an overlapping-interval argument reduces the relation to a function of the product; and the resulting continuous Pexider equation is solved from first principles. Consequently, all residual finite-capacity freedom is confined to full-capacity configurations and to diagonally unfaithful update slack, as stated in Corollary K. Open Problem 17.2 of [EC] is therefore equivalent to a diagonally unfaithful instance of Open Problem G at capacity 3, as shown in Corollary L, while an LP hierarchy converts the remaining question into a computable limit, as established in Theorem J. An exact Choi-rank ledger assigns costs to geometric instruments and identifies decoherence rate with capacity flux, as shown in Theorem D′. Part II specifies a reproducible computational artifact in the style of the Enter-calculus repository: every theorem is either executed as a derivation or enforced as a runtime invariant, and every open problem is represented by a numerical probe.
We prove an exact domain-of-dependence theorem for quantum program dynamics generated by a strongly normalizing calculus, called the Enter calculus, executed on a discrete substrate under partitioned block schedules of range r. The causal cone of slope r arises from the geometry of these schedules, while the metatheoretic interface—strong normalization, probabilistic confluence, internal no-signaling, records, and affinity, abstractly stated as conditions (E1)–(E6)—ensures that program semantics, including terminal laws, adaptive strategies, and readouts, factor through cone-local data. We establish a one-step domain-of-dependence lemma and an exact cone theorem formulated for readout instruments, prove attainability by an explicit relay schedule showing that the lattice signaling speed is exactly r, and construct a faithful-embedding pair consisting of soundness and simulation under a routing condition for calculus-generated block instruments. We then prove necessity results for transmissive long-range primitives realized as genuine repartitionings with a single exceptional block: such primitives violate the original-metric cone, transfer sectors using explicit resources, and destroy metric-local autonomy despite having identical non-selective quantum marginals. A complementary negative result follows from fidelity monotonicity for completely positive maps: a linear long-range channel violates neither affinity, ensemble indistinguishability relative to the complete operational input, nor semantic no-cloning. Under two explicitly conditional hypotheses—device boost-closure and the two-clause causal-executability axiom (E7), both provable on admissible substrates—bidirectional super-cone devices generate closed causal chains and are therefore excluded, yielding a retiming-stable causal bound; isotropy follows only under additional homogeneity assumptions. Finally, we replace the former informal continuum program with a conditional continuum limit: under explicit geometric, operational, algebraic, and frame-covariance hypotheses (C1)–(C7), the limit satisfies a continuum domain-of-dependence theorem, operational no-signaling, algebraic microcausality, and, when the limiting cone is Euclidean and D is at least 2, frame invariance of the maximal speed via the Alexandrov–Zeeman theorem. The existence of a scaling family satisfying (C1)–(C7) remains open and is isolated in two sharply delimited conjectures.
Quantum mechanics lacks a physical definition of measurement, observer, probability, and experienced time. These notions are instead treated as primitive or interpretation-dependent, leading to persistent foundational problems including the measurement problem, the origin of the Born rule, observer disagreement in Wigner’s Friend scenarios, the arrow of time, and apparent information loss in black hole evaporation. In this work, we show that these problems share a single missing ingredient: the absence of an operational definition of observers as bounded physical systems. We define observers as physically realizable systems capable of forming irreversible internal records under unitary dynamics. Measurement is identified with record formation, probability with record redundancy, experienced time with record accumulation, and irreversibility with computational inaccessibility rather than non-unitarity. Using decoherence and quantum Darwinism, we show that the number of accessible, decoherence-stable records associated with an outcome scales with the squared amplitude, yielding the Born rule from record counting without invoking collapse, subjective probability, or additional axioms. Observer-relative paradoxes dissolve once outcome definiteness is indexed to record formation rather than to the global quantum state. Reconstruction of global quantum information is shown to require exponential resources, rendering measurement and black hole evaporation operationally irreversible despite global unitarity. The resulting framework closes quantum mechanics conceptually by eliminating undefined primitives, without modifying its mathematical structure or introducing new dynamical postulates.