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 readout laws and reduced preparations: the subsystem state determines, and is determined by, the local statistics

Physical scope

The reading of the framework's Born law (P2) and ideal conditional-measurement law (P3) for quantities of one factor of a declared composite of two distinguishable subsystems: the outcome law of a local readout equals the outcome law of the factor quantity in the reduced preparation, the reduced preparation is determined by the local statistics, and a declared ideal sharp measurement of the factor acts on the composite with conditional and discarded reductions inherited from the factor. The unchanged opposite reduction is proved only for the declared ideal P3 instrument; no disturbance claim about a real apparatus, no dynamics, no interaction, no apparatus realization and no empirical fact are asserted.

Statement

Adopt the framework's composition, state 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, Reduced preparations of a declared composite: the subsystem states of the framework, Declared ideal measurements and instruments 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), the choice hypotheses of the cited suppliers. Let $ρ, ρ^{'} \in D (H \hat{\otimes} K)$ be preparations with reduced preparations $ρ_{A} = {Tr}_{K} ρ$ , $ρ_{A}^{'} = {Tr}_{K} ρ^{'}$ and $ρ_{B} = {Tr}_{H} ρ$ . Then:

(a) Local readout law. For every assigned sharp observable $(A, u_{A})$ of subsystem $A$ with local readout $(A^{l o c}, u_{A})$ and every Borel $B \subseteq R$ , $μ_{ρ}^{A^{l o c}} (B) = tr (ρ (E_{A} (B) \otimes I_{K})) = tr (ρ_{A} E_{A} (B)) = μ_{ρ_{A}}^{A} (B),$ where $E_{A}$ is the spectral projection valued measure of $A$ . In particular the local statistics of subsystem $A$ depend on the composite preparation only through its reduced preparation, and if $ρ_{A} = ρ_{A}^{'}$ then every local readout law is the same in $ρ$ and in $ρ^{'}$ .

(b) Determination of the reduced preparation. Conversely, if $ρ_{A} \neq ρ_{A}^{'}$ , then there are a bounded assigned sharp observable $(P, 1)$ of subsystem $A$ and a Borel set $B$ with $μ_{ρ}^{P^{l o c}} (B) \neq μ_{ρ^{'}}^{P^{l o c}} (B)$ : the family of local readout laws of subsystem $A$ determines $ρ_{A}$ among the preparations of the composite.

(c) Ideal local measurement. Let $(P_{a})_{a \in A_{0}}$ be a declared ideal sharp measurement of subsystem $A$ (Declared ideal measurements and instruments of the framework clause (a)). Then $(P_{a} \otimes I_{K})_{a \in A_{0}}$ is a declared ideal sharp measurement of the declared composite, its outcome probabilities in a preparation $ρ$ are $p_{a} = tr (ρ (P_{a} \otimes I_{K})) = tr (ρ_{A} P_{a}),$ and for $p_{a} > 0$ the conditional state $ρ_{a} : = (P_{a} \otimes I_{K}) ρ (P_{a} \otimes I_{K}) / p_{a}$ of the composite has the reduced preparation $(ρ_{a})_{A} = \frac{P_{a} ρ_{A} P_{a}}{p_{a}},$ which is the selective Lueders update of $ρ_{A}$ by $P_{a}$ . The discarded-outcome state $Φ (ρ) = \sum_{a} (P_{a} \otimes I_{K}) ρ (P_{a} \otimes I_{K})$ has reduced preparations $Φ (ρ)_{A} = \sum_{a} P_{a} ρ_{A} P_{a}, Φ (ρ)_{B} = {Tr}_{H} Φ (ρ) = ρ_{B} .$ The analogous statements hold with the roles of $A$ and $B$ exchanged.

(d) Scope. Clauses (a)-(c) are conditional consequences of P1, P2 and P3 in the readings of the cited items and of the cited mathematics. They concern the declared composite and its declared measurements; they assert no dynamics, no interaction, no apparatus realization, no uniqueness of recorded outcomes and no empirical fact, and clause (c) is a statement about the declared ideal Lueders instrument only, not about every laboratory procedure.

Facts & Assumptions

Given: The declared composite with assigned spaces $H, K$ ; preparations $ρ, ρ^{'}$ ; reduced preparations $ρ_{A}, ρ_{A}^{'}, ρ_{B}$ ; an assigned sharp observable $(A, u_{A})$ of subsystem $A$ with spectral measure $E_{A}$ ; a declared ideal sharp measurement $(P_{a})_{a \in A_{0}}$ of subsystem $A$ ; the choice hypotheses.

