Physics theoremStatement: AI-adaptedProof: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Local instruments and no-signalling: operations on one factor do not change the other factor's local statistics

Physical scope

The declared local instruments of one factor of a composite of two distinguishable subsystems: a declared finite or countable instrument on one factor leaves the reduced preparation, and hence every local outcome law, of the other factor unchanged once its classical record is discarded; conditioning on the record displays the correlation through the conditional reduced preparations, whose probability-weighted average is the original reduced preparation. The statement is a conditional consequence of the framework's measurement readings and the cited mathematics; it asserts no relativistic causality principle, no disturbance of the other factor by any particular apparatus, no apparatus realization and no empirical fact.

Statement

Adopt the framework's composition and measurement readings for a declared composite of two distinguishable subsystems $A, B$ with assigned spaces $H, K$ (Composite systems of the framework: product bases, local readouts, local effects and local instruments, Declared ideal measurements and instruments of the framework, Reduced preparations of a declared composite: the subsystem states of the framework), and assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice), as required by the local sharp-readout law used below. Let $ρ \in D (H \hat{\otimes} K)$ be a preparation of the declared composite with reduced preparations $ρ_{A} = {Tr}_{K} ρ$ , $ρ_{B} = {Tr}_{H} ρ$ , and let $(M_{a, r})_{\begin{array}{c} a \in A_{0} \\ r \in R_{a} \end{array}}$ be a declared finite or countable instrument of subsystem $B$ , normalized: $\sum_{a, r} M_{a, r}^{*} M_{a, r} = I_{K}$ in the strong sense, with effects $F_{a} : = \sum_{r} M_{a, r}^{*} M_{a, r}$ and outcome probabilities $p_{a} = tr (ρ_{B} F_{a})$ . Then:

(a) The local extension. The family $(I_{H} \otimes M_{a, r})_{\begin{array}{c} a \in A_{0} \\ r \in R_{a} \end{array}}$ is a declared finite or countable instrument of the declared composite, with outcome effects $F_{a}^{l o c} = I_{H} \otimes F_{a}$ , outcome probabilities $p_{a} = tr (ρ F_{a}^{l o c})$ , and conditional states $ρ_{a} : = \frac{1}{p_{a}} \sum_{r} (I_{H} \otimes M_{a, r}) ρ (I_{H} \otimes M_{a, r})^{*} (p_{a} > 0) .$

(b) No-signalling. The discarded-outcome state $Φ (ρ) : = \sum_{a, r} (I_{H} \otimes M_{a, r}) ρ (I_{H} \otimes M_{a, r})^{*}$ is a preparation of the composite, its reduced preparation on $A$ is unchanged, ${Tr}_{K} Φ (ρ) = {Tr}_{K} ρ = ρ_{A},$ and consequently every local outcome law of subsystem $A$ is unchanged: $μ_{Φ (ρ)}^{A^{l o c}} = μ_{ρ}^{A^{l o c}} for every assigned sharp observable (A, u_{A}) of A .$ The same holds with the roles of $A$ and $B$ exchanged.

(c) Conditional reductions. If $p_{a} > 0$ , the conditional state $ρ_{a}$ has reduced preparation $(ρ_{a})_{A} = {Tr}_{K} ρ_{a}$ on $A$ , and $\sum_{a : p_{a} > 0} p_{a} (ρ_{a})_{A} = ρ_{A};$ the conditional reduced preparations $(ρ_{a})_{A}$ may differ from $ρ_{A}$ , and the recorded outcome $a$ is the classical datum needed to select them.

(d) Scope. Clauses (a)-(c) are conditional consequences of P1, P2 and P3 in the stated readings and of the cited mathematics; they concern declared instruments of the declared composite. They assert no relativistic causality principle, no claim that a particular apparatus realizes the declared instrument, no disturbance of the other factor by any concrete device and no empirical fact.

Facts & Assumptions

Given: The declared composite with assigned spaces $H, K$ ; a preparation $ρ$ ; reduced preparations $ρ_{A}, ρ_{B}$ ; a declared finite or countable instrument $(M_{a, r})$ of subsystem $B$ with effects $F_{a}$ ; the Axiom of Countable Choice and the Axiom of Choice.

[F1]

Local extension of an instrument. For a declared finite or countable instrument $(M_{a, r})$ of subsystem $B$ the family $(I_{H} \otimes M_{a, r})$ is a declared instrument of the declared composite, with effects $I_{H} \otimes F_{a}$ and conditional updates as displayed; this is part of clause (e) of Composite systems of the framework: product bases, local readouts, local effects and local instruments (Bounded tensor maps: extension, norm estimate, adjoint and commutation, Local PVM extension: tensoring a projection-valued measure with the identity clause (c)).

[F2]

Declared instrument reading and discarded map. Apply clause (d) of Declared ideal measurements and instruments of the framework on the composite space to the extended family of [F1]. Its effects are $F_{a}^{l o c} = I_{H} \otimes F_{a}$ , its probabilities are $p_{a} = tr (ρ F_{a}^{l o c})$ , and its conditional states are $\sum_{r} (I_{H} \otimes M_{a, r}) ρ (I_{H} \otimes M_{a, r})^{*} / p_{a}$ only when $p_{a} > 0$ . Enumerate the factor operators as $(N_{b})$ on $K$ and put $L_{b} = I_{H} \otimes N_{b}$ on $H \hat{\otimes} K$ . By [F1], $\sum_{b} L_{b}^{*} L_{b} = I_{H \hat{\otimes} K}$ strongly. Clause (a) of Declared countable instruments: normalization, discarded ensembles and the repeatability criterion applied to $(L_{b})$ and $ρ$ gives the trace-norm convergent discarded map $Φ (ρ) = \sum_{b} L_{b} ρ L_{b}^{*}$ , positivity, trace preservation and a state. A finite family is padded by zero operators. Each positive branch has trace equal to its probability; a zero-probability branch is zero because a positive trace-class operator has trace norm equal to its trace, as used in that theorem's proof. Grouping the positive series therefore yields $Φ (ρ) = \sum_{a : p_{a} > 0} p_{a} ρ_{a}$ in trace norm. No repeatability criterion is used.

