Complete Context Purity Identities

Abstract

Complete complementary rank-one measurements express purity exactly in Born-probability coordinates.

Theorem 1.1 (Complete context purity identities).

$$\begin{gathered} \forall n:Nat,C:\mathrm{Fin}(n+2)\to \mathrm{RankOneContext}(n+1),\rho :\mathrm{Matrix}(\mathrm{Fin}(n+1),\mathrm{Fin}(n+1),\mathbb{C}), \\ (\forall l:\mathrm{Fin}(n+2),\mathrm{IsRecordMeasurement}(\mathrm{projector}(C_l)))\wedge \\ (\forall l,k:\mathrm{Fin}(n+2),j,r:\mathrm{Fin}(n+1), \\ \mathrm{Tr}(\mathrm{projector}(C_l,j)\cdot \mathrm{projector}(C_k,r))=\mathrm{if}(l=k,\mathrm{if}(j=r,1,0),\frac{1}{n+1}))\wedge \\ \mathrm{PosSemidefinite}(\rho )\wedge \mathrm{Tr}(\rho )=1\Rightarrow \\ (\sum _l\sum _j{\mathrm{basisProbability}(\rho ,C_l,j)-\frac{1}{n+1}}^2=\mathrm{ReTr}({\rho }^2)-\frac{1}{n+1})\wedge \\ (\sum _l\sum _j\mathrm{basisProbability}(\rho ,C_l,j{)}^2=1+\mathrm{ReTr}({\rho }^2)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CompleteContextPurityIdentities.complete_context_purity_identities (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take n+2 complete rank-one record measurements in dimension n+1. The public overlap equation gives Kronecker trace overlap within one context and constant inverse-dimension overlap between distinct contexts.

The overlap equation derives both pairwise orthogonality of the trace-zero measurement projections and reconstruction of every trace-zero Hermitian state. The existing probability Pythagoras theorem then has zero residual.

Each context’s Born coordinates sum to one. Expanding the centered squares across all n+2 contexts therefore gives the equivalent uncentered identity: the total squared probability is one plus the real trace purity.

References

• Truth anchor: D5/S3/Quantum/Measurements/CompleteContextPurityIdentities.complete_context_purity_identities
• Dependency: D5/S3/Quantum/Tomography/CompleteContextTomography
• Dependency: D5/S3/Quantum/Tomography/PurityPythagorasDecomposition