DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge 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.

Finite instruments and conditional states

Definition

Let $H$ be a nonzero finite-dimensional complex-inner-product space, let $K$ be a finite-dimensional complex-inner-product space, and let $Ω$ be a finite nonempty outcome set. A finite instrument from $H$ to $K$ is a family of complex-linear maps $I_{a} : L (H) \to L (K)$ , one for each $a \in Ω$ , such that each $I_{a}$ is completely positive (Completely positive maps) and

$\sum_{a \in Ω} {tr}_{K} (I_{a} (X)) = {tr}_{H} (X) for every X \in L (H) .$

For a density operator $ρ$ on $H$ (nonnegative with trace one, Density operator), define the outcome weight $p_{a} (ρ) : = {tr}_{K} (I_{a} (ρ))$ . The conditional state for outcome $a$ is

$ρ_{a} : = {\begin{cases} I_{a} (ρ) / p_{a} (ρ), & p_{a} (ρ) > 0, \\ ⊥, & p_{a} (ρ) = 0. \end{cases}$

Here $⊥$ is a symbol meaning that no conditional density operator is assigned; it is not a state. Positivity and normalization of the outcome weights, and density of every positive-probability conditional state, are proved in Instrument outcome weights normalize ↗ and Positive-probability instrument branches are density operators ↗.

Depends on

Used by

MNRS finite reversible-walk finding Algorithm
One Simon Fourier-sampling sample Algorithm
Power-of-two dihedral hidden-subgroup sieve Algorithm
Quantum phase estimation Algorithm
Simon promise decision by sampled rank Algorithm
Szegedy-walk marked-set detection Algorithm
A symmetrized acceptance polynomial can exceed one between Hamming layers Counterexample
Finite authenticated key-distribution protocol Definition
Finite measurement branches and classical control Definition
Finite open-graph adaptive measurement pattern Definition
Heralded success and conditional verification contract Definition
Normalized output law for finite quantum query branches Definition
Oracle-only bit-query algorithm Definition
Pauli measurement branch semantics Definition
The outcome law and outputs of a measured circuit Definition
A one-query exact algorithm on a two-point OR promise Example
A projective measurement branch with probability zero Example
Heralded success and the zero-success branch Example
A finite instrument has an isometric coherent record Lemma
A finite instrument with nonzero input has nonzero output space Lemma
Coherent normal form for finite quantum query algorithms Lemma
Computational-basis instruments and conditional states on two registers Lemma
Dihedral hidden-state pair combination Lemma
Fourier sample from a generalized-dihedral reflection coset state Lemma
One-bit J-gate teleportation branch identity Lemma
Pauli projectors define a finite measurement instrument Lemma
Unnormalized branch density entries have degree at most twice the query count Lemma
A zero-probability instrument branch has no conditioned state Theorem
Every finite instrument induces a unique POVM Theorem
Every finite open-graph pattern is a measurement circuit Theorem
Finite reversible-walk finding cost Theorem
Instrument branch Kraus families satisfy total normalization Theorem
Instrument outcome weights normalize Theorem
Kuperberg dihedral hidden-subgroup scope and resource claim Theorem
Pattern branch probabilities and zero-probability transcripts Theorem
Phase estimation on a superposition of eigenspaces Theorem
Positive-probability instrument branches are density operators Theorem
Simon query and output measurement produce a coset pair Theorem
The nonselective output of an instrument is a density operator Theorem
The square-root Lüders maps form an instrument Theorem

…and 1 more result.

Dependency tree · two levels

17 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.2.4 (standard reference, not scraped)