Recording Isometry

Abstract

The canonical projective recording map is isometric and exposes every state block.

Theorem 1.1 (Projective recording is isometric with explicit state blocks).

$$\forall S\in Type,A\in Type,\left(\mathrm{Fintype}\left(S\right)\wedge \left(\mathrm{DecidableEq}\left(S\right)\wedge \left(\mathrm{Fintype}\left(A\right)\wedge \mathrm{DecidableEq}\left(A\right)\right)\right)\right)\Rightarrow \left(\forall P\in A\to \mathrm{Matrix}\left(S,S,\mathbb{C}\right),\left(\left(\forall a\in A,P{\left(a\right)}^{\ast }=P\left(a\right)\right)\wedge \left(\left(\forall a\in A,b\in A,P\left(a\right)\cdot P\left(b\right)=\mathrm{ite}\left(a=b,P\left(a\right),0\right)\right)\wedge \sum _{a\in A}P\left(a\right)=I\right)\right)\Rightarrow \mathrm{let}V:\mathrm{Matrix}\left(S\times A,S,\mathbb{C}\right),\forall i:S,a:A,j:S,\mathrm{entry}\left(V,\mathrm{pair}\left(i,a\right),j\right)=\mathrm{entry}\left(P\left(a\right),i,j\right);V^{\ast }\cdot V=I\wedge \left(\forall rho\in \mathrm{Matrix}\left(S,S,\mathbb{C}\right),a\in A,b\in A,i\in S,j\in S,\mathrm{entry}\left(V\cdot \rho \cdot V^{\ast },\mathrm{pair}\left(i,a\right),\mathrm{pair}\left(j,b\right)\right)=\mathrm{entry}\left(P\left(a\right)\cdot \rho \cdot P\left(b\right),i,j\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/RecordingIsometry.recording_isometry_and_state_blocks (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite system and outcome carriers have decidable equality. The supplied matrices are self-adjoint orthogonal projectors whose sum is the identity.

The recording matrix is defined on the product basis by V((i,a),j) = P(a)(i,j). Its adjoint product is the identity, and conjugating any complex system matrix yields the displayed P(a) rho P(b) block.

References

• Truth anchor: D5/S3/Quantum/Decoherence/RecordingIsometry.recording_isometry_and_state_blocks