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.
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.
We embed the operational semantics of a strongly normalising quantum-programme calculus, the Enter calculus, into a discrete spatial substrate executed under partitioned block schedules of range r, and prove an exact domain-of-dependence theorem for the resulting dynamics. The causal cone of slope r arises from the geometry of the schedules, while the metatheoretic interface—strong normalisation, probabilistic confluence, internal no-signalling, records, and affinity, abstractly stated as (E1)–(E6)—ensures that programme semantics, including terminal laws, adaptive strategies, and readouts, factors through cone-local data. We establish a one-step domain-of-dependence lemma and an exact cone theorem for readout instruments, prove attainability through an explicit relay schedule, and show that the lattice signalling speed is exactly r. We also obtain a faithful-embedding pair for calculus-generated block instruments: soundness, together with simulation under a routing condition. We then prove necessity results for transmissive long-range primitives, realised as genuine repartitionings with a single exceptional block. These results include violation of the original-metric cone, sector transfer using explicit resources, and failure of metric-local autonomy despite identical non-selective quantum marginals. Nevertheless, fidelity monotonicity for completely positive maps shows that a linear long-range channel violates neither affinity, nor 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), which is 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, under explicit geometric, operational, algebraic, and frame-covariance hypotheses (C1)–(C7), the continuum limit satisfies a continuum domain-of-dependence theorem, operational no-signalling, algebraic microcausality, and, when the limiting cone is Euclidean and D ≥ 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.
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 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.
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 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
Relational quantum causal processes formulate finite operational contexts as normal positive functionals on local completely positive maps. Response differences generate an influence algebra, and its central projections define jointly readable Boolean events. We develop this starting point through a sequence of exact and controlled models. Fresh-environment unitary collision circuits produce dephasing-exchange kinetics with an exact charge-center fixed algebra, a uniform finite-step limit at fixed response order, and graph-controlled metastable Markov dynamics. An absorbing-state model exhibits a sharp transition between non-Abelian quantum memory and Boolean records. A reversal-covariant defect dynamics generates a locally finite partial order on a restricted graph family without assuming a Lyapunov time. Conditional on a certified order, a positive additive record measure, compactness, and identifiability, we prove subsequential convergence to a Lorentzian metric-measure space, finite reconstruction bounds, and uniqueness of admissible smooth limits. Complementary finite regulators provide controlled tests of modular-to-boost response, null tomography, same-update variational identities, induced quadratic gravity, and compatible common-refinement limits. These results are exact or controlled within their stated models, but they do not yet constitute a single background-independent microscopic law that jointly generates adjacency, time, volume normalization, dimension, signature, nonlinear Einstein constraints, and quantum matter. We therefore present RQCP-QG as a theorem-indexed framework that separates established mechanisms, conditional compositions, and open assumptions.