LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

A finite instrument with nonzero input has nonzero output space

Statement

Let $H$ be a nonzero finite-dimensional complex inner-product space, let $K$ be a finite-dimensional complex inner-product space, and suppose a finite instrument $(I_{a})_{a \in Ω}$ from $H$ to $K$ exists. Then $K$ is nonzero.

Facts & Assumptions

Given: A nonzero finite-dimensional input space $H$ , a finite-dimensional output space $K$ , and a finite instrument from $H$ to $K$ .

[F1]

Finite instruments and conditional states: for every $X \in L (H)$ , $\sum_{a \in Ω} {tr}_{K} (I_{a} (X)) = {tr}_{H} (X)$ .

[F2]

Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis: every finite-dimensional vector space has a finite basis, and dimension zero is equivalent to being the zero space.

[F3]

Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The basis-independent trace of an endomorphism of a finite-dimensional vector space, and The trace $tr (A)$ as the sum of the diagonal entries: in an ordered basis of length $h$ , the identity endomorphism has matrix $I_{h}$ , and its trace is the sum of its $h$ diagonal ones.

Proof

1.1givenF2F3choosealgebra

Put $h = \dim H$ . By [F2] and $H \neq 0$ , $h \geq 1$ ; choose an ordered basis of length $h$ . The coordinate columns of the identity map give the matrix $I_{h}$ by [F3], so ${tr}_{H} (I_{H}) = tr (I_{h}) = h > 0$ .

2.1givenstep 1.1F1F2discharge-contradiction∎

Suppose $\dim K = 0$ . Then [F2] gives $K = {0}$ , so every output endomorphism $I_{a} (I_{H})$ is the zero operator and has trace $0$ . Applying [F1] to $I_{H}$ would give $0 = {tr}_{H} (I_{H})$ , contradicting step 1.1. Hence $\dim K > 0$ and $K \neq 0$ .

Depends on

Used by

Dependency tree · two levels

27 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 author-hosted draft), §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)