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.
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.
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.
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
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.
The Enter Calculus derives the Born rule and the Lüders update from five operational requirements on evaluation strategies. This manuscript studies the quantitative regime in which those requirements hold only approximately. The analysis identifies the local variables that may legitimately control a per-measurement tolerance, proves a linear residual-state estimate, and shows that outcome maps inherit an almost-Lipschitz modulus without requiring an independent Hölder assumption.The record axiom is separated into three inequivalent scopes: pair, protocol, and controlled. This distinction determines the accumulation law for adaptive protocols. On the Lüders-exact residual class, the optimal adaptive deviation is exactly 1 minus (1 minus epsilon) raised to the mth power. A rotated-residual construction proves that this class is maximal.A noisy Born witness gives the crossover profile 1 minus (1 minus epsilon divided by 2) raised to the mth power. The reflected direct/suspended gap has the closed form: 1 minus epsilon, multiplied by the quantity 1 minus (1 minus epsilon divided by 2) raised to the mth power. This expression is independent of coherent copy multiplicity.A multi-axiom tolerance geometry yields a cube-root transfer into derived anchoring, while credit constraints produce a scaling collapse onto the function F of x, equal to 1 minus e raised to the negative x divided by 2.The accompanying born-rates package verifies the closed forms and falsifies invalid scope promotions, but it does not replace proof. The resulting geometry is governed by three features: the local budget, the scope of the record axiom, and the residual class.
The Enter calculus [EC] derives the Born rule and the 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 metatheory, stating each result at precisely the strength established. An update grammar of four primitive moves makes every cut-indexed causal potential a conservation law, as shown in Theorem E through a case analysis of the grammar, and derives scalar monotonicity rather than assuming it. A latent-active split with fully specified typing rules turns monogamy of causal change into a typing invariant, as established in Theorem F. Resource-relative admissibility, with its quantification made explicit, is downward closed along runs, ensuring that the forcing threshold is well defined. The minimal register cost of the decohered fine-graining construction is computed in closed form in Theorem H, and the resulting realizable rational net improves the capacity-four rigidity mesh from the vacuous value delta equals one to delta star equals one-sixth in Theorem C star. Two rigidity layers are proved unconditionally: boundary rigidity, consisting of monotonicity, antipodal symmetry, the Sandwich and Seal lemmas, and a descent proposition, which holds for every admissible strategy without an update hypothesis; and diagonal-faithful rigidity, established in Theorem I through a fully detailed single-qubit case with an explicit Pexider argument and a multi-qubit induction, forcing the Born rule on every sub-capacity configuration at every capacity N greater than or equal to three. The residual question—whether diagonal-unfaithful update slack can survive at full depth—remains unresolved. Instead, it is reduced in both directions to sharply delimited objects: an effective hierarchy of relaxations whose finite levels upper-bound the residual freedom and make rigidity refutable at a finite level, as shown in Theorem J, without claiming that the limit is attained; and a compensated transport family based on odds-ratio-preserving Plackett transports, for which the two-qubit layer, the record-family seal lift in closed form, and the full-support three-qubit extension on compact sets are proved. This family satisfies every axiom instance generated by record-chain protocols from two-qubit initial configurations at every depth, as established in Theorem M prime. Consequently, no capacity-three rigidity proof can proceed through record chains alone. Full capacity-three admissibility reduces to a single explicitly stated Extension Conjecture; under that conjecture, Open Problem G three has a positive answer and the minimum threshold N zero of one and the pair one, two equals four. Depth-two and depth-three record probes pass at machine precision, and an eta-scan Pareto front reaches the axis numerically. Part II specifies a reproducible artefact in which every major claim is either proved, reduced to a finite check, or implemented as a property test or golden regression over a rich class of instances, with each item’s status—Theorem, conditional result, conjecture, or probe—labelled explicitly.