Purity Pythagoras Decomposition

Abstract

Pairwise orthogonal basis measurements split density-matrix purity excess into visible probability energy and orthogonal residual mass.

Theorem 1.1 (The complex matrix inner product is a trace pairing).

$$\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),\forall (C:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),\mathrm{inner}\left(\mathbb{C},A,C\right)=\mathrm{trace}\left(\mathrm{conjTranspose}\left(A\right)\cdot C\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.matrix_inner_eq_trace_conjTranspose_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Hilbert–Schmidt inner product of two square complex matrices is the trace of the conjugate transpose of the first times the second. This identity applies in every natural dimension, including zero.

Theorem 1.2 (Products of Hermitian matrices have real trace).

$$\forall (d:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),\forall (C:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\mathrm{IsHermitian}\left(A\right))\Rightarrow ((\mathrm{IsHermitian}\left(C\right))\Rightarrow (\mathrm{trace}\left(A\cdot C\right)=(\mathrm{re}\left(\mathrm{trace}\left(A\cdot C\right)\right):\mathbb{C})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.trace_mul_real_of_hermitian (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two Hermitian factors need not commute. Taking the conjugate of their product trace reverses their order, and cyclicity of trace restores the original value. Thus the complex trace is its real part embedded into the complex numbers.

Theorem 1.3 (Centering removes the squared scalar trace component).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}\left(d\right)]\forall (H:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\mathrm{IsHermitian}\left(H\right))\Rightarrow ((\Vert H-\mathrm{smul}\left(\frac{\mathrm{trace}\left(H\right)}{(d:\mathbb{C})},(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right))\right)\Vert {)}^2=\mathrm{re}\left(\mathrm{trace}\left(H\cdot H\right)\right)-\frac{(\mathrm{re}\left(\mathrm{trace}\left(H\right)\right){)}^2}{(d:\mathbb{R})})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.centered_hermitian_norm_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Hermitian matrix in nonzero dimension, subtracting trace(H)/d times the identity removes exactly (real trace H) squared divided by d from its squared Hilbert–Schmidt norm. The trace is real and the remaining matrix has trace zero.

Theorem 1.4 (Measurement energy is the sum of squared trace coordinates).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}\left(d\right)]\forall (B:\mathrm{RankOneContext}\left(d\right)),(\mathrm{IsRecordMeasurement}\left(\mathrm{projector}\left(B\right)\right))\Rightarrow (\forall (X:\mathrm{traceZeroHermitian}\left(d\right)),(\Vert \sum _{j:\mathrm{Fin}\left(d\right)}(\mathrm{projector}\left(B,j\right)\cdot (X).1.1\cdot \mathrm{projector}\left(B,j\right))\Vert {)}^2=\sum _{j:\mathrm{Fin}\left(d\right)}((\mathrm{re}\left(\mathrm{trace}\left((X).1.1\cdot \mathrm{projector}\left(B,j\right)\right)\right){)}^2))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.traceZero_measurement_norm_sq (✓ std3). ∎

Source. Repository-derived.

Commentary.

A trace-zero Hermitian matrix X is a Hermitian matrix with trace zero, represented by its underlying matrix X.1.1. For a complete rank-one record context, its measured matrix is the sum of P_j X P_j. The rank-one compression identity expresses this as a sum of trace coordinates times P_j, and these projectors are orthonormal in the Hilbert–Schmidt inner product. Its squared norm is therefore the sum of squared real trace coordinates.

