Unread-State Orthogonal Projection

Abstract

Unread measurement projects orthogonally onto block-diagonal matrices.

Theorem 1.1 (Unread measurement is the block-diagonal orthogonal projection).

$$\begin{array}{c}\forall n,\kappa ,P:\kappa \to M_n(\mathbb{C}),\mathrm{Finite}\left(n\right),\mathrm{Finite}\left(\kappa \right),\\ \mathrm{CompleteOrthogonalProjectionFamily}\left(P\right),(\forall X\in M_n(\mathbb{C}),{\mathcal{D}}_P(X)=\sum _i{P}_{i}X{P}_i),\\ {\mathcal{B}}_P=\{X\mid \forall i,j,i\ne j\Rightarrow P_{i}X{P}_j=0\},\\ \Rightarrow \\ (\forall X,{\mathcal{D}}_P({\mathcal{D}}_P(X))={\mathcal{D}}_P(X))\wedge \\ (\forall X,Y,⟨{\mathcal{D}}_P(X),Y{⟩}_{HS}=⟨X,{\mathcal{D}}_P(Y){⟩}_{HS})\wedge \\ \mathrm{range}\left({\mathcal{D}}_P\right)={\mathcal{B}}_P\wedge \\ (\forall X,X={\mathcal{D}}_P(X)+(X-{\mathcal{D}}_P(X))\wedge ⟨{\mathcal{D}}_P(X),X-{\mathcal{D}}_P(X){⟩}_{HS}=0)\wedge \\ (\forall X,{\Vert X\Vert }_{HS}^2={\Vert {\mathcal{D}}_P(X)\Vert }_{HS}^2+{\Vert X-{\mathcal{D}}_P(X)\Vert }_{HS}^2).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Conditioning/UnreadStateOrthogonalProjection.unread_state_orthogonal_projection (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let P be a finite complete family of pairwise orthogonal self-adjoint idempotent complex matrix projections. The unread measurement channel is constructed as the sum of the compressed blocks P_i X P_i; it is not defined from the target range.

The channel is idempotent and self-adjoint for the trace pairing. Its range is exactly the matrices whose P_i X P_j cross blocks vanish when i and j differ.

Every matrix splits into its unread image and discarded residual. These two named components are Hilbert–Schmidt orthogonal, and the existing trace definition of squared Hilbert–Schmidt norm gives the displayed Pythagorean identity.

References

• Truth anchor: D5/S3/Observer/Conditioning/UnreadStateOrthogonalProjection.unread_state_orthogonal_projection
• Dependency: D5/S3/Observer/Conditioning
• Dependency: D5/S3/Quantum/Tomography/RankOneContextCommutator