LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

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.

Subsystem expectations and reduced finite tensor densities

Statement

Let $V_{A}, V_{B}$ be nonzero finite-dimensional ordered tensor registers as in Ordered tensor registers, their inner product, and wire permutations, with the product orthonormal bases and linear-first inner products specified there. On any such register $W$ , use finite tensor density to mean a matrix $R$ with $R = R^{*}$ , $x^{*} R x \geq 0$ for every coordinate vector $x$ , and $Tr R = 1$ . Here $R^{*}$ is the conjugate transpose and $Tr R$ is the sum of its diagonal entries. A finite POVM on $W$ is a family $(M_{a})_{a = 1}^{r}$ , $r \geq 1$ , of Hermitian matrices with $x^{*} M_{a} x \geq 0$ for every $x$ and $\sum_{a} M_{a} = I_{W}$ ; an effect is a Hermitian matrix $M$ with $0 \leq M \leq I_{W}$ , meaning both $M$ and $I_{W} - M$ are nonnegative in this sense. These conventions extend the identical coordinate definitions of Finite tensor density, observable and measurement language from $W = (C^{q})^{\otimes N}$ to arbitrary nonzero finite ordered registers. Let $ρ$ be a finite tensor density on $V_{A} \otimes V_{B}$ . Then $ρ_{A} : = {Tr}_{B} ρ$ is a finite tensor density on $V_{A}$ . For every matrix $A$ on $V_{A}$ , $Tr (ρ_{A} A) = Tr (ρ (A \otimes I_{B})) .$ For a finite POVM $(M_{a})_{a = 1}^{r}$ on $V_{A}$ , the trace pairings of its outcomes in $ρ_{A}$ equal the trace pairings of the lifted effects $M_{a} \otimes I_{B}$ in $ρ$ .

Facts & Assumptions

Given: The ordered tensor and density conventions specified in the Statement, a density $ρ$ on $V_{A} \otimes V_{B}$ , and a finite POVM when the last claim is used.

[F1]

Partial trace over a finite tensor factor: the partial trace contracts the second tensor factor in the specified product basis.

[F2]

The partial trace is characterized by the trace pairing and is basis-independent: its trace-pairing identity is $tr (({Tr}_{B} R) T) = tr (R (T \otimes I_{B}))$ .

[F3]

The partial trace preserves non-negativity and total trace: partial trace preserves non-negativity and total trace.

[F4]

Ordered tensor registers, their inner product, and wire permutations: the ordered product basis is orthonormal for the product inner product and spans $V_{A} \otimes V_{B}$ .

[F5]

Tensor products of finitely many linear maps: $M \otimes I_{B}$ is the linear tensor map sending $x \otimes y$ to $M x \otimes y$ .

[F6]

The Statement's extension of Finite tensor density, observable and measurement language: a finite POVM on any of the stated registers is a family of nonnegative matrices whose sum is the identity.

Proof

1.1givenF1F3

By the coordinate definition [F1], $ρ_{A}$ is the second-factor partial trace. Apply [F3] to the nonnegative trace-one operator $ρ$ . It gives $ρ_{A} \geq 0$ and $Tr ρ_{A} = Tr ρ = 1$ ; therefore $ρ_{A}$ is a finite tensor density by the Statement's explicit definition on $V_{A}$ .

2.1givenF2F4F5F6algebra∎

Apply [F2] with $R = ρ$ and $T = A$ to obtain the displayed expectation identity. If $(M_{a})$ is a POVM, choose an orthonormal basis $(b_{j})_{j = 1}^{\dim V_{B}}$ of $V_{B}$ . For $x = \sum_{j} x_{j} \otimes b_{j}$ , the product inner product [F4] and tensor map [F5] give $⟨ (M_{a} \otimes I_{B}) x, x ⟩ = \sum_{j} ⟨ M_{a} x_{j}, x_{j} ⟩ \geq 0,$ where nonnegativity of each $M_{a}$ follows from [F6]; hence every lifted matrix is nonnegative. Moreover, $\sum_{a = 1}^{r} M_{a} \otimes I_{B} = (\sum_{a = 1}^{r} M_{a}) \otimes I_{B} = I_{A} \otimes I_{B} = I_{V_{A} \otimes V_{B}};$ the final identity holds on every elementary tensor, hence on the whole finite tensor product by [F5]. Therefore the lifts are a POVM, and each is an effect because its complement is the sum of the other nonnegative lifts by [F6]. Substituting $A = M_{a}$ in the trace-pairing identity shows that each lifted outcome pairing equals the corresponding reduced-state pairing.

Subsystem expectations and reduced finite tensor densities

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources