LF2: POVMs (positive operator-valued measures)

Category: 3-Local (LF2 matrix-based POVM built on the Effect type).

A POVM on an N-dimensional complex Hilbert space is a finite family of effects {Eᵢ} that sum to the identity — the most general (non-projective) quantum measurement. This file gives the type, the Born weight pᵢ(ψ) = ⟨ψ, Eᵢ ψ⟩, and the completeness identity ∑ᵢ pᵢ(ψ) = ‖ψ‖².

This is P.1 of the POVM tranche (specs/povm-plan.md): the type the Naimark dilation (LF4/POVMDilation.lean) and the ontic volume reading hang off.

The Born weight is taken in the EuclideanSpace/toEuclideanLin form re ⟨ψ, Eᵢ ψ⟩ — matching Empirical/QM/Bell.lean's expectation form and the fs_born_volume_ratio_N projective-Born surface — so the dilation transfer (born_transfer) composes cleanly through the matrix↔operator adjoint bridge.

structure CSD.LF2.POVM (N : ℕ) (ι : Type u_2) [Fintype ι] : Type u_2

POVM on an N-dimensional complex Hilbert space. A finite family of Effects (Hermitian, 0 ≤ Eᵢ ≤ I) that sum to the identity. The completeness relation ∑ᵢ Eᵢ = I is what makes {⟨ψ, Eᵢ ψ⟩}ᵢ a probability vector.

• E : ι → Effect N

  The effect family.

• complete : ∑ i : ι, (self.E i).M = 1

  Completeness: the effects sum to the identity.

noncomputable def CSD.LF2.POVM.weight {N : ℕ} {ι : Type u_1} [Fintype ι] (P : POVM N ι) (ψ : EuclideanSpace ℂ (Fin N)) (i : ι) : ℝ

POVM Born weight pᵢ(ψ) = ⟨ψ, Eᵢ ψ⟩ (real, via re; Eᵢ Hermitian makes the inner product real). The probability the i-th outcome occurs on preparation ψ.

Equations

• P.weight ψ i = RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (P.E i).M) ψ))

theorem CSD.LF2.POVM.weights_sum_eq_normSq {N : ℕ} {ι : Type u_1} [Fintype ι] (P : POVM N ι) (ψ : EuclideanSpace ℂ (Fin N)) : ∑ i : ι, P.weight ψ i = ‖ψ‖ ^ 2

Completeness of the Born weights. ∑ᵢ pᵢ(ψ) = ‖ψ‖², so on a unit vector the POVM Born weights form a probability distribution. Routes through ∑ᵢ Eᵢ = I (complete) and ⟨ψ, ψ⟩ = ‖ψ‖².

theorem CSD.LF2.POVM.weights_sum_eq_one {N : ℕ} {ι : Type u_1} [Fintype ι] (P : POVM N ι) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) : ∑ i : ι, P.weight ψ i = 1

Born weights of a unit preparation sum to one.

theorem CSD.LF2.POVM.weight_nonneg {N : ℕ} {ι : Type u_1} [Fintype ι] (P : POVM N ι) (ψ : EuclideanSpace ℂ (Fin N)) (i : ι) : 0 ≤ P.weight ψ i

Per-outcome nonnegativity of the Born weights (the CL-006 named API test, landed 2026-08-20): every POVM weight is nonnegative — the effect's positivity read through the quadratic form. Together with weights_sum_eq_one, the weights of a unit preparation form a genuine probability vector.