Deterministic Readout Commutativity

Abstract

Deterministic readout projections share a diagonal basis, while general quantum observables need not commute.

Theorem 1.1 (Common-basis projections commute; a qubit pair is noncommuting).

$$\forall X:\mathrm{Type},O:\mathrm{Type},I:\mathrm{Type},[\mathrm{Fintype}(X)],[\mathrm{DecidableEq}(X)],[\mathrm{DecidableEq}(O)],q:I\to X\to O\Rightarrow \forall i:I,j:I,o:O,op:O,\mathrm{deterministicProjection}(q(i),o)\circ \mathrm{deterministicProjection}(q(j),op)=\mathrm{deterministicProjection}(q(j),op)\circ \mathrm{deterministicProjection}(q(i),o)\wedge \exists P,Q:\mathrm{QubitMatrix}(),\mathrm{star}(P)=P\wedge \mathrm{star}(Q)=Q\wedge P\circ P=I\wedge Q\circ Q=I\wedge P\circ Q\ne Q\circ P.$$

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

Source. Repository-derived.

Commentary.

Every deterministic interface is represented by diagonal indicators of its readout fibers in one standard basis, so all such projections commute.

The reverse inclusion fails: the Pauli qubit pair is self-adjoint, squares to the identity, and has unequal products in the two orders.

References

• Truth anchor: D5/S3/Quantum/Measurements/DeterministicReadoutCommutativity.deterministic_readout_commutes_and_quantum_counterexample
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/Quantum/Measurements/DeterministicReadoutPvm