Documentation

CsdLean4.Empirical.QM.USD

Empirical/QM: unambiguous state discrimination (the IDP POVM) #

Category: 3-Local. The POVM-essential QM-validity result: distinguishing two non-orthogonal pure states with zero error, at the cost of an inconclusive outcome — provably impossible with a projective (von Neumann) measurement, the canonical "why POVMs are needed" example (Ivanovic 1987, Dieks 1988, Peres 1988).

Setup #

Two non-orthogonal states with real overlap s = ⟨ψ₁, ψ₂⟩ ∈ [0, 1): ψ₁ = |0⟩, ψ₂ = s|0⟩ + σ|1⟩ with σ = √(1−s²). The conclusive effects are scaled rank-1 projectors onto the orthogonal complements:

E₁ = a |ψ₂^⊥⟩⟨ψ₂^⊥|   ("conclude state 1"),   E₂ = a |ψ₁^⊥⟩⟨ψ₁^⊥|   ("conclude 2"),

with a = 1/(1+s) (the optimal Ivanovic–Dieks–Peres coefficient), ψ₁^⊥ = |1⟩, ψ₂^⊥ = −σ|0⟩ + s|1⟩. The third, inconclusive, effect is the rank-1 projector E? = |χ?⟩⟨χ?| = I − E₁ − E₂ with χ? = √s|0⟩ + (σ√s/(1+s))|1⟩; its positivity (hence the validity of the POVM) is exactly the completeness constraint, satisfied at a = 1/(1+s).

What this file proves #

Unambiguity (the defining no-error property): ⟨ψ₂, E₁ ψ₂⟩ = 0 and ⟨ψ₁, E₂ ψ₁⟩ = 0 — outcome "1" never fires on state 2 and vice versa, because each conclusive effect lives on the orthogonal complement of the other state.
Success probability: ⟨ψ₁, E₁ ψ₁⟩ = 1 − s — the IDP success rate.
Completeness: E₁ + E₂ + |χ?⟩⟨χ?| = I (usd_complete), giving the full three-outcome usdPOVM : POVM 2 (Fin 3) — a genuine non-projective POVM realising zero-error discrimination of the two non-orthogonal states.

The unambiguity is exactly the POVM-essential content: a projective measurement cannot have an informative outcome that gives identically zero on a non-orthogonal state while leaving room for a second such outcome.

The USD states and conclusive effects #

noncomputable def CSD.Empirical.QM.USD.sig (s : ℝ) :

σ = √(1 − s²).

Equations

CSD.Empirical.QM.USD.sig s = √(1 - s ^ 2)

Instances For

noncomputable def CSD.Empirical.QM.USD.psi1 :

EuclideanSpace ℂ (Fin 2)

ψ₁ = |0⟩.

Equations

CSD.Empirical.QM.USD.psi1 = EuclideanSpace.single 0 1

Instances For

noncomputable def CSD.Empirical.QM.USD.psi2 (s : ℝ) :

EuclideanSpace ℂ (Fin 2)

ψ₂ = s|0⟩ + σ|1⟩ (overlap ⟨ψ₁,ψ₂⟩ = s).

Equations

CSD.Empirical.QM.USD.psi2 s = EuclideanSpace.single 0 ↑s + EuclideanSpace.single 1 ↑(CSD.Empirical.QM.USD.sig s)

Instances For

noncomputable def CSD.Empirical.QM.USD.psi1perp :

EuclideanSpace ℂ (Fin 2)

ψ₁^⊥ = |1⟩.

Equations

CSD.Empirical.QM.USD.psi1perp = EuclideanSpace.single 1 1

Instances For

noncomputable def CSD.Empirical.QM.USD.psi2perp (s : ℝ) :

EuclideanSpace ℂ (Fin 2)

ψ₂^⊥ = −σ|0⟩ + s|1⟩.

Equations

CSD.Empirical.QM.USD.psi2perp s = EuclideanSpace.single 0 ↑(-CSD.Empirical.QM.USD.sig s) + EuclideanSpace.single 1 ↑s

