DefinitionDefinition: 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.

Ordered tensor registers, their inner product, and wire permutations

Definition

An ordered tensor register consists of a finite ordered list of finite-dimensional complex inner-product spaces $H_{0}, \dots, H_{n - 1}$ , each equipped with a specified ordered orthonormal basis. Its space is $H_{0} \otimes \dots \otimes H_{n - 1}$ , with factors retained in the displayed order. The product basis is ordered lexicographically by its tuple of factor indices. The empty tensor product is $C$ with basis ${1}$ . A zero-dimensional factor is allowed in this mathematical construction and makes the tensor space zero; it is not a register under Finite registers and their ordered computational bases.

The inner product is linear in the first argument and conjugate-linear in the second, and on elementary tensors it is

${⟨ ⨂_{k < n} x_{k}, ⨂_{k < n} y_{k} ⟩}_{\otimes} : = \prod_{k < n} ⟨ x_{k}, y_{k} ⟩_{r o o t, k} .$

For the empty tensor, the right side is the empty product $1$ , giving the standard inner product on $C$ .

For a permutation $σ$ of the $n$ factor positions, the wire permutation $P_{σ}$ maps the product basis vector indexed by $(i_{0}, \dots, i_{n - 1})$ to the product basis vector whose output factor order is $(σ (0), \dots, σ (n - 1))$ . It is extended linearly; for $n = 0$ it is the identity on $C$ . The extension is a linear map in the sense of Linear map between vector spaces over the same field.

Facts & Assumptions

Given: A finite ordered list of finite-dimensional complex inner-product spaces with specified ordered orthonormal bases.

[F1]

For free modules with ordered bases, the elementary tensors of basis vectors form a basis, including an empty basis in either factor (The elementary tensors of two bases form the product basis of the tensor product).

[F2]

Finite iterated tensor products represent multilinear maps, with the empty tensor product equal to the scalar module and the one-factor case unchanged (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F3]

The standard coordinate pairing on a finite complex coordinate space is an inner product, linear in the first argument (The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products).

[F4]

Each factor pairing is linear in its first argument and conjugate-linear in its second (Real and complex inner-product spaces and their induced length).

[F5]

Coordinates in a finite ordered basis are unique (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[F6]

The module tensor product is generated by elementary tensors, which are multilinear in their factors; over $C$ it has its stated module structure and the empty tensor unit is $C$ (The tensor product $M \otimes_{R} N$ from the additive group underlying the free $Z$ -module on $M \times N$ , elementary tensors, and finite tensor sums, Over a commutative ring, $M \otimes_{R} N$ is an $R$ -module with $r (m \otimes n) = (r m) \otimes n = m \otimes (r n)$ , Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F7]

A linear map preserves finite linear combinations (Linear map between vector spaces over the same field).

Proof

1.1givenF1F2F6algebra

For $n = 0$ , the declared space is $C$ with its usual pairing and basis ${1}$ . For $n > 0$ , repeated use of [F1] and the associativity identifications in [F2] shows that the lexicographically ordered elementary product vectors form a basis of the tensor space. If one factor basis is empty, the product basis is empty and the tensor space is zero.

2.1step 1.1F3F4F5

Use the coordinates in this product basis to define the pairing by the standard coordinate formula of [F3]. The basis gives unique coordinates by [F5], so this is a well-defined sesquilinear positive-definite pairing. It is linear first and conjugate-linear second by [F3] and [F4].

3.1step 2.1F3F5F6algebra

Write $x_{k} = \sum_{i_{k}} x_{k, i_{k}} e_{k, i_{k}}$ and $y_{k} = \sum_{i_{k}} y_{k, i_{k}} e_{k, i_{k}}$ in the supplied bases, using their unique coordinates [F5]. Multilinearity of elementary tensors [F6], applied one factor at a time, gives the coefficient $\prod_{k} x_{k, i_{k}}$ of each product-basis vector in $⨂_{k} x_{k}$ , and similarly $\prod_{k} y_{k, i_{k}}$ for $⨂_{k} y_{k}$ . The standard coordinate formula [F3] therefore gives $\sum_{(i_{0}, \dots, i_{n - 1})} \prod_{k} x_{k, i_{k}} \overline{y_{k, i_{k}}}$ . Repeated finite distributivity factors this as $\prod_{k} \sum_{i_{k}} x_{k, i_{k}} \overline{y_{k, i_{k}}}$ , which is the displayed product formula. For $n = 0$ both expressions are $1$ ; if a factor has dimension $0$ , the product basis is empty and both the tensor pairing and product over factor pairings are $0$ .

4.1step 3.1F1F4F6

The product formula depends only on the factor pairings. Any other supplied orthonormal bases therefore give the same pairing on elementary tensors; elementary tensors span by [F1], so sesquilinearity makes the pairings equal everywhere.

5.1step 1.1F1F2F5F7algebra∎

The factor permutation in the Definition sends the product basis bijectionally to the product basis in the reordered factors. Unique coordinates [F5] make its linear extension well-defined, and [F7] makes that extension linear; applying the inverse permutation to basis vectors gives the inverse linear map. For the empty list the definition is already the identity.

Depends on

Used by

Complete-graph continuous-time search Algorithm
Costed coherent evaluation of cyclic group powers Algorithm
Exact binary QFT circuit Algorithm
Exact Two-Level Elimination of a Unitary Algorithm
Five-local history-state adiabatic path Algorithm
Hypercube continuous-time state transfer Algorithm
Isometry Unitary Completion Algorithm
One finite abelian hidden-subgroup Fourier sample Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
Power-of-two dihedral hidden-subgroup sieve Algorithm
Product block encoding with separate ancillas Algorithm
Quantum phase estimation Algorithm
Reversible embedding of a Boolean circuit Algorithm
Reversible modular multiplication by a unit Algorithm
Simon promise decision by sampled rank Algorithm
Distance corrects unlocated errors and known erasures Corollary
A preserved unknown state cannot program its own reflection Counterexample
Abort-aware real and ideal QKD outputs and security errors Definition
Choi matrix with input factor first Definition
Clean and dirty ancillas Definition
Clean-ancilla zero-branch postselection Definition
Coherent finite sampler and observable value Definition
Coherent XOR function oracle Definition
Complementary channels and coherent information Definition
Completely positive maps Definition
Controlled Unitary Access Definition
Controlled-Z and SWAP Definition
CSS code from nested binary codes Definition
Denotational semantics of a finite layered circuit Definition
Eigenphase estimation access model Definition
Ensemble and purification Definition
Feynman–Kitaev history Hamiltonian Definition
Finite authenticated key-distribution protocol Definition
Finite block encoding Definition
Finite classical-quantum states and Holevo information Definition
Finite measurement branches and classical control Definition
Finite open-graph adaptive measurement pattern Definition
Finite quantum mutual, conditional, and conditional mutual information Definition

…and 169 more results.

Dependency tree · two levels

51 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)