Sharp-Measurement Compatibility

Abstract

Joint sharp measurements are exactly pairwise commuting, while general effects need not commute.

Theorem 1.1 (Sharp measurements are jointly measurable exactly when they commute).

$$\begin{gathered} \forall n\in \mathrm{Type}\left(\right),A\in \mathrm{Type}\left(\right),B\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)][\mathrm{Fintype}\left(A\right)][\mathrm{Fintype}\left(B\right)],\forall P:A\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right),Q:B\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right), \\ \begin{array}{c}\mathrm{IsRecordMeasurement}\left(P\right)\wedge \mathrm{IsRecordMeasurement}\left(Q\right)\Rightarrow \\ (\left(\exists R\in A\times B\to \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\mathrm{IsRecordMeasurement}\left(R\right)\wedge \left(\left(\forall a\in A,P\left(a\right)=\sum _{b\in B}R\left(\mathrm{pair}\left(a,b\right)\right)\right)\wedge \left(\forall b\in B,Q\left(b\right)=\sum _{a\in A}R\left(\mathrm{pair}\left(a,b\right)\right)\right)\right)\right)\iff \left(\forall a\in A,b\in B,P\left(a\right)\cdot Q\left(b\right)=Q\left(b\right)\cdot P\left(a\right)\right))\wedge \\ \mathrm{let}zPlus:\mathrm{QubitState}\left(\right):=vec2\left(1,0\right);\\ \mathrm{let}zMinus:\mathrm{QubitState}\left(\right):=vec2\left(0,1\right);\\ \mathrm{let}xPlus:\mathrm{QubitState}\left(\right):=vec2\left(1,1\right);\\ \mathrm{let}xMinus:\mathrm{QubitState}\left(\right):=vec2\left(1,-1\right);\\ \mathrm{let}joint:Bool\times Bool\to \mathrm{QubitMatrix}\left(\right),joint\left(\mathrm{pair}\left(false,false\right)\right)=\frac{1}{2}\cdot \mathrm{vecMulVec}\left(zPlus,\mathrm{star}\left(zPlus\right)\right),joint\left(\mathrm{pair}\left(false,true\right)\right)=\frac{1}{4}\cdot \mathrm{vecMulVec}\left(xPlus,\mathrm{star}\left(xPlus\right)\right),joint\left(\mathrm{pair}\left(true,false\right)\right)=\frac{1}{4}\cdot \mathrm{vecMulVec}\left(xMinus,\mathrm{star}\left(xMinus\right)\right),joint\left(\mathrm{pair}\left(true,true\right)\right)=\frac{1}{2}\cdot \mathrm{vecMulVec}\left(zMinus,\mathrm{star}\left(zMinus\right)\right);\\ \mathrm{let}first:Bool\to \mathrm{QubitMatrix}\left(\right),\forall a:Bool,first\left(a\right)=\sum _{b\in Bool}joint\left(\mathrm{pair}\left(a,b\right)\right);\\ \mathrm{let}second:Bool\to \mathrm{QubitMatrix}\left(\right),\forall b:Bool,second\left(b\right)=\sum _{a\in Bool}joint\left(\mathrm{pair}\left(a,b\right)\right);\\ \left(\forall o\in Bool\times Bool,\mathrm{PosSemidef}\left(joint\left(o\right)\right)\right)\wedge \left(\sum _{o\in Bool\times Bool}joint\left(o\right)=1\wedge \left(\left(\neg \mathrm{IsRecordMeasurement}\left(first\right)\right)\wedge \left(\left(\neg \mathrm{IsRecordMeasurement}\left(second\right)\right)\wedge first\left(false\right)\cdot second\left(false\right)\ne second\left(false\right)\cdot first\left(false\right)\right)\right)\right).\end{array} \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/SharpMeasurementCompatibility.sharp_measurement_compatibility (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two arbitrary finite record measurements admit a joint record measurement with the stated marginals exactly when every effect from the first family commutes with every effect from the second.

The forward direction expands both marginals and uses orthogonality of distinct joint outcomes. The reverse direction constructs each joint outcome as the product of the commuting effects.

The final clauses give one shared positive normalized qubit measurement. Both of its marginals are nonsharp, and their false-false effects do not commute. This records the source’s contrast with general nonsharp effects on the same public construction.

References

• Truth anchor: D5/S3/Quantum/Measurement/SharpMeasurementCompatibility.sharp_measurement_compatibility
• Dependency: D5/S3/Observer/Conditioning
• Dependency: D5/S3/Quantum/QubitWitnesses