Instances For

theorem CSD.Empirical.QM.USD.sig_sq (s : ℝ) (hs1 : s ≤ 1) (hs0 : -1 ≤ s) :

sig s ^ 2 = 1 - s ^ 2

Component values and inner products #

theorem CSD.Empirical.QM.USD.inner_two (x y : EuclideanSpace ℂ (Fin 2)) :

inner ℂ x y = star (x.ofLp 0) * y.ofLp 0 + star (x.ofLp 1) * y.ofLp 1

theorem CSD.Empirical.QM.USD.psi1_ofLp :

psi1.ofLp 0 = 1 ∧ psi1.ofLp 1 = 0

theorem CSD.Empirical.QM.USD.psi1perp_ofLp :

psi1perp.ofLp 0 = 0 ∧ psi1perp.ofLp 1 = 1

theorem CSD.Empirical.QM.USD.psi2_ofLp (s : ℝ) :

(psi2 s).ofLp 0 = ↑s ∧ (psi2 s).ofLp 1 = ↑(sig s)

theorem CSD.Empirical.QM.USD.psi2perp_ofLp (s : ℝ) :

(psi2perp s).ofLp 0 = ↑(-sig s) ∧ (psi2perp s).ofLp 1 = ↑s

theorem CSD.Empirical.QM.USD.psi1_norm :

‖psi1 ‖ = 1

theorem CSD.Empirical.QM.USD.psi1perp_norm :

‖psi1perp ‖ = 1

theorem CSD.Empirical.QM.USD.psi2_norm (s : ℝ) (hs1 : s ≤ 1) (hs0 : -1 ≤ s) :

‖psi2 s‖ = 1

theorem CSD.Empirical.QM.USD.psi2perp_norm (s : ℝ) (hs1 : s ≤ 1) (hs0 : -1 ≤ s) :

‖psi2perp s‖ = 1

theorem CSD.Empirical.QM.USD.inner_psi2_psi2perp (s : ℝ) :

inner ℂ (psi2 s) (psi2perp s) = 0

⟨ψ₂, ψ₂^⊥⟩ = 0 — the orthogonality behind the unambiguity of outcome 1.

theorem CSD.Empirical.QM.USD.inner_psi1_psi1perp :

inner ℂ psi1 psi1perp = 0

⟨ψ₁, ψ₁^⊥⟩ = 0 — orthogonality behind the unambiguity of outcome 2.

theorem CSD.Empirical.QM.USD.inner_psi1_psi2perp (s : ℝ) :

inner ℂ psi1 (psi2perp s) = ↑(-sig s)

⟨ψ₁, ψ₂^⊥⟩ = −σ — the overlap driving the success probability.

The USD effects, unambiguity, and success #

noncomputable def CSD.Empirical.QM.USD.usdA (s : ℝ) :

The optimal IDP coefficient a = 1/(1+s).

Equations

CSD.Empirical.QM.USD.usdA s = 1 / (1 + s)

Instances For

theorem CSD.Empirical.QM.USD.usdA_nonneg (s : ℝ) (hs0 : 0 ≤ s) :

theorem CSD.Empirical.QM.USD.usdA_le_one (s : ℝ) (hs0 : 0 ≤ s) :

