LF4: the canonical Naimark dilation of a POVM exists (P.5)

Category: 3-Local (LF4 POVM existence layer).

This is P.5 of the POVM tranche (specs/povm-plan.md): the construction that inhabits NaimarkDilation P for every POVM, making the Phase-1 results (born_transfer, povm_born_eq_dilated_volume, povm_born_frequency_volume) unconditional — no longer conditional on a supplied dilation.

The construction

The canonical Naimark isometry is V ψ = ∑ᵢ (√Eᵢ ψ) ⊗ |i⟩, i.e. the matrix V_{(n,i), m} = (√Eᵢ)_{n,m}, where √Eᵢ = cfc Real.sqrt Eᵢ is the positive square root via the continuous functional calculus on Matrix n n ℂ (the bespoke Hermitian CFC instance — P.5a is a library call, √Eᵢ √Eᵢ = Eᵢ by cfc_mul + √x·√x = x on the nonneg spectrum + cfc_id; no hand-built spectral construction). Then:

• isometry Vᴴ V = ∑ᵢ √Eᵢ √Eᵢ = ∑ᵢ Eᵢ = I (uses povmSqrt_mul_self and the POVM completeness ∑ Eᵢ = I);
• pullback Vᴴ Πᵢ V = √Eᵢ √Eᵢ = Eᵢ (the ancilla-i projector compresses to Eᵢ).

Both reduce to the same inner column sum ∑ₙ conj(√Eᵢ)_{n,m} (√Eᵢ)_{n,m'} = (Eᵢ)_{m,m'} (sqrt_inner_sum), using that √Eᵢ is Hermitian.

Honest scope

This removes the "supplied dilation" caveat: every POVM has a Naimark dilation, so the ontic POVM Born = Kähler-volume reading holds for every POVM. What remains posited is the enlarged sector structure on Σ' = ℂℙ^{N·|ι|−1} (the SO-1 sector datum on the dilated space — the ancilla is the apparatus/environment), and, beneath it, the dynamics (D1). The dilation is still non-canonical as a choice (Naimark dilations are non-unique); canonicalNaimark is one explicit, always-available inhabitant, not a forced one.

The positive square root of an effect

theorem CSD.LF4.povmSqrt_isHermitian {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) (i : ι) : (cfc Real.sqrt (P.E i).M).IsHermitian

√Eᵢ is Hermitian (any cfc of a real function is self-adjoint).

theorem CSD.LF4.povmSqrt_mul_self {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) (i : ι) : cfc Real.sqrt (P.E i).M * cfc Real.sqrt (P.E i).M = (P.E i).M

√Eᵢ √Eᵢ = Eᵢ (the defining square-root property; on spectrum ℝ Eᵢ ⊆ [0,∞), √x · √x = x, and cfc id Eᵢ = Eᵢ).

theorem CSD.LF4.povmSqrt_conj_entry {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) (i : ι) (n m : Fin N) : star (cfc Real.sqrt (P.E i).M n m) = cfc Real.sqrt (P.E i).M m n

Entry-level Hermitian symmetry: conj (√Eᵢ)_{n,m} = (√Eᵢ)_{m,n}.

theorem CSD.LF4.sqrt_inner_sum {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) (i : ι) (m m' : Fin N) : ∑ n : Fin N, star (cfc Real.sqrt (P.E i).M n m) * cfc Real.sqrt (P.E i).M n m' = (P.E i).M m m'

The common inner column sum: ∑ₙ conj(√Eᵢ)_{n,m} (√Eᵢ)_{n,m'} = (Eᵢ)_{m,m'}.

The canonical Naimark isometry

noncomputable def CSD.LF4.naimarkV {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) : Matrix (Fin N × ι) (Fin N) ℂ

The canonical Naimark isometry V_{(n,i), m} = (√Eᵢ)_{n,m}, i.e. V ψ = ∑ᵢ (√Eᵢ ψ) ⊗ |i⟩ as a matrix ℂ^N → ℂ^N ⊗ ℂ^ι.

Equations

• CSD.LF4.naimarkV P = Matrix.of fun (p : Fin N × ι) (m : Fin N) => cfc Real.sqrt (P.E p.2).M p.1 m

theorem CSD.LF4.naimarkV_isom {N : ℕ} {ι : Type u_1} [Fintype ι] (P : LF2.POVM N ι) : (naimarkV P).conjTranspose * naimarkV P = 1

V is an isometry: Vᴴ V = ∑ᵢ Eᵢ = I.

theorem CSD.LF4.blockProj_mul_naimarkV {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) (i : ι) (n : Fin N) (j : ι) (m : Fin N) : (blockProj N i * naimarkV P) (n, j) m = if j = i then cfc Real.sqrt (P.E i).M n m else 0

The action of the ancilla projector on V: (Πᵢ V)_{(n,j), m} = if j = i then (√Eᵢ)_{n,m} else 0.

theorem CSD.LF4.naimarkV_pullback {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) (i : ι) : (naimarkV P).conjTranspose * blockProj N i * naimarkV P = (P.E i).M

Naimark pullback: the ancilla-i projector compresses V back to the effect, Vᴴ Πᵢ V = Eᵢ.

noncomputable def CSD.LF4.canonicalNaimark {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) : NaimarkDilation P

Every POVM has a Naimark dilation. The canonical inhabitant of NaimarkDilation P, built from the CFC square roots √Eᵢ. ⚠️ Scope note 2026-08-04: "canonical" names this construction, not a uniqueness claim. Naimark dilations are genuinely non-unique (WV works for suitable unitary W), and no uniqueness or universal property is proved here. What is canonical about it is that cfc Real.sqrt is basis-independent. Consumers needing dilation-independence must say so: PovmDynamics.lean records the instrument as dilation-relative for exactly this reason. ⚠️ Scope note 2026-08-04: "canonical" names this construction, not a uniqueness claim. Naimark dilations are genuinely non-unique (WV works for suitable unitary W), and no uniqueness or universal property is proved here. What is canonical about it is that cfc Real.sqrt is basis-independent. Consumers needing dilation-independence must say so: PovmDynamics.lean records the instrument as dilation-relative for exactly this reason. This makes the Phase-1 ontic POVM Born = Kähler-volume results hold for every POVM, modulo the dilation genericity condition.

Equations

• CSD.LF4.canonicalNaimark P = { V := CSD.LF4.naimarkV P, isom := ⋯, pullback := ⋯ }