TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The square-root Lüders maps form an instrument

Statement

Let $(E_{a})_{a \in Ω}$ be a finite POVM on $H$ , and let $M_{a} = E_{a}^{1 / 2}$ be the nonnegative square root of each effect. The maps

$I_{a} (X) : = M_{a} X M_{a}, X \in L (H),$

form an instrument from $H$ to itself.

Facts & Assumptions

Given: A nonzero finite-dimensional complex-inner-product space $H$ , a finite POVM $(E_{a})_{a \in Ω}$ , and $M_{a} = E_{a}^{1 / 2}$ .

[F1]

Finite POVMs and their outcome law: each effect $E_{a}$ is nonnegative and $\sum_{a} E_{a} = I_{H}$ .

[F2]

Finite instruments and conditional states: a family of completely positive outcome maps whose output traces sum to the input trace on every operator is an instrument.

[F3]

Completely positive maps: a branch map is completely positive when all its finite-ancilla extensions preserve nonnegative operators.

[F4]

Finite ancilla amplification is a well-defined block map: for an extension input with blocks $X_{i j}$ , the amplification of $X \mapsto M_{a} X M_{a}$ has blocks $M_{a} X_{i j} M_{a}$ .

[F5]

A non-negative operator has a unique non-negative square root: $M_{a}$ is nonnegative and $M_{a}^{2} = E_{a}$ .

[F6]

The space $L (V, W)$ of linear maps with pointwise addition and scalar multiplication: $L (H)$ has pointwise addition and scalar multiplication.

[F7]

$L (V, W)$ is a vector space over the common scalar field: those pointwise operations make $L (H)$ a vector space.

[F8]

Identity maps and composites of linear maps are linear: a composition of linear maps is linear.

[F9]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is cyclic for compatible rectangular products.

[F10]

Trace is a linear functional on $M_{n} (F)$ : trace is linear on finite-dimensional matrix spaces.

[F11]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: compatible block matrices multiply by row-by-column finite sums.

[F12]

Non-negative and positive operators: a nonnegative operator is self-adjoint and has nonnegative quadratic form on every vector.

[F13]

Ordered tensor registers, their inner product, and wire permutations: after specifying ordered orthonormal bases for the factors, their tensor register carries the product inner product, linear in the first argument.

[F14]

Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis: finite-dimensional $H$ has a finite basis; since $H$ is nonzero, this basis is nonempty.

[F15]

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans: Gram–Schmidt turns a finite linearly independent list, in particular a basis, into an orthonormal list with the same span.

[F16]

The product basis is orthonormal and tensor dimensions multiply: product vectors from specified orthonormal bases of the factors form an orthonormal basis of the tensor register.

Proof

1.1givenF6F7F8

For each $a$ , $X \mapsto M_{a} X M_{a}$ takes $L (H)$ to $L (H)$ by composition of linear maps [F8]. For $X, Y \in L (H)$ , scalars $s, t \in C$ , and $v \in H$ , evaluate at $v$ to obtain $M_{a} ((s X + t Y) (M_{a} v)) = s M_{a} X M_{a} v + t M_{a} Y M_{a} v$ . By the pointwise operations [F6]–[F7], this is $s I_{a} (X) v + t I_{a} (Y) v$ , so $I_{a}$ is complex-linear.

1.2givenF3F4F5F11F12F13F14F15F16

Fix any finite $r$ and a nonnegative $X$ on $H \otimes C^{r}$ in the sense of [F12]. By [F14] choose a finite basis of $H$ , which is linearly independent by the basis definition, and apply [F15] to obtain an orthonormal basis; together with the standard basis of $C^{r}$ , [F16] gives the product basis of $H \otimes C^{r}$ . By [F4], the extended branch map sends the blocks of $X$ to $M_{a} X_{i j} M_{a}$ . Let $S_{a}$ be the block-diagonal operator with $M_{a}$ on every diagonal block and zero off the diagonal. By the block product formula [F11], $(S_{a} X S_{a})_{i j} = \sum_{k, ℓ} (S_{a})_{i k} X_{k ℓ} (S_{a})_{ℓ j} = M_{a} X_{i j} M_{a}$ , so the extension is $S_{a} X S_{a}$ . Write $z = \sum_{j} z_{j} \otimes e_{j}$ and $w = \sum_{j} w_{j} \otimes e_{j}$ using that product basis. The product inner product [F13] gives $⟨ S_{a} z, w ⟩ = \sum_{j} ⟨ M_{a} z_{j}, w_{j} ⟩ = \sum_{j} ⟨ z_{j}, M_{a} w_{j} ⟩ = ⟨ z, S_{a} w ⟩$ , since $M_{a}$ is self-adjoint by [F5]; hence $S_{a}$ is self-adjoint. For all $z, w$ , self-adjointness of $S_{a}$ and $X$ gives $⟨ S_{a} X S_{a} z, w ⟩ = ⟨ X S_{a} z, S_{a} w ⟩ = ⟨ S_{a} z, X S_{a} w ⟩ = ⟨ z, S_{a} X S_{a} w ⟩$ , so $S_{a} X S_{a}$ is self-adjoint. Therefore $⟨ S_{a} X S_{a} z, z ⟩ = ⟨ X S_{a} z, S_{a} z ⟩ \geq 0$ by [F12]. Thus the extension is nonnegative for every $r$ , so [F3] gives complete positivity of each $I_{a}$ .

2.1givenF1F2F5F9F10∎

For any $X \in L (H)$ , rectangular trace cyclicity [F9] and $M_{a}^{2} = E_{a}$ give $tr (I_{a} (X)) = tr (M_{a} X M_{a}) = tr (X M_{a}^{2}) = tr (X E_{a})$ . By [F10] and completeness in [F1], $\sum_{a} tr (I_{a} (X)) = tr (X \sum_{a} E_{a}) = tr (X)$ . Thus the family satisfies the instrument trace condition [F2].

Depends on

Used by

One Simon Fourier-sampling sample Algorithm
Power-of-two dihedral hidden-subgroup sieve Algorithm
Quantum phase estimation Algorithm
Szegedy-walk marked-set detection Algorithm
A projective measurement branch with probability zero Example
Dihedral hidden-state pair combination Lemma
Fourier sample from a generalized-dihedral reflection coset state Lemma
Finite reversible-walk finding cost Theorem
Kuperberg dihedral hidden-subgroup scope and resource claim Theorem
Simon query and output measurement produce a coset pair Theorem
Walk detection correctness and cost Theorem

Dependency tree · two levels

56 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information (2018), §2.3.2 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3: Foundations II: Measurement and Evolution, §§3.1.2–3.2.4 (standard reference, not scraped)