noncomputable def CSD.Empirical.QM.USD.E1 (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

E₁ = a|ψ₂^⊥⟩⟨ψ₂^⊥| — the "conclude state 1" effect.

Equations

CSD.Empirical.QM.USD.E1 s hs0 hs1 = CSD.LF2.scaledRankOneEffect (CSD.Empirical.QM.USD.usdA s) ⋯ ⋯ (CSD.Empirical.QM.USD.psi2perp s) ⋯

Instances For

noncomputable def CSD.Empirical.QM.USD.E2 (s : ℝ) (hs0 : 0 ≤ s) :

E₂ = a|ψ₁^⊥⟩⟨ψ₁^⊥| — the "conclude state 2" effect.

Equations

CSD.Empirical.QM.USD.E2 s hs0 = CSD.LF2.scaledRankOneEffect (CSD.Empirical.QM.USD.usdA s) ⋯ ⋯ CSD.Empirical.QM.USD.psi1perp CSD.Empirical.QM.USD.psi1perp_norm

Instances For

theorem CSD.Empirical.QM.USD.usd_unambiguous_1 (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

RCLike.re (inner ℂ (psi2 s) ((Matrix.toEuclideanLin (E1 s hs0 hs1).M) (psi2 s))) = 0

Unambiguity (outcome 1): ⟨ψ₂, E₁ ψ₂⟩ = 0 — concluding "state 1" never fires on state 2, because E₁ lives on the orthogonal complement of ψ₂.

theorem CSD.Empirical.QM.USD.usd_unambiguous_2 (s : ℝ) (hs0 : 0 ≤ s) :

RCLike.re (inner ℂ psi1 ((Matrix.toEuclideanLin (E2 s hs0).M) psi1)) = 0

Unambiguity (outcome 2): ⟨ψ₁, E₂ ψ₁⟩ = 0.

theorem CSD.Empirical.QM.USD.usd_success (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

RCLike.re (inner ℂ psi1 ((Matrix.toEuclideanLin (E1 s hs0 hs1).M) psi1)) = 1 - s

Success probability: ⟨ψ₁, E₁ ψ₁⟩ = 1 − s (the Ivanovic–Dieks–Peres rate).

The inconclusive effect and the full POVM #

noncomputable def CSD.Empirical.QM.USD.chiInc (s : ℝ) :

EuclideanSpace ℂ (Fin 2)

The inconclusive-outcome vector χ? = √s|0⟩ + (σ√s/(1+s))|1⟩, with E? = |χ?⟩⟨χ?| = I − E₁ − E₂.

Equations

CSD.Empirical.QM.USD.chiInc s = EuclideanSpace.single 0 ↑√s + EuclideanSpace.single 1 ↑(CSD.Empirical.QM.USD.sig s * √s / (1 + s))

Instances For

theorem CSD.Empirical.QM.USD.chiInc_ofLp (s : ℝ) :

(chiInc s).ofLp 0 = ↑√s ∧ (chiInc s).ofLp 1 = ↑(sig s * √s / (1 + s))

theorem CSD.Empirical.QM.USD.outer_apply (φ : EuclideanSpace ℂ (Fin 2)) (i j : Fin 2) :

LF2.outerProduct φ i j = φ.ofLp i * star (φ.ofLp j)

theorem CSD.Empirical.QM.USD.usd_complete (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

(E1 s hs0 hs1).M + (E2 s hs0).M + LF2.outerProduct (chiInc s) = 1

Completeness: E₁ + E₂ + |χ?⟩⟨χ?| = I at the optimal a = 1/(1+s). The trine of orthogonal-complement projectors completes to the identity.

noncomputable def CSD.Empirical.QM.USD.Einc (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

E? = |χ?⟩⟨χ?| as an Effect (the inconclusive outcome). PSD as a rank-1 projector; ≤ I because I − E? = E₁ + E₂ is a sum of PSD effects.

Equations

CSD.Empirical.QM.USD.Einc s hs0 hs1 = { M := CSD.LF2.outerProduct (CSD.Empirical.QM.USD.chiInc s), isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

Instances For

noncomputable def CSD.Empirical.QM.USD.usdPOVM (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :

LF2.POVM 2 (Fin 3)

The USD POVM {E₁, E₂, E?} — the three-outcome unambiguous-discrimination measurement (two conclusive outcomes + one inconclusive), a genuine non-projective POVM realising zero-error discrimination of the two non-orthogonal states.

Equations

CSD.Empirical.QM.USD.usdPOVM s hs0 hs1 = { E := ![CSD.Empirical.QM.USD.E1 s hs0 hs1, CSD.Empirical.QM.USD.E2 s hs0, CSD.Empirical.QM.USD.Einc s hs0 hs1], complete := ⋯ }

Instances For