[F3]

Local trace-preserving maps leave the other reduction fixed. For bounded operators $(N_{b})_{b \geq 1}$ on $K$ with $\sum_{b \leq N} N_{b}^{*} N_{b} \to I_{K}$ strongly and a trace-class $R$ on $H \hat{\otimes} K$ , the series $\sum_{b} (I_{H} \otimes N_{b}) R (I_{H} \otimes N_{b})^{*}$ converges in trace norm, its sum $Φ (R)$ is trace class and ${Tr}_{K} Φ (R) = {Tr}_{K} R$ (Local trace-preserving Kraus maps do not change the opposite reduced state).

[F4]

Local readout law. For every assigned sharp observable $(A, u_{A})$ of subsystem $A$ , the local readout law is $μ_{ρ^{'}}^{A^{l o c}} (B) = tr (ρ_{A}^{'} E_{A} (B))$ for every preparation $ρ^{'}$ of the composite with reduced preparation $ρ_{A}^{'} = {Tr}_{K} ρ^{'}$ (Local readout laws and reduced preparations: the subsystem state determines, and is determined by, the local statistics clause (a), Separable partial trace and its basic properties clause (a)).

[F5]

Reduced preparations. $ρ_{A} = {Tr}_{K} ρ$ and $ρ_{B} = {Tr}_{H} ρ$ are linear, trace-norm continuous images of $ρ$ , and the outcome probabilities of a declared instrument of $B$ read $p_{a} = tr (ρ_{B} F_{a})$ (Reduced preparations of a declared composite: the subsystem states of the framework clauses (a), (b), Separable partial trace and its basic properties clauses (a), (b)).

[F6]

Choice hypothesis. The Axiom of Choice is assumed by the cited local sharp-readout result for the general spectral PVM construction (The Axiom of Choice).

Proof

technique · direct; read the local extension off the fibered definition of local instruments, apply the trace-preserving local-map lemma to the discarded-outcome state to fix the reduction of the untouched factor, and average the conditional reductions with the outcome probabilities

Given: The data of the statement and [F1]-[F5].

1.1givenF1F2F3F5algebra

[Extension and discarded map] By [F1] the family $(I_{H} \otimes M_{a, r})$ is a declared instrument of the composite with effects $I_{H} \otimes F_{a}$ and conditional states $ρ_{a}$ for $p_{a} > 0$ ; by [F2] its discarded-outcome map $Φ$ is positive and trace preserving, so $Φ (ρ)$ is a preparation of the composite; and re-indexing the doubly indexed family as a sequence $(N_{b})$ on $K$ with $\sum_{b \leq N} N_{b}^{*} N_{b} \to I_{K}$ strongly, [F3] gives ${Tr}_{K} Φ (ρ) = {Tr}_{K} ρ = ρ_{A}$ . This is (a) together with the first assertion of (b); likewise $p_{a} = tr (ρ F_{a}^{l o c}) = tr (ρ_{B} F_{a})$ by [F5].

2.1givenF4F6step 1.1algebra

[No-signalling] Let $(A, u_{A})$ be an assigned sharp observable of $A$ . By step 1.1 the state $Φ (ρ)$ has reduced preparation $ρ_{A}$ , so [F4] gives $μ_{Φ (ρ)}^{A^{l o c}} (B) = tr (ρ_{A} E_{A} (B)) = μ_{ρ}^{A^{l o c}} (B)$ for every Borel $B$ : no local A-statistic changes under the discarded local instrument. This is (b).

2.2givenF2F3F5step 1.1algebra

[Conditional reductions] For each $a$ with $p_{a} > 0$ , the conditional state $ρ_{a}$ of [F2] satisfies $p_{a} ρ_{a} = \sum_{r} (I_{H} \otimes M_{a, r}) ρ (I_{H} \otimes M_{a, r})^{*}$ , so by linearity and trace-norm continuity of ${Tr}_{K}$ from [F5] one has $p_{a} (ρ_{a})_{A} = {Tr}_{K} \sum_{r} (I_{H} \otimes M_{a, r}) ρ (I_{H} \otimes M_{a, r})^{*}$ . Summing over the positive-probability outcomes and using the trace-norm convergence of the discarded series from [F3] gives $\sum_{a : p_{a} > 0} p_{a} (ρ_{a})_{A} = {Tr}_{K} Φ (ρ) = ρ_{A}$ by step 1.1; the terms for zero-probability outcomes are zero contributions to $Φ (ρ)$ and no conditional state is assigned to them. This is (c); the exchanged-roles form of (b) is the same argument with $H$ and $K$ interchanged.

3.1step 1.1step 2.1step 2.2∎

[Assembly and scope] Step 1.1 is (a), step 2.1 is (b), step 2.2 is (c), and (d) records that only the declared readings and the cited mathematics were used, with no causality or apparatus claim.

Local instruments and no-signalling: operations on one factor do not change the other factor's local statistics

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources