TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Dirac Notation Coordinate Identity

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces with ordered orthonormal bases $E = (e_{j})_{j < n}$ and $F = (f_{i})_{i < m}$ . Let $T : H \to K$ be linear (Linear map between vector spaces over the same field), and write $T_{i j}$ for the $(i, j)$ entry of its matrix in these bases. Then, for every $z \in H$ ,

$T z = \sum_{j < n} \sum_{i < m} T_{i j} ⟨ z, e_{j} ⟩_{H, r o o t} f_{i}, T = \sum_{j < n} \sum_{i < m} T_{i j} ∣ f_{i} ⟩ ⟨ e_{j} ∣ .$

For $x \in K$ and $y \in H$ , the rank-one map $∣ x ⟩ ⟨ y ∣$ has coordinate matrix $[x]_{F} [y]_{E}^{†}$ , where $M^{†} = {\overline{M}}^{T}$ . Its amplitude satisfies $⟨ x ∣ T ∣ y ⟩_{D} = ⟨ T y, x ⟩_{K, r o o t}$ . All sums are empty when an index dimension is zero, and the identities include those cases.

Facts & Assumptions

Given: The spaces, ordered orthonormal bases, linear map, and vectors in the Statement.

[F1]

For an orthonormal basis $(e_{j})_{j < n}$ , $z = \sum_{j < n} ⟨ z, e_{j} ⟩ e_{j}$ ; the corresponding inner-product coordinate formula and empty-basis case also hold (Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis).

[F2]

The $j$ -th matrix column of a linear map is the coordinate column of the image of the $j$ -th basis vector (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[F3]

$∣ x ⟩ ⟨ y ∣$ acts on $z$ by $z \mapsto ⟨ z, y ⟩_{r o o t} x$ , and $⟨ x ∣ y ⟩_{D} = ⟨ y, x ⟩_{r o o t}$ (Dirac Notation Conversion).

[F4]

Matrix multiplication is row-by-column finite summation (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F5]

Transposition interchanges matrix rows and columns (The transpose $A^{T}$ of a matrix).

[F6]

Complex conjugation is the usual scalar involution (Real and imaginary parts, complex conjugation, and modulus).

[F7]

The root inner product is conjugate-symmetric (Real and complex inner-product spaces and their induced length).

Proof

1.1givenF1F2algebra

By [F1], $z = \sum_{j < n} ⟨ z, e_{j} ⟩ e_{j}$ . Applying $T$ and using linearity, then expanding each $T e_{j}$ by [F2], gives $T z = \sum_{j < n} \sum_{i < m} T_{i j} ⟨ z, e_{j} ⟩ f_{i}$ .

1.2F1F2F3F4F5F6F7algebra

Write $x_{i} = ⟨ x, f_{i} ⟩$ and $y_{j} = ⟨ y, e_{j} ⟩$ , the coordinates from [F1]–[F2]. The image of $e_{j}$ under $∣ x ⟩ ⟨ y ∣$ is $⟨ e_{j}, y ⟩ x = \overline{y_{j}} x$ by [F1] and [F7]. Its $i$ -th coordinate is therefore $x_{i} \overline{y_{j}}$ . By [F4]–[F6], these are exactly the entries of $[x]_{F} [y]_{E}^{†}$ .

1.3F3given

The amplitude identity is the defining Dirac conversion [F3].

2.1F3step 1.1

By [F3], the operator sum in the Statement sends every $z$ to the right-hand side of step 1.1. It therefore agrees with $T$ on every vector.

3.1givenstep 1.1step 2.1step 1.2step 1.3algebra∎

If $n = 0$ , then $H = 0$ , $T = 0$ , and $y = 0$ ; if $m = 0$ , then $K = 0$ , $T = 0$ , and $x = 0$ . In either case the displayed sums and rank-one map are zero, and the amplitude identity is $0 = 0$ . Thus all formulas include zero dimensions.

Depends on

Used by

Relative Phase Definition
Dirac and rank-one coordinate check Example
Register endianness and a two-qubit partial trace Example
Dihedral hidden-state pair combination Lemma
Fourier sample from a generalized-dihedral reflection coset state Lemma
Measurement law of a coherent sampler Lemma
One-bit J-gate teleportation branch identity Lemma
Phase-estimation finite outcome law Lemma
Every finite state ensemble is obtainable from a purification Theorem
Fourier samples are uniform in the annihilator Theorem
Fusion measurement branches are normalized exactly when nonzero Theorem
Pattern branch probabilities and zero-probability transcripts Theorem
Phase estimation on a superposition of eigenspaces Theorem

Cited to discharge well-definedness by Dirac Notation Conversion.

Dependency tree · two levels

23 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), Chapters 1–2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27), Appendices A.3, A.5, A.7 and A.10 (standard reference, not scraped)