TheoremStatement: AI-adaptedProof: 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.

An isometric quantum encoding gives an orthogonal code projector

Statement

Let $H_{L}, H_{P}$ be finite-dimensional complex inner-product spaces and let $V : H_{L} \to H_{P}$ be a linear isometry. Then $V^{*} V = I_{H_{L}}$ . Consequently $P : = V V^{*}$ is self-adjoint and idempotent and is the orthogonal projection onto $im V$ . If $K = \dim H_{L}$ and $N = \dim H_{P}$ , then $0 \leq K \leq N$ ; when $K = 1$ the code is a line, and when $K = N$ the code subspace is all of $H_{P}$ and $P = I_{H_{P}}$ .

Facts & Assumptions

Given: Finite-dimensional complex inner-product spaces $H_{L}, H_{P}$ , with pairing linear in the first argument, and a norm-preserving linear map $V : H_{L} \to H_{P}$ .

[F1]

Real and complex inner-product spaces and their induced length: The complex inner product is linear in its first argument and conjugate-linear in its second.

[F2]

Finite complex linear isometries preserve inner products: A linear isometry between finite-dimensional complex inner-product spaces preserves the first-linear inner product.

[F3]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : The adjoint satisfies $⟨ V x, z ⟩_{P} = ⟨ x, V^{*} z ⟩_{L}$ .

[F4]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: Such an adjoint exists uniquely for finite-dimensional inner-product spaces.

[F5]

Inner products separate vectors, and the induced norm is homogeneous: $∥ λ v ∥ = ∣ λ ∣ ∥ v ∥$ : Inner-product pairings separate vectors.

[F6]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : $(S T)^{*} = T^{*} S^{*}$ and $T^{* *} = T$ for compatible finite-dimensional maps.

[F7]

An endomorphism is an orthogonal projection exactly when it is idempotent and self-adjoint: A finite-dimensional endomorphism is an orthogonal projection exactly when it is self-adjoint and idempotent; its range is the projected subspace.

[F8]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : For a finite-dimensional domain, $\dim V = \dim \ker T + \dim im T$ .

[F9]

If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ : A subspace of a finite-dimensional space has dimension at most the ambient dimension and equals the ambient space when dimensions agree.

Proof

1.1F1F2given

Norm preservation and [F2] give $⟨ V x, V y ⟩_{P} = ⟨ x, y ⟩_{L}$ for all $x, y$ , since each of the four norms in the polarization formula is preserved.

2.1F1F3F4F5step 1.1

The adjoint exists by [F4]. By [F3] and step 1.1, $⟨ x, (V^{*} V - I) y ⟩_{L} = 0$ for every $x$ . Conjugate symmetry from [F1] and nondegeneracy [F5] imply $(V^{*} V - I) y = 0$ for every $y$ . Thus $V^{*} V = I$ .

3.1F6step 2.1given

With $P = V V^{*}$ , [F6] gives $P^{*} = V V^{*} = P$ , and step 2.1 gives $P^{2} = V (V^{*} V) V^{*} = V V^{*} = P$ .

4.1F7step 2.1step 3.1given

For every $z \in H_{P}$ , $P z = V (V^{*} z)$ belongs to $im V$ . Conversely, $P (V x) = V (V^{*} V) x = V x$ , so every vector in $im V$ lies in $im P$ . Therefore $im P = im V$ , and [F7] identifies $P$ as the orthogonal projection onto the code subspace.

5.1F1F8F9step 4.1given∎

If $V x = 0$ , norm preservation gives $∥ x ∥ = 0$ , hence $x = 0$ by positive definiteness [F1]; so $V$ is injective. [F8] yields $\dim im V = K$ , and [F9] gives $K \leq N$ . Also $0 \leq K$ because dimensions are natural numbers. If $K = 1$ , the image is a line. If $K = N$ , [F9] gives $im V = H_{P}$ , so step 4.1 gives $P = I$ .

Remarks

The root inner product is linear in the first argument; no bra-ket convention is imported. The norm-preservation implication is proved locally in Finite complex linear isometries preserve inner products, so this argument uses no choice principle.

Depends on

Used by

Cited to discharge well-definedness by Quantum code as an isometric encoding and its code projector.

Dependency tree · two levels

46 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

Richard Cleve, Quantum Information Processing course notes, §§36.1 and 37.3 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 7, §§7.1 and 7.4.1 (standard reference, not scraped)