Finite-Dimensional QM Formalization

Finite-dimensional quantum mechanics is a useful starting point for formalization because every linear operator is bounded and every sum over a basis is finite. The hard work is still mathematical: positivity, normalization, complete positivity, and subsystem identity must be encoded correctly. A matrix calculation becomes reusable only when its relation to the abstract state and channel interfaces is proved.

Required background. Density Operators defines positivity and trace normalization; Hilbert Space Tensor Products identifies composite spaces.

Choose an abstract space and a coordinate interface

One approach uses a finite-dimensional complex inner-product space $H$ and its linear endomorphisms. Another represents vectors as functions on a finite index type and operators as complex matrices. Both are legitimate; the bridge is an explicitly chosen orthonormal basis.

If $U:\mathbb C^d\to H$ maps coordinates to that basis, the matrix of $A$ is $U^*AU$. A nonorthonormal basis instead carries a Gram matrix, and conjugate transpose alone no longer represents the physical adjoint. An implementation that silently assumes the Euclidean inner product can therefore verify the wrong operator property even when its array dimensions are correct.

Finite index types can enforce compatible matrix products. They do not identify the physical meaning of two same-sized factors. A pair of qubits and a four-level system have isomorphic vector spaces but different declared subsystem structures.

States and effects include proofs of their defining properties

A density-operator structure should contain a matrix or endomorphism, a proof of positivity, and a proof that its trace is one. Positivity can be defined by Hermiticity and

$$\langle x,\rho x\rangle\ge0\qquad\text{for every }x\in H,$$

with the real-valued interpretation of the quadratic form explicit. Nonnegative matrix entries are a different property. They neither express Hermiticity nor ensure a nonnegative quadratic form.

An effect has $0\le E\le I$, and a finite POVM adds the normalization $\sum_iE_i=I$. The Born probability theorem then consumes those structures and yields a real number between zero and one. The effects treatment proves that mathematical result; a formal interface should retain precisely its hypotheses instead of asking every application to reconstruct them.

Existence of a normalized state requires a nontrivial space. Keeping this condition visible prevents vacuous universal claims over a state type that happens to be empty.

A channel requires more than a linear function

A finite-dimensional channel acts linearly between operator spaces, preserves trace, and is completely positive. A useful constructor takes a finite Kraus family with

$$\sum_iK_i^*K_i=I$$

and returns the channel $\Phi(\rho)=\sum_iK_i\rho K_i^*$ together with the relevant proofs. The general Kraus theorem and complete-positivity argument remain in Kraus Representation Limits and its linked derivation; the implementation should invoke that theorem rather than assume positivity from a few sample inputs.

Composition, tensoring with an identity channel, and discarding a subsystem then become typed operations on channels. Branches of an instrument are usually trace nonincreasing, so they require a different interface from a deterministic channel. Normalizing a selected branch is generally nonlinear and should not be smuggled into the linear channel type.

Tensor indices carry conventions that dimensions do not

Choose an ordering for a basis of $H_A\otimes H_B$. Under row labels $(a,b)$ and column labels $(a',b')$, partial trace over $B$ is

$$(\operatorname{Tr}_B\rho)_{a,a'} =\sum_b\rho_{(a,b),(a',b)}.$$

This formula is a specification for an index implementation. A proof should connect it to the basis-independent trace-pairing definition and establish which factor is discarded. When factors have equal dimension, tracing the wrong one can pass every matrix-size check.

Associating three factors as $(H_A\otimes H_B)\otimes H_C$ or $H_A\otimes(H_B\otimes H_C)$ also requires a declared identification. Swapping factors is a unitary map, not equality of every coordinate array. Such transport maps make circuit and channel proofs preserve the identity of each subsystem.

Separate exact semantics from executable approximations

An abstract complex number is not automatically a finite floating-point datum. A formal existence theorem or exact matrix identity can use arbitrary complex parameters without providing a numerical evaluator for them. An executable implementation may restrict entries, approximate functions, and accumulate roundoff. Relating those results to exact semantics requires an error statement and its own proof or certified bound.

Verified Examples uses exact rational and algebraic entries for small checks. Quantum Information Theorems in Proof Assistants explains how a general semantic interface can support proofs for whole families of circuits.

Exercise: detect a same-size subsystem error

For $\rho=|0\rangle\langle0|_A\otimes|1\rangle\langle1|_B$ with two qubits, compute both partial traces. Why does this input test something that a maximally mixed state would miss?

Solution

Tracing $B$ gives $|0\rangle\langle0|$ on $A$; tracing $A$ gives $|1\rangle\langle1|$ on $B$. Both arrays are $2\times2$, but their diagonal entries differ. A maximally mixed bipartite state gives the same $I/2$ for either marginal and cannot reveal that factor swap. A useful finite test therefore respects the semantic distinction the general formal theorem must prove.

References

• Hietala, Kesha, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks, “A Verified Optimizer for Quantum Circuits,” Proceedings of the ACM on Programming Languages 5, POPL (2021), doi:10.1145/3434318 — symbolic matrix semantics for parameterized circuit proofs.
• Unruh, Dominique, “Quantum and Classical Registers,” Archive of Formal Proofs, 28 October 2021, formal development — subsystem interfaces and their composition.
• Watrous, John, The Theory of Quantum Information, Cambridge University Press, 2018, doi:10.1017/9781316848142 — states, channels, and basis-independent definitions.