[F1]

Local readout and its outcome law. For an assigned sharp observable $(A, u_{A})$ of subsystem $A$ , the local readout $(A^{l o c}, u_{A})$ is the assigned sharp observable of the composite with spectral projection valued measure $F_{A} = E_{A} (\cdot) \otimes I_{K}$ , so that $μ_{ρ}^{A^{l o c}} (B) = tr (ρ (E_{A} (B) \otimes I_{K}))$ ; $E_{A}$ is regular and $F_{A}$ is a regular projection valued measure by Local PVM extension: tensoring a projection-valued measure with the identity (Composite systems of the framework: product bases, local readouts, local effects and local instruments clause (c), Assigned sharp observables and the outcome law of the framework clauses (a), (b)).

[F2]

Partial trace. $tr (({Tr}_{K} T) X) = tr (T (X \otimes I_{K}))$ for every trace-class $T$ and bounded $X$ , and ${Tr}_{K}$ is linear, positive, trace preserving and trace-norm contractive; moreover ${Tr}_{K} T_{u \otimes v, u^{'} \otimes v^{'}} = ⟨ v, v^{'} ⟩ T_{u, u^{'}}$ (Separable partial trace and its basic properties clauses (a), (b), (c)).

[F3]

Trace pairing and cyclicity. For trace-class $T$ and bounded $B$ one has $tr (B T) = tr (T B)$ and $∣ tr T ∣ \leq ∥ T ∥_{1}$ (Nuclear bounded cyclicity for trace-class operators clause (b), Trace is absolutely convergent and basis independent, Trace class is a two sided Banach operator ideal clauses 1, 2); the rank-one operators satisfy $tr (S T_{w, w^{'}}) = ⟨ S w, w^{'} ⟩$ , $T_{w, w^{'}}$ is bounded with $∥ T_{w, w^{'}} ∥ = ∥ w ∥ ∥ w^{'} ∥$ , and $T_{w, w}$ is an orthogonal projection for unit $w$ (Rank-one operator calculus clauses (a), (b), (c), (e)).

[F4]

Separating local statistics. If two density operators $ρ_{A} \neq ρ_{A}^{'}$ on $H$ are distinct, then there is a unit $w$ with $⟨ ρ_{A} w, w ⟩ \neq ⟨ ρ_{A}^{'} w, w ⟩$ , and the rank-one projection $P = T_{w, w}$ has the outcome laws $μ_{ρ_{A}}^{P} ({1}) = tr (ρ_{A} P) = ⟨ ρ_{A} w, w ⟩$ and $μ_{ρ_{A}^{'}}^{P} ({1}) = ⟨ ρ_{A}^{'} w, w ⟩$ (Distinct density operators are separated by the law of a bounded rank-one projection clauses (a), (b), Density operators and scalar spectral probability clause (b)).

[F5]

Ideal sharp measurement of the composite. For a declared ideal sharp measurement $(P_{a})$ of a system, the outcome probability in $ρ$ is $p_{a} = tr (ρ P_{a})$ , the conditional state is $P_{a} ρ P_{a} / p_{a}$ when $p_{a} > 0$ , and the discarded-outcome state is the trace-norm convergent sum $Φ (ρ) = \sum_{a} P_{a} ρ P_{a}$ with $tr (Φ (ρ) P_{a}) = p_{a}$ (Consequences of a declared ideal sharp measurement: repeatability and discarded ensembles clauses (a), (b), (c), Declared ideal measurements and instruments of the framework clauses (a), (b)).

[F6]

Tensor calculus and strong continuity. $(S \otimes I_{K}) κ (x \otimes y) = κ (S x \otimes y)$ for bounded $S$ , and $(S \otimes T) (S^{'} \otimes T^{'}) = (S S^{'}) \otimes (T T^{'})$ , $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ , $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ for bounded operators (Bounded tensor maps: extension, norm estimate, adjoint and commutation clauses (a), (b), (c)); if a sequence of bounded operators is uniformly bounded and converges strongly, then tensoring with $I_{K}$ preserves the strong convergence (Local PVM extension: tensoring a projection-valued measure with the identity clause (c)).

[F7]

Density-operator expansion. The preparation $ρ$ has a finite or countable trace-norm convergent expansion $ρ = \sum_{n} w_{n} T_{u_{n}, u_{n}}$ with $(u_{n})$ orthonormal, $w_{n} \geq 0$ and $\sum_{n} w_{n} = 1$ (Density operators and scalar spectral probability clause (a)).

Proof

Proof technique: direct; establish the intertwining identity for the partial trace and bounded operators on one factor, derive the local readout law from the partial trace characterization, read the determination of the reduced preparation off the separating rank-one projection, and compute the conditional and discarded reductions of a local ideal sharp measurement with the intertwining identity.

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

1.1F2F3F6algebra

[Intertwining identity] Let $T$ be trace class on $H \hat{\otimes} K$ and $X, Y$ bounded on $H$ . For every bounded $Z$ on $H$ , [F2] gives $tr ({Tr}_{K} ((X \otimes I) T (Y \otimes I)) Z) = tr ((X \otimes I) T (Y \otimes I) (Z \otimes I)) = tr (T (Y Z X \otimes I)) = tr (({Tr}_{K} T) (Y Z X)) = tr (X ({Tr}_{K} T) Y Z)$ by [F3] and [F6]; since ${Tr}_{K} ((X \otimes I) T (Y \otimes I))$ and $X ({Tr}_{K} T) Y$ are trace-class operators with equal trace pairings against every bounded $Z$ , they are equal by [F3].

1.2givenF6algebra

[The extended family is a declared measurement] The operators $P_{a} \otimes I_{K}$ are orthogonal projections by [F6]; $P_{a} P_{b} = 0$ for $a \neq b$ gives $(P_{a} \otimes I_{K}) (P_{b} \otimes I_{K}) = (P_{a} P_{b}) \otimes I_{K} = 0$ ; and $\sum_{a \in A_{0}} (P_{a} \otimes I_{K}) = I_{H} \otimes I_{K}$ in the strong sense, because the finite partial sums are $(\sum_{a \leq N} P_{a}) \otimes I_{K}$ by linearity and converge strongly to $I_{H} \otimes I_{K}$ by [F6], the projections $\sum_{a \leq N} P_{a}$ being uniformly bounded and converging strongly to $I_{H}$ . Hence $(P_{a} \otimes I_{K})$ is a declared ideal sharp measurement of the composite.

1.3givenF1F2algebra

[Local readout law] For every Borel $B$ , [F1] gives $μ_{ρ}^{A^{l o c}} (B) = tr (ρ (E_{A} (B) \otimes I_{K}))$ , and [F2] applied with the bounded operator $E_{A} (B)$ gives $tr (ρ (E_{A} (B) \otimes I_{K})) = tr (ρ_{A} E_{A} (B)) = μ_{ρ_{A}}^{A} (B)$ by [F1]; applying the same identity to $ρ^{'}$ gives the case $ρ_{A} = ρ_{A}^{'}$ , so this is (a).

2.1givenF3F4step 1.3algebra

[Determination of the reduced preparation] Suppose $ρ_{A} \neq ρ_{A}^{'}$ . By [F4] there is a unit $w$ with $⟨ ρ_{A} w, w ⟩ \neq ⟨ ρ_{A}^{'} w, w ⟩$ ; declare the bounded self-adjoint operator $P : = T_{w, w}$ with unit $1$ as a bounded assigned sharp observable of subsystem $A$ . Its local readout $(P^{l o c}, 1)$ has, by step 1.3, the outcome law $μ_{ρ}^{P^{l o c}} ({1}) = tr (ρ (P \otimes I_{K})) = tr (ρ_{A} P) = ⟨ ρ_{A} w, w ⟩$ , and likewise $μ_{ρ^{'}}^{P^{l o c}} ({1}) = ⟨ ρ_{A}^{'} w, w ⟩$ ; the two numbers differ, so some local readout law differs, which is (b).

2.2givenF2F5step 1.1step 1.2algebra

[Conditional local measurement] By step 1.2 the family $(P_{a} \otimes I_{K})$ is a declared ideal sharp measurement of the composite, so [F5] gives $p_{a} = tr (ρ (P_{a} \otimes I_{K})) = tr (ρ_{A} P_{a})$ by [F2], and the conditional state $ρ_{a} = (P_{a} \otimes I_{K}) ρ (P_{a} \otimes I_{K}) / p_{a}$ for $p_{a} > 0$ . Step 1.1 with $X = Y = P_{a}$ gives ${Tr}_{K} ((P_{a} \otimes I_{K}) ρ (P_{a} \otimes I_{K})) = P_{a} ρ_{A} P_{a}$ , hence $(ρ_{a})_{A} = P_{a} ρ_{A} P_{a} / p_{a}$ ; the conditional update of the composite reduces to the selective Lueders update of $ρ_{A}$ , which is the first part of (c).

2.3givenF2F3F5F6F7step 1.1step 1.2algebra

[Discarded local measurement] The discarded-outcome state $Φ (ρ)$ of [F5] has $A$ -reduction $\sum_{a} P_{a} ρ_{A} P_{a}$ : apply ${Tr}_{K}$ to the trace-norm convergent series termwise using step 1.1 and the trace-norm continuity of ${Tr}_{K}$ from [F2]. For the $B$ -reduction let $Y$ be bounded on $K$ , enumerate the outcomes, and set $S_{N} = \sum_{a \leq N} P_{a}$ . Orthogonality and the strong resolution of the identity give $0 \leq S_{N} \leq I_{H}$ and $S_{N} \to I_{H}$ strongly. By [F6], $S_{N} \otimes I_{K} \to I_{H} \otimes I_{K}$ strongly, and the tensor product rule gives $S_{N} \otimes Y = (S_{N} \otimes I_{K}) (I_{H} \otimes Y) \to I_{H} \otimes Y$ strongly with $\sup_{N} ∥ S_{N} \otimes Y ∥ \leq ∥ Y ∥$ . The strong limit passes through this trace pairing by a finite-tail argument: [F7] and the rank-one trace identity in [F3] give $tr (ρ (S_{N} \otimes Y)) = \sum_{k} w_{k} ⟨ (S_{N} \otimes Y) u_{k}, u_{k} ⟩$ . For each $k$ the summand converges to $w_{k} ⟨ (I_{H} \otimes Y) u_{k}, u_{k} ⟩$ , and its modulus is at most $w_{k} ∥ Y ∥$ . Given $ε > 0$ , choose a finite initial segment ending at $N_{0}$ whose omitted weights sum to less than $ε / (4 ∥ Y ∥)$ when $Y \neq 0$ ; the tail of the difference from the limit is at most $2 ∥ Y ∥ \sum_{k > N_{0}} w_{k} < ε / 2$ , while strong convergence on the finite segment makes that part less than $ε / 2$ for all sufficiently large $N$ ; hence $tr (ρ (S_{N} \otimes Y)) \to tr (ρ (I_{H} \otimes Y))$ . The case $Y = 0$ is immediate. Now let $Φ_{N} (ρ) = \sum_{a \leq N} (P_{a} \otimes I_{K}) ρ (P_{a} \otimes I_{K})$ . Trace-norm convergence in [F5] and the trace ideal bound give $tr (Φ_{N} (ρ) (I_{H} \otimes Y)) \to tr (Φ (ρ) (I_{H} \otimes Y))$ . For each finite $N$ , cyclicity [F3] and the tensor rules [F6] give $tr (Φ_{N} (ρ) (I_{H} \otimes Y)) = tr (ρ (S_{N} \otimes Y))$ . Therefore $tr ({Tr}_{H} Φ (ρ) Y) = tr (Φ (ρ) (I_{H} \otimes Y)) = tr (ρ (I_{H} \otimes Y)) = tr (ρ_{B} Y)$ by [F2]. Since the trace pairings against every bounded $Y$ determine a trace-class operator, ${Tr}_{H} Φ (ρ) = ρ_{B}$ . This completes (c); the exchanged-roles statement is the same argument with $H$ and $K$ interchanged.

3.1step 1.3step 2.1step 2.2step 2.3∎

[Assembly and scope] Step 1.3 is (a), step 2.1 is (b), steps 2.2 and 2.3 are (c), and (d) records that only P1, P2, P3 in their stated readings and the cited mathematics were used.

Remarks

Which factor is measured. Clause (c) measures subsystem $A$ ; its discarded version leaves $ρ_{B}$ fixed while changing $ρ_{A}$ into the Lueders mixture. The conditional version changes the description of $B$ as well, and that conditional change is exactly the correlation between the factors; no signalling claim beyond the outcome-law invariance is made here.
Unbounded readouts. Clause (a) covers unbounded assigned sharp observables of the factor, including the position and momentum observables of the massive-particle model, because the local readout is defined through the spectral measure $E_{A} (\cdot) \otimes I_{K}$ .

Local readout laws and reduced preparations: the subsystem state determines, and is determined by, the local statistics

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources