Born–Lüders as the unique measurement strategy of a strictly linear quantum λ-calculus A self-contained finite characterization in the Enter calculus

We characterize the destructive computational-basis measurement primitive of a fixed strictly linear quantum lambda calculus. The admissible strategies are state sufficient, have normalized outcome laws, and assign pure conditional residuals to positive-probability branches. The argument separates two logical layers. First, Born probabilities and destructive projective update define a concrete calculus with type safety, a syntactic linear step bound, observational confluence, circuit adequacy, semantic no-cloning, and internal no-signaling. Second, only the measurement transition is left unknown. Composability, no-signaling, nullity, continuity, and a typed record equation are satisfied by the Born strategy and uniquely determine it within the stated class. Two independent finite constructions establish diagonal anchoring without the record equation. Whole-register records then determine coherent outcome laws, composability determines partial readout, and branch-specific continuation tests determine residual rays. We also prove resource-budgeted stability estimates and derive mixed-state, adaptive, and finite-instrument consequences. A static appendix constructs positive non-Born marginal assignments and exhibits their failure of operational nullity. Later record, decoder, instrument, and cutoff interfaces are kept separate from the premises of primitive uniqueness.

The result is conditional on the structural class stated below. It is not a reconstruction of qubit kinematics, an independence theorem for the five requirements, or a proof of record-free uniqueness. It is not a physical Frauchiger–Renner no-go theorem. No field-theoretic instrument, infinite apparatus, microscopic evaporation channel, horizon construction, characteristic quantum coefficient, or energy-uniform channel approximation is derived.

Fix a quantum programming language: its types, allocation, tensor composition, coherent gates, and classical control. Leave only the outcome law and conditional update of a destructive measurement primitive unspecified. Which strategies interpret that primitive while satisfying specified equations between experiments?

The primitive considered here is $\mathsf{Enter}$, destructive computational-basis readout of a finite qubit register. A configuration contains one global pure state. Runtime qubit names are access rights to its tensor factors; they are not individual pure-state assignments. Readout consumes the measured names, returns classical bits, and leaves a state on the surviving factors.

This manuscript gives a self-contained, scope-restricted presentation of the finite Enter-calculus characterization of Cheung EnterCalculus. The central result is Theorem thm:main. Here “Born–Lüders” means projective conditioning followed by removal of the measured factors, not retention of those factors. The distinction between outcome probabilities and state change is essential; the historical projective update is discussed in Lüders' work and its English translation LudersTranslation.

I: specified semantics. The concrete calculus ${\mathsf{EC}}_{\mathrm{Born}}$ has Born probabilities and destructive projective update by definition. Safety, termination, confluence, adequacy, and no-signaling are theorems about that already specified semantics.

II: unknown measurement. A strategy $\mathsf{S}=(\mathsf{P},\mathsf{U})$ replaces only the measurement transition. The structural class fixes the domain of the characterization. The five requirements

are conditions on the unknown strategy.

The two directions are

The first establishes inhabitation; the second establishes uniqueness within the declared class. A concrete Born calculation is not available for an unknown strategy merely because both strategies interpret the same syntax.

No silent quantum deletion is added to the language. Algebraic partial traces used in proofs are not term-level weakening operations.

Quantum lambda calculi with classical control already provide well-developed operational and typing frameworks; the affine calculus of Selinger and Valiron is a representative example SelingerValiron. The present language uses strict, branch-wise linear ownership. Its characterization question concerns a variable measurement transition in a fixed language, rather than type safety alone.

Gleason's theorem concerns measures on Hilbert-space subspaces subject to a different assumption package Gleason. The present proof does not begin with probabilities for all effects or projectors. It characterizes one fixed-basis primitive; other measurements are represented later by programs.

The uniform-correlation argument uses a system/environment permutation mechanism related to envariance arguments ZurekEnvariance. Its premises are stated explicitly as operational requirements. The importance of distinguishing such premises from derived probabilities is emphasized in the analysis of Schlosshauer and Fine SchlosshauerFine. Neither envariance nor a separate noncontextuality axiom is imported as an additional premise.

Finally, the companion manuscripts discussed in Section sec:interfaces concern implementation and observational boundaries. They are not premises of Theorem thm:main.

Types are

Tensor powers are right nested: $A^{\otimes 0}=1$ and $A^{\otimes 1}=A$. The empty tuple is $\ast$. Linear pairing and elimination implement the usual associativity and unit isomorphisms. Tuple notation suppresses these administrative maps, not resource uses.

Terms are

Source variables are $x,y,\dots$. Runtime names $q,r,\dots$ are introduced by allocation. Source programs contain no runtime names. Every finite-register unitary is available as a gate; a dense-gate variant is given in Corollary cor:dense.

We abbreviate $(\lambda x:A.u)t$ by $\mathsf{let}x=t\mathsf{in}u$. Tuple-pattern binders abbreviate iterated linear tuple elimination.

Contexts assign types to distinct source variables and runtime names. Contexts separated in a multiplicative rule are disjoint. There is no structural weakening or contraction.

The conditional is additive: its alternatives use the same context, but only one alternative executes. The bit $1$ selects the then-branch and $0$ the else-branch.

An occurrence selection retains the guard of each conditional and exactly one of its alternatives, recursively. It is a selection in the syntax tree, not a reduction. The set $\mathrm{own}(t)$ consists of the free runtime names of $t$.

If $\Gamma ⊢t:A$, every resource in $\Gamma$ has exactly one free occurrence in every occurrence selection. The free runtime names of $t$ are exactly the runtime names in $\Gamma$, and the two alternatives of a conditional have identical free-runtime-name sets.

Proof. Induct on typing. Multiplicative rules partition contexts. Abstraction removes its bound variable from the free context. For a conditional, the guard uses its own context, and either selected alternative uses the shared alternative context once. The same induction proves equality of the alternatives' name sets.

A resource may therefore appear in both unexecuted alternatives without being duplicated during execution.

Classical copying and deletion are definable:

Their types are $\mathsf{Bit}⊸\mathsf{Bit}\otimes \mathsf{Bit}$ and $\mathsf{Bit}⊸1$. Finite classical functions are definable by finite case analysis.

The type $\mathsf{Q}⊸\mathsf{Q}\otimes \mathsf{Q}$ is inhabited:

has that type. Typing prohibits duplicate ownership, not all terms with a possible cloning type. Universal cloning is excluded semantically in Theorem thm:nocloning. Quantum consumption by an explicit measurement followed by classical deletion is also different from structural quantum weakening.

For a finite live-name set $L$, write

An ordering is chosen for matrices and bit strings. Changing the ordering simultaneously permutes names and tensor factors.

For $S\subseteq L$, let $\overline{S}=L\setminus S$, and define

The projector acts on ${\mathcal{H}}_L$, whereas

removes the measured factors. It satisfies

A configuration is $[\psi ,t]$, where $\psi$ is a unit vector in ${\mathcal{H}}_L$, modulo global phase, and $\mathrm{own}(t)=L$. It is well typed at $A$ if

Allocation extends the name-to-factor ordering by a fresh name; destructive readout restricts it to surviving names.

An entangled name is not assigned an individual pure state. All live names refer to factors of the same vector.

Values are

Left-to-right call-by-value contexts are

They do not enter abstraction bodies, let-bodies, or conditional alternatives.

Administrative root reductions are

They preserve the state and are closed under $E$. Together with allocation and gates,

they form the deterministic transitions.

The specified Born measurement transition is

There is no transition on a zero-weight branch. Measured names are removed. For $S=\varnothing$, the outcome is $\ast$ and the state is unchanged. A zero-qubit gate changes only an irrelevant phase.

The calculus with these transitions is ${\mathsf{EC}}_{\mathrm{Born}}$. Equation (eq:born-rule) is a definition in Layer I.

If

with disjoint contexts, then

In a context consisting only of runtime names, values of types $\mathsf{Q},\mathsf{Bit},1$, tensor, and function are respectively names, bits, $\ast$, pairs, and abstractions.

Proof. Induct on the typing derivation for substitution. A multiplicative rule places $x$ in one premise. In a conditional, $x$ occurs either in the guard context or in the shared alternative context. In the latter case substitute in both alternatives and reuse the same inserted context $\Delta$ in the additive rule. Canonical forms follow from the value grammar and possible final typing rules.

Every deterministic or positive-probability Born transition preserves the type of a well-typed configuration. Every nonvalue well-typed configuration has an enabled transition.

Proof. Administrative preservation follows from substitution. Conditional selection retains the shared alternative resources by Lemma lem:branchwise. Allocation adds one name and one factor. A gate changes neither ownership nor type. Readout removes precisely its argument names and returns a bit tuple of the required type.

For progress, follow the call-by-value typing decomposition until a root operation is reached. Canonical forms supply the required value shape. Gate and readout arguments are tuples of distinct runtime names, or $\ast$ at arity zero. Finally,

provides at least one positive measurement branch.

Define

and

Under the hypotheses of Lemma lem:substitution,

Simultaneous substitutions for disjoint linear resources increase $m$ by at most the sum of the inserted measures.

Proof. Induct on typing, simultaneously proving the multiple-substitution statement. Multiplicative premises receive disjoint substitutions. If substitutions of total measure $a$ enter the shared alternative context, then

Substitutions in the guard are disjoint from these. This proves the conditional case; the other cases are additive.

Every reduction sequence from a well-typed configuration $[\psi ,t]$ has length at most $m(t)$.

Proof. Every root transition decreases $m$ by at least one. Beta reduction and tuple elimination use Lemma lem:measure; conditional selection uses the maximum. Other transitions remove one counted operation. Along an evaluation-context hole the measure is additive, since the hole is never inside a body or unselected alternative. The same decrease therefore holds contextually.

The bound counts primitive syntax operations. A unitary is one node regardless of its matrix dimension or synthesis cost. Since $m(t)$ is bounded by the number of written operation nodes, this is a syntactically linear bound, not a physical complexity claim.

For an output of type ${\mathsf{Bit}}^{\otimes m}\otimes {\mathsf{Q}}^{\otimes k}$, $\mathrm{Obs}[\psi ,t]$ is the terminal law of the classical tuple. The quantum tuple remains returned and owned; this observation does not test its state. Purely classical output is included using the unit isomorphism.

Termination, finite branching, and normalized transitions make these laws well defined.

Liberal contexts permit independent argument evaluation:

They still do not enter bodies or alternatives. A scheduler chooses an enabled redex at every nonterminal configuration. Configurations are identified up to consistent live-name renaming, tensor permutation, and global phase.

Distinct enabled liberal redexes occupy nonnested positions and own disjoint runtime-name sets. Firing either and then the residual of the other gives equal joint weights and equivalent resulting configurations.

Proof. An enabled root redex has no enabled accessible redex inside it: its required arguments are values, and bodies and alternatives are inaccessible. Distinct redexes are therefore nonnested. Their positions are separated by context-splitting rules. Shared additive contexts occur only in inaccessible alternatives.

Disjoint administrative transitions commute. Allocations commute up to fresh-name renaming and commute with operations on existing factors. Disjoint gates commute. A gate commutes with destructive readout on disjoint factors, with the canonical identification of the surviving output space.

For disjoint readouts,

Both orders have joint weight

and, on a positive joint branch, the same normalized residual. Zero joint weights contribute zero in both orders.

All liberal schedulers yield the same terminal observation law for a well-typed ${\mathsf{EC}}_{\mathrm{Born}}$ configuration.

Proof. The termination measure also decreases in liberal contexts. Induct on $m(t)$. If two first choices differ, refine each successor by firing the residual of the other redex. Lemma lem:diamond matches the resulting configurations with equal weights. The induction hypothesis identifies their terminal laws. If the first choices agree, apply induction to their successors.

Joint readout of disjoint $S,T$ and successive readout in either order have the same ordered joint law, with all other names returned.

Proof. Every joint weight equals ${\Vert {M^{S\cup T}}_{\kappa \lambda }\psi \Vert }^2$.

Confluence compares evaluations of one program. Composability compares distinct programs.

A first-order interface has only finite classical and quantum data at input and output. Internal higher-order terms are allowed. For a fixed classical input, the quantum input and output spaces are fixed by the interface.

For a fixed well-typed program with a first-order interface, every complete classical history $h$ determines a linear map $K_h$ from its quantum input space to its returned quantum output space. It is a composition of allocation isometries, gates, wiring permutations, and destructive readout maps. For a pure input $\psi$,

and

Proof. A complete history fixes all classical choices. Administrative reductions determine syntax and wiring but do not inspect the quantum vector. Multiplying the quantum maps along the history gives $K_h$. The successive conditional normalizations cancel in the product of branch probabilities, leaving ${\Vert K_h\psi \Vert }^2$.

For completeness use the finite formal outcome tree, including branches whose weight is zero on a particular input. At a readout,

Allocation is isometric and gates are unitary. Backward induction on the tree proves completeness. All paths have the same output Hilbert space after the canonical identification by the returned tuple.

Every well-typed program with a first-order interface denotes a finite quantum instrument. Conversely, every finite circuit built from the available gates, zero-state allocation, destructive computational-basis readout, and finite classical control has a well-typed implementation with the same instrument.

Proof. For reported output $y$, define

The maps are completely positive and their sum is trace preserving by Lemma lem:path. Unrolling the finite formal evaluation tree gives a finite adaptive circuit.

Conversely, input wires are linear arguments. Fresh wires use $\mathsf{new}$, routing uses pairing and tuple elimination, and operations use gates or $\mathsf{Enter}$. Finite control uses conditionals, $\mathsf{copyBit}$, and $\mathsf{dropBit}$. Every quantum wire is passed to exactly one next operation, explicitly consumed, or returned. Induction through the circuit identifies its path maps.

The CP-map language here is the standard finite-dimensional instrument language; its operator-sum and dilation background is provided by Choi and Stinespring Choi,Stinespring. The adequacy proof itself is included above.

No closed term $c:\mathsf{Q}⊸\mathsf{Q}\otimes \mathsf{Q}$ returns two copies of every pure qubit input.

Proof. By Lemma lem:path, its averaged output map $\Phi$ is linear on density operators. A universal cloner would satisfy

But

Linearity gives two expressions for $\Phi (I/2)$. Their diagonal entries at $|01⟩$ are respectively $0$ and $1/4$, a contradiction.

This is a calculus-level application of semantic no-cloning, rather than an inference from the absence of contraction; compare Wootters and Zurek WoottersZurek.

A bipartite experiment has a state on $A\bigsqcup B$ and two local programs owning disjoint initial name sets. They may allocate locally but exchange neither names nor messages. An admissible interleaving retains each local program's left-to-right order.

Alice's terminal classical law is independent of Bob's local program and of the admissible interleaving.

Proof. Let $K_a$ and $L_b$ be their local path maps, including allocations and returned outputs. Disjoint maps commute with the canonical output identifications. The joint history weight is ${\Vert (K_a\otimes L_b)\psi \Vert }^2$. Consequently

where the second line uses local completeness. Summing histories with the same reported output proves the claim. The calculation is independent of the interleaving.

This concerns unconditioned local records. Conditional dependence on a reported remote outcome is not excluded.

For $k$ source and $k$ target qubits, let $C_k$ be the grouped CNOT unitary

It is a tensor product of CNOTs together with the required linear regrouping maps. At $k=0$, it is the identity.

Let $L=S\bigsqcup B$, $|S|=k$, and suppose

The source term is

Its deferred term is

Here ${\mathsf{new}}^k$ denotes a tuple of $k$ fresh allocations. The continuation consumes the entire register $B$. It may contain allocations, gates, readouts, and classical control, but uses neither source nor record names.

After the stipulated tuple isomorphisms, the source has classical arity $m+k$, while the target has type

Both report the same ordered classical pair $(c,x)$. The target also returns the original source register. Left-to-right evaluation completes $u$ before reading the record.

Every retained source name occurs once in the returned tuple. Thus neither term duplicates a quantum name or silently drops a spectator. In particular, $u=\ast$ is legal only when $B=\varnothing$.

In ${\mathsf{EC}}_{\mathrm{Born}}$,

Proof. Write

For a path $h$ of $u$, let $K_h$ be its path map. The source's joint weight for $h,\kappa$ is ${\Vert K_h{\xi }_{\kappa }\Vert }^2$.

Allocation and copying in the target produce

After path $h$, the unnormalized vector is

Record readout has the same joint weight ${\Vert K_h{\xi }_{\kappa }\Vert }^2$. Sum histories with the same reported continuation output.

The proposition uses the specified Born semantics. The same equation becomes a requirement on unknown strategies below; its two typed terms remain unchanged.

For disjoint $S,T\subseteq L$, put $Z=L\setminus (S\cup T)$. The sequential experiment is

The reverse experiment reads $T$ first but reports the same ordered classical pair. Joint readout of $S\cup T$ likewise returns $Z$. These terms have the same observation interface after linear tuple rearrangement.

A local identity experiment may return its names with a constant classical unit. A remote allocation experiment returns the additional allocated name. Thus ancilla comparisons below do not use quantum weakening.

There are two record scopes:

1. readout instances: $S=L$ and $u=\ast$;

2. continuation instances: $u$ consumes all of $L\setminus S$.

The outcome proof uses only readout instances. The update proof uses

No equation for arbitrary surrounding contexts is assumed.

Only the measurement transition varies. The admissible class has the following properties.

1. Qubit kinematics. For every finite live-name set $L$, states are unit rays in ${\mathcal{H}}_L$, with ordinary tensor composition.

2. Fixed coherent dynamics. All finite-register unitaries and fresh $|0⟩$ allocation act as in Layer I, with their stated linear-algebraic composition and tensor placement.

3. State sufficiency. The outcome law ${{\mathsf{P}}^{\mathsf{S}}}_{\psi }$ and positive-branch residual ray ${{\mathsf{U}}^{\mathsf{S}}}_{\psi }(\kappa )$ depend only on the current global ray and measured register, not on history, apparatus identity, or hidden memory.

4. Normalized laws and pure residuals. ${{\mathsf{P}}^{\mathsf{S}}}_{\psi }$ is a probability distribution on $\{0,1{\}}^S$. Each positive-probability outcome has a unit residual ray on ${\mathcal{H}}_{L\setminus S}$. Values on zero-probability outcomes are not part of the strategy.

5. Permutation equivariance. Consistent relabeling of names, tensor factors, measured positions, and outcome coordinates transports laws and residuals accordingly.

6. Unbounded finite resources. The strategy is defined at every finite size. Experiments may use any finite number of ancillas. Witnesses need not have the size of the system whose law is being characterized.

7. Evaluation convention. Single programs use left-to-right evaluation. Bipartite experiments interleave their local left-to-right executions. General liberal scheduler independence is not assumed.

No closure under silent quantum deletion is included. Arbitrary input rays are admissible configurations, whether or not a restricted gate language can prepare them exactly.

A strategy is a pair $\mathsf{S}=(\mathsf{P},\mathsf{U})$ in the structural class, interpreting readout by

Safety and the step bound use only types, ownership, and normalized branching, so terminal laws also exist for unknown strategies. The concrete diamond, path maps, and no-signaling theorem are not transferred before characterization.

The theory $\mathsf{T}$ consists of:

$(\mathrm{C}{)}^{\star }$: composability.

For disjoint $S,T\subseteq L$, successive readout in either order and joint readout of $S\cup T$ yield the same ordered joint law, with all other names returned. On a positive first branch,

$${{\mathsf{P}}^{\mathsf{S}\cup \mathsf{T}}}_{\psi }(\kappa ,\lambda )={{\mathsf{P}}^{\mathsf{S}}}_{\psi }(\kappa ){{\mathsf{P}}^{\mathsf{T}}}_{{{\mathsf{U}}^{\mathsf{S}}}_{\psi }(\kappa )}(\lambda ).$$

A zero first weight gives zero joint weight. In particular,

$${{\mathsf{P}}^{\mathsf{S}}}_{\psi }={\mathrm{marg}}_S{{\mathsf{P}}^{\mathsf{S}\cup \mathsf{T}}}_{\psi }.$$

Only the classical joint laws, not complete residual instruments, are equated.

$(\mathrm{NS}{)}^{\star }$: no-signaling.

For every bipartition, the terminal classical law of either local program is independent of the other program and of the admissible interleaving. Local programs may allocate, apply gates, read out, use classical control, and return quantum spectators. They exchange neither names nor messages.

$(\mathrm{N}{)}^{\star }$: nullity.

For every $\psi ,S,\kappa$,

$${M^S}_{\kappa }\psi =0⟹{{\mathsf{P}}^{\mathsf{S}}}_{\psi }(\kappa )=0.$$

The experiment reads $S$ and returns its complement. This is a zero-support condition, not a vacuum condition or a Born probability formula.

$(\mathrm{K}{)}^{\star }$: continuity.

At every fixed finite live register and measured subset,

$$[\psi ]⟼{{\mathsf{P}}^{\mathsf{S}}}_{\psi }$$

is continuous from ray space to the finite probability simplex, equivalently in total variation. No continuity of $\mathsf{U}$ is assumed.

$(\mathrm{R}{)}^{\star }$: records.

For every configuration of Definition def:record,

$${\mathrm{Obs}}_{\mathsf{S}}[\psi ,t_{S,u}]={\mathrm{Obs}}_{\mathsf{S}}[\psi ,{\mathrm{defer}}_S(t_{S,u})].$$

The continuation consumes the entire complementary register and does not use the first reported outcome.

Each comparison has an explicit typed experiment. The requirements do not assume probability covariance under arbitrary computational-basis permutations; the needed symmetry is derived below.

Define the Born strategy by

on positive branches.

The Born strategy belongs to the structural class and satisfies $(\mathrm{C}{)}^{\star },(\mathrm{NS}{)}^{\star },(\mathrm{N}{)}^{\star },(\mathrm{K}{)}^{\star },(\mathrm{R}{)}^{\star }$.

Proof. The formulas give normalized laws and pure residual rays, are state sufficient and phase invariant, and are equivariant under consistent name and tensor permutation. They are defined at every finite size with the fixed coherent dynamics and evaluation convention.

Composability is Lemma lem:concrete-C. No-signaling is Theorem thm:internal-ns. A zero destructive component has zero squared norm, proving nullity. Each squared norm is continuous, and there are finitely many outcomes, proving continuity. Proposition prop:concrete-record proves records.

A strategy in Assumption ass:strategy-class satisfies Definition def:requirements if and only if it is the Born strategy. For every finite configuration, measured subset $S$, and outcome $\kappa$,

Whenever this number is positive,

where $\doteq$ denotes equality up to global phase. No residual is specified on a zero-probability branch.

The uniqueness proof occupies Sections sec:locality–sec:born. Its dependencies are:

The anchoring proofs are alternatives. Nullity is not needed for locality. Continuity is used in anchoring, not as an update-continuity premise.

Throughout this and the next two sections, $\mathsf{S}$ is unknown.

Under $(\mathrm{NS}{)}^{\star }$, appending fresh zero-state factors outside $S$ does not change ${{\mathsf{P}}^{\mathsf{S}}}_{\psi }$. Applying a unitary outside $S$ does not change it either.

Proof. Compare a remote allocation-and-return program with a remote identity program, and schedule allocation before local readout. No-signaling equates the local laws. State sufficiency identifies the post-allocation law with the law at the enlarged global state.

For a remote gate, compare its gate-and-return program with the identity program and schedule the gate first.

Under $(\mathrm{NS}{)}^{\star }$, global pure states with the same reduced density operator on $S$ have the same $S$-outcome law.

Proof. Pad the smaller environment by zero-state qubits until environment dimensions agree. Remote invariance leaves the law unchanged; consistent relabeling identifies the environment name sets. If

on its support, the purifications have the forms

with orthonormal environment families. The isometry $f_j\mapsto g_j$ extends to an environment unitary. Apply remote invariance again.

Hence there is a well-defined function

This partial trace is an algebraic construction from the stipulated vector, not a measurement-probability postulate.

Under $(\mathrm{NS}{)}^{\star },(\mathrm{K}{)}^{\star }$, $F_S$ is continuous on the density operators on ${\mathcal{H}}_S$.

Proof. Use the fixed-dimensional purification

Its norm is one and its reduction is $\rho$. Matrix square root is continuous in finite dimension, so this is a continuous choice of vector purification. Apply $(\mathrm{K}{)}^{\star }$ and purification locality.

Assume $(\mathrm{C}{)}^{\star },(\mathrm{NS}{)}^{\star },(\mathrm{N}{)}^{\star }$. If

where the computational strings $k$ are distinct and the computational strings ${\eta }_k$ are distinct, then ${{\mathsf{P}}^{\mathsf{S}}}_{\psi }$ is uniform on $K$.

Proof. A diagonal environment unitary removes the phases without changing the $S$-law. Write

Nullity restricts $\nu$ to $(k,{\eta }_k)$. Composability gives

For a permutation $\pi$ of $K$, extend it to a computational-basis permutation unitary ${\Pi }_{\pi }$ on $S$. Then

The same vector is $W\psi$, where $W$ is an environment unitary sending ${\eta }_k$ to ${\eta }_{{\pi }^{-1}(k)}$. Its $S$-law remains $p$, by invariance under $W$. Its $B$-law remains $q$, by invariance under ${\Pi }_{\pi }$.

For the new pairing, nullity and composability imply

Every permutation preserves $p$, so $p(k)=1/d$.

Probability covariance under arbitrary basis permutations was not assumed. The required equality was derived by comparing two coherent implementations of the same transformed vector.

Diagonal anchoring is the conclusion

It is not a separate requirement.

Assume $(\mathrm{C}{)}^{\star },(\mathrm{N}{)}^{\star }$ and (S5). For

the first-qubit law is $(1/3,2/3)$, and the first-qubit reduction is $\mathrm{diag}(1/3,2/3)$.

Proof. Nullity restricts the full law to the displayed strings. Tensor-factor permutations preserve $\Omega$ and act transitively on its support. Equivariance forces equal weights, hence $1/3$ each. Composability gives the first-coordinate marginal. The accompanying last-two-qubit strings are distinct, so the first-qubit reduction has no off-diagonal entry and has the stated diagonal.

This example illustrates the mechanism; it does not by itself establish arbitrary diagonal anchoring.

Assume $(\mathrm{C}{)}^{\star },(\mathrm{NS}{)}^{\star },(\mathrm{N}{)}^{\star },(\mathrm{K}{)}^{\star }$ and (S5). Then diagonal anchoring holds.

Proof. Let $S$ have $n$ qubits. First take a rational diagonal state

Zero-weight labels are omitted.

Take $M$ blocks of $n$ qubits. Let $\mathcal{A}$ consist of sequences $(k_1,\dots ,k_M)$ containing exactly $m_k$ copies of each $k$, and put

Block permutations are tensor-factor permutations. They preserve this vector and act transitively on $\mathcal{A}$. Nullity and equivariance force a uniform full law.

Composability gives the first-block marginal

since

The first-block reduction is exactly ${\rho }_S$. Completions with different first labels have different remaining multisets, hence disjoint computational supports; all off-diagonal first-block entries vanish. The diagonal entries are the same counting ratios.

Locality transfers the law to every purification of ${\rho }_S$. Rational diagonal states are dense, so reduced-state continuity proves the result for all diagonal states. The empty register has a unique outcome.

This witness uses $nM$ qubits. Its resource size is finite but not uniformly bounded in the rational denominator.

For disjoint label sets $R_k$, $|R_k|=m_k$, the vector

has the desired reduction on $S$. However,

Coherences remain within each block. Distinct refined labels $r$ have repeated companions $k(r)$; Theorem thm:uniformity therefore does not apply to the $E^{\prime }$-readout.

A further computational label distinguishes those companions. This chooses another purification of the same ${\rho }_S$; it does not claim that a remote unitary decoheres a fixed reduced state.

Assume $(\mathrm{C}{)}^{\star },(\mathrm{NS}{)}^{\star },(\mathrm{N}{)}^{\star },(\mathrm{K}{)}^{\star }$. Then diagonal anchoring holds.

Proof. Use the rational weights above and set

Choose disjoint $R_k\subseteq \{0,1{\}}^a$, $|R_k|=m_k$, and injections

Define

Its reduction on $S$ is ${\rho }_S$.

With $E^{\prime }$ written first, each $r$ has companion $(k(r),e_{k(r)}(r))$. These companions are distinct: different blocks have different $k$, and each $e_k$ is injective. Uniform correlations therefore give

on the used labels.

Let $\nu ={{\mathsf{P}}^{\mathsf{S}\cup {\mathsf{E}}^{\prime }}}_{\Phi }$. Nullity restricts its support to $(k(r),r)$. Composability makes its $E^{\prime }$-marginal uniform. Each $r$ has only one allowed companion, so

The $S$-marginal is $m_k/M$. Locality transfers this law to every purification of ${\rho }_S$, and continuity supplies arbitrary diagonal weights.

The witness uses

qubits. For weights $(1/3,2/3)$, one choice is

The three-qubit symmetry witness is smaller for that particular law.

The numerical fine-graining argument does not use (S5) as a probability-symmetry premise. The structural class still contains (S5); no independence theorem for the complete assumption package is claimed.

Assume diagonal anchoring, $(\mathrm{C}{)}^{\star }$, and the readout instances of $(\mathrm{R}{)}^{\star }$. Then, for every finite configuration and $S\subseteq L$,

Proof. First let $S=L$. The source

is well typed because no complementary quantum names remain.

Write $\psi ={\sum }_j{a}_j|j{⟩}_L$. Before record readout, the deferred program has vector

Its record reduction is

Diagonal anchoring gives record law $|a_j{|}^2$. The readout record equation identifies this with ${{\mathsf{P}}^{\mathsf{L}}}_{\psi }(j)$.

For a proper subset, composability gives

No partial-register record test with omitted spectators is used.

Assume the Born outcome law, $(\mathrm{C}{)}^{\star }$, and the continuation instances of $(\mathrm{R}{)}^{\star }$. If

then

Proof. Fix a positive branch $\kappa$. Choose unit representatives

If $B=\varnothing$, its Hilbert space is one dimensional and the claim is immediate.

For a unitary $V$ on $B$, use

By the unknown strategy's transition rule and state sufficiency, the joint source weight for $(\lambda ,\kappa )$ is

This does not use a Born update.

The deferred vector after copying and applying $V$, before either readout, is

The target reads $B$, then $R$, and returns $S$. Composability equates its joint law to joint $B\cup R$ readout. The established Born outcome law gives joint weight

Records therefore imply

Using the established outcome law on the left,

for every $V,\lambda$.

Choose $V{\phi }_{\kappa }=|0^{|B|}⟩$. Then