Pure Record Distinguishability and Coherence

Abstract

Normalized pure records obey exact distinguishability-coherence complementarity.

Theorem 1.1 (Pure-record distinguishability and coherence are complementary).

$$\begin{gathered} \forall E:{\mathrm{InnerProductSpace}}_{\mathbb{C}},e_L,e_R\in E,\Vert e_L\Vert =1\wedge \Vert e_R\Vert =1, \\ c=⟨e_L,e_R⟩,V=|c|,D=\sqrt{1-V^2}\Rightarrow \\ {D}^2+V^2=1\wedge \\ (c=0\Rightarrow D=1\wedge V=0)\wedge \\ (V=1\Rightarrow D=0\wedge V=1)\wedge \\ (D=1\Rightarrow V=0\wedge \forall \rho \in \mathbb{C},c\rho =0)\wedge \\ (V=1\Rightarrow D=0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/PureState/RecordCoherenceComplementarity.pure_record_distinguishability_coherence_complementarity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let eL and eR be normalized pure record vectors. Their overlap is c, the retained coherence is V = |c|, and the optimal equal-prior distinguishability is D = sqrt(1 - V^2).

The theorem retains the exact identity D^2 + V^2 = 1 and both overlap endpoints. Zero overlap gives perfect distinguishability and zero visibility; unit visibility gives zero distinguishability.

The operational consequence is explicit: perfect distinguishability forces c to annihilate every unread off-diagonal amplitude. Conversely, complete retained coherence leaves no distinguishability.

Loogle, LeanSearch, and the pinned Mathlib tree identify norm_inner_le_norm and Real.sq_sqrt as the exact declarations applied by the Lean proof.

References

• Truth anchor: D5/S3/Quantum/PureState/RecordCoherenceComplementarity.pure_record_distinguishability_coherence_complementarity