Theorem 1.5 (Orthogonal contexts split every trace-zero Hermitian matrix).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}\left(d\right)]\forall (L:Type\ast ),[\mathrm{Fintype}\left(L\right)]\forall (C:(L\to \mathrm{RankOneContext}\left(d\right))),(\forall (l:L),\mathrm{IsRecordMeasurement}\left(\mathrm{projector}\left(C\left(l\right)\right)\right))\Rightarrow ((\forall (l:L),\forall (k:L),(l\ne k)\Rightarrow (\forall (x:\mathrm{traceZeroHermitian}\left(d\right)),\forall (y:\mathrm{traceZeroHermitian}\left(d\right)),\mathrm{inner}\left(\mathbb{R},\sum _{j:\mathrm{Fin}\left(d\right)}(\mathrm{projector}\left(C\left(l\right),j\right)\cdot (x).1.1\cdot \mathrm{projector}\left(C\left(l\right),j\right)),\sum _{j:\mathrm{Fin}\left(d\right)}(\mathrm{projector}\left(C\left(k\right),j\right)\cdot (y).1.1\cdot \mathrm{projector}\left(C\left(k\right),j\right))\right)=0))\Rightarrow (\forall (s:\mathrm{traceZeroHermitian}\left(d\right)),(\Vert (s).1.1\Vert {)}^2=\sum _{l:L}((\Vert \sum _{j:\mathrm{Fin}\left(d\right)}(\mathrm{projector}\left(C\left(l\right),j\right)\cdot (s).1.1\cdot \mathrm{projector}\left(C\left(l\right),j\right))\Vert {)}^2)+(\Vert (s).1.1-\sum _{l:L}(\sum _{j:\mathrm{Fin}\left(d\right)}(\mathrm{projector}\left(C\left(l\right),j\right)\cdot (s).1.1\cdot \mathrm{projector}\left(C\left(l\right),j\right)))\Vert {)}^2))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.traceZero_context_pythagoras (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each context is a family of normalized Hermitian rank-one idempotents resolving the identity. A record context has pairwise orthogonal projectors. Assume that the measurement images of distinct contexts are mutually orthogonal for the real Hilbert–Schmidt inner product; this is the expanded hypothesis below. The underlying trace-zero Hermitian matrix then splits into the sum of all measured components and their orthogonal residual. The formula expands each measured component as its compression sum and the residual as the original matrix minus the sum of these components. No positivity or trace-one assumption is imposed on the input.

Lemma 1.6 (Every visible measurement is orthogonal to the residual).

$$\begin{gathered} \mathrm{RankOneContextFamily}\left(C,d\right)\wedge \mathrm{RecordMeasurements}\left(C\right)\wedge \mathrm{PairwiseOrthogonalMeasurements}\left(C\right)\Rightarrow \\ \forall l,x,s:\mathrm{traceZeroHermitian}\left(d\right),\mathrm{innerR}\left(\mathrm{traceZeroBasisMeasurement}\left(\mathrm{context}\left(C,l\right),x\right),\mathrm{residualVector}\left(C,s\right)\right)=0. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.measurement_inner_residualVector (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let C be a finite family of complete rank-one record measurements on the trace-zero Hermitian space. Assume the ranges of the corresponding real orthogonal projections are pairwise orthogonal.

For any chosen context, projected test vector, and state, the real Hilbert–Schmidt inner product of that visible component with the state minus the sum of all visible components is zero. Thus the defined residual lies in the orthogonal complement of every visible measurement image.

Symmetry and idempotence identify the selected context’s contribution with its pairing against the original state, while pairwise orthogonality removes every cross-context contribution.

Theorem 1.7 (Purity excess splits into visible and residual mass).

$$\begin{gathered} \mathrm{NormalizedDensity}\left(\rho ,d\right)\wedge \mathrm{RecordMeasurements}\left(C\right)\wedge \mathrm{PairwiseOrthogonalMeasurements}\left(C\right)\Rightarrow \\ \mathrm{ReTr}\left({\rho }^2\right)-\frac{1}{d}= \\ \sum _l\sum _j{\mathrm{basisProbability}\left(\rho ,\mathrm{context}\left(C,l\right),j\right)-\frac{1}{d}}^2+\mathrm{purityResidual}\left(C,\mathrm{centeredDensity}\left(\rho \right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.purity_pythagoras_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let rho be a positive semidefinite complex matrix of trace one in dimension d. Centering it by the maximally mixed state produces a trace-zero Hermitian vector whose squared Hilbert–Schmidt norm is the real trace purity minus the inverse dimension.

For each complete rank-one record context, the squared norm of its visible projection is the sum over outcomes of the squared Born probability deviations from the uniform value. Pairwise orthogonality makes these visible energies add without cross terms.

The preceding residual-orthogonality result then gives an exact Pythagorean split: purity excess equals the double sum of visible probability energies plus the squared norm of the remaining component. The family need not be tomographically complete; any unseen mass is retained by the nonnegative residual term.

References

• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.centered_hermitian_norm_sq
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.matrix_inner_eq_trace_conjTranspose_mul
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.measurement_inner_residualVector
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.purity_pythagoras_decomposition
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.traceZero_context_pythagoras
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.traceZero_measurement_norm_sq
• Truth anchor: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition.trace_mul_real_of_hermitian
• Dependency: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence
• Dependency: D5/S3/Quantum/Measurement/BasisMeasurementProjection