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.

Finite wire permutations are unitary basis permutations

Statement

Let $H_{0}, \dots, H_{n - 1}$ be a finite ordered family of finite-dimensional complex inner-product spaces, with the product bases of Ordered tensor registers, their inner product, and wire permutations. For a permutation $σ$ of the factor positions, the map $P_{σ}$ that reorders the factors is a bijective linear isometry from $H_{0} \otimes \dots \otimes H_{n - 1}$ to $H_{σ (0)} \otimes \dots \otimes H_{σ (n - 1)}$ . When source and target are identified as the same register, $P_{σ}$ is a unitary operator in the sense of Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces.

Facts & Assumptions

Given: The ordered factors, their specified orthonormal bases, and a permutation $σ$ of the factor positions.

[F1]

$P_{σ}$ sends a product-basis vector to the product-basis vector with the same factor labels in permuted order (Ordered tensor registers, their inner product, and wire permutations).

[F2]

The ordered product vectors form an orthonormal basis, including the empty and zero-dimensional cases (The product basis is orthonormal and tensor dimensions multiply).

[F3]

A linear isometry preserves vector norms; an invertible linear isometry of a finite-dimensional complex inner-product space to itself is unitary (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces).

Proof

1.1givenF1algebra

By [F1], $P_{σ}$ sends each product-basis vector to exactly one product-basis vector, and the inverse permutation sends it back. Thus the basis assignment extends to a bijective linear map whose inverse is $P_{σ^{- 1}}$ . The empty list gives the identity on $C$ .

2.1step 1.1F2algebra

Write an arbitrary vector as $\sum_{α} c_{α} e_{α}$ in the orthonormal product basis from [F2]. Its squared norm is $\sum_{α} ∣ c_{α} ∣^{2}$ . The map permutes that basis, so its image has the same coefficients in a permuted orthonormal basis and the same squared norm. Thus $P_{σ}$ is a linear isometry. If a factor is zero-dimensional, both tensor spaces are zero and the unique map between them is bijective and isometric.

3.1step 1.1step 2.1F3∎

When the source and target are the same register, steps 1.1 and 2.1 give an invertible linear isometry of that space, hence a unitary operator by [F3].

Depends on

Used by

Dependency tree · two levels

16 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 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, Appendix A.6 (standard reference, not scraped)