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 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 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.
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 [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.
We study operational strategies, consisting of outcome laws and residual states, assigned to measurements of subsystems of a pure state and required to satisfy five exact axioms: sequential composability, nullity, continuity, equivariance, and records. We then examine what changes when no-signaling is weakened to a quantitative tolerance delta. There are two inequivalent versions: a one-shot tolerance imposed separately for each configuration, and a uniform tolerance required across adaptive procedures of every size. We prove five main results. First, composition obeys a sharp modulus: the error is delta for coarse bipartitions and 2 delta for pairwise compositions, and both bounds are tight. Second, for strategies that factor across tensor products, any uniform delta-no-signaling condition with delta less than 1 already implies exact no-signaling, by Hellinger amplification. Third, constraints based on causality, reliability, or cryptography can impose only an upper limit on delta, never a positive lower limit, because the Born strategy satisfies all of them exactly when delta is zero. Fourth, the exact axioms together with one-shot delta-no-signaling imply quantitative closeness to the Born rule: the total-variation distance is bounded by a function eta sub d of delta that scales as the cube root of Lambda squared d times delta; this yields a signaling bound of at most twice eta sub d and Hausdorff convergence of the admissible strategies to the Born strategy. Finally, we construct an explicit purity-signal strategy satisfying nullity, continuity, equivariance, and records exactly while changing a remote outcome law by precisely epsilon divided by four. Thus, all substantive no-signaling content is carried by sequential composability, leaving a single precisely formulated open problem.
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