Diagonal Phase Blindness

Abstract

Diagonal observable families cannot recover relative phase without a non-diagonal interface.

Theorem 1.1 (Diagonal observables cannot recover relative phase).

$$\begin{array}{r}\forall I:\mathrm{Type},\\ (\forall observable:I\to QubitMatrix,(\forall i:I,\mathrm{IsDiag}\left(\mathrm{observable}\left(i\right)\right))\Rightarrow \\ equalSuperpositionDensity\ne \mathrm{mul}\left(\mathrm{mul}\left(qubitZ,equalSuperpositionDensity\right),qubitZ\right)\wedge \mathrm{apply}\left(\mathrm{jointReadout}\left(\mathrm{fun}\left(i,rho,\mathrm{bornProbability}\left(rho,\mathrm{observable}\left(i\right)\right)\right)\right),equalSuperpositionDensity\right)=\mathrm{apply}\left(\mathrm{jointReadout}\left(\mathrm{fun}\left(i,rho,\mathrm{bornProbability}\left(rho,\mathrm{observable}\left(i\right)\right)\right)\right),\mathrm{mul}\left(\mathrm{mul}\left(qubitZ,equalSuperpositionDensity\right),qubitZ\right)\right))\\ \wedge (\forall A:QubitMatrix,\mathrm{bornProbability}\left(equalSuperpositionDensity,A\right)\ne \mathrm{bornProbability}\left(\mathrm{mul}\left(\mathrm{mul}\left(qubitZ,equalSuperpositionDensity\right),qubitZ\right),A\right)\Rightarrow \neg \mathrm{IsDiag}\left(A\right))\\ \wedge (\neg \mathrm{IsDiag}\left(qubitX\right)\wedge \mathrm{bornProbability}\left(equalSuperpositionDensity,qubitX\right)\ne \mathrm{bornProbability}\left(\mathrm{mul}\left(\mathrm{mul}\left(qubitZ,equalSuperpositionDensity\right),qubitZ\right),qubitX\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The equal superposition density and its conjugate by the canonical phase flip are distinct. Every indexed family of diagonal matrices gives the same joint trace-expectation readout on this pair, regardless of the size of the index type.

The second public clause uses the same pair: any matrix whose expectation separates the two states cannot be diagonal. The canonical Pauli X matrix supplies such a non-diagonal interface explicitly.

The family readout, trace expectation, diagonal predicate, states, and interface are existing repository or pinned-library primitives; no parallel observation carrier is introduced.

References

• Truth anchor: D5/S3/Quantum/Tomography/DiagonalPhaseBlindness.diagonal_prime_observables_cannot_recover_relative_phase
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/Quantum/QubitWitnesses