LF4: Naimark dilation of a POVM and the Born transfer

Category: 3-Local (LF4 dilation layer on the LF2 POVM type).

This is P.2 of the POVM tranche (specs/povm-plan.md): the abstract Naimark data and the Born transfer, the bridge that turns a (non-projective) POVM Born weight into a projective Born weight on a dilated space, where the achieved fs_born_volume_ratio_N result reads it as a Fubini–Study volume.

Naimark dilation

A POVM {Eᵢ} on ℂ^N is the compression of a projective measurement on the dilated space ℂ^N ⊗ ℂ^ι: there is an isometry V : ℂ^N → ℂ^N ⊗ ℂ^ι (Vᴴ V = I) such that Eᵢ = Vᴴ Πᵢ V, where Πᵢ = I_N ⊗ |i⟩⟨i| (blockProj i) is the rank-N ancilla-i projector. Then the Born transfer

⟨ψ, Eᵢ ψ⟩ = ⟨Vψ, Πᵢ (Vψ)⟩

makes the POVM weight the projective Born weight of the dilated state Vψ against Πᵢ — a coarse (rank-N) projective outcome, i.e. a union of rank-1 computational-basis cells on ℂℙ^{N·|ι|−1}.

NaimarkDilation P carries the dilation as supplied data (an isometry V with the pullback property), not constructed here — dilations are non-unique (honest-scope note in the plan). The canonical construction from √Eᵢ (which inhabits this structure for every POVM) is the separate existence half (P.5).

born_transfer mirrors Empirical/QM/Bell.lean's inner_alphaVec_betaVec: push V across the inner product via the matrix↔operator adjoint bridge (toEuclideanLin_conjTranspose_eq_adjoint), fold the three operator applications with toLpLin_mul_same, and collapse with the pullback identity.

noncomputable def CSD.LF4.blockProj {ι : Type u_1} [DecidableEq ι] (N : ℕ) (i : ι) : Matrix (Fin N × ι) (Fin N × ι) ℂ

The ancilla-i block projector Πᵢ = I_N ⊗ |i⟩⟨i| on the dilated index Fin N × ι. In the computational basis it is ∑ₙ |e_{(n,i)}⟩⟨e_{(n,i)}|, the rank-N projector onto the i-th ancilla level.

Equations

• CSD.LF4.blockProj N i = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Matrix.single i i 1)

theorem CSD.LF4.blockProj_mulVec {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (v : Fin N × ι → ℂ) (n : Fin N) (j : ι) : (blockProj N i).mulVec v (n, j) = if j = i then v (n, i) else 0

Action of the ancilla-i block projector on a coordinate. Πᵢ keeps the components whose ancilla index is i and zeroes the rest: (Πᵢ v)_{(n,j)} = if j = i then v_{(n,i)} else 0.

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

Naimark dilation of a POVM (supplied data). An isometry V : ℂ^N → ℂ^N ⊗ ℂ^ι (Vᴴ V = I) whose conjugation of the ancilla block projectors recovers the effects: Vᴴ Πᵢ V = Eᵢ. This is the defining Naimark property; the family {Πᵢ} is a genuine projective measurement on the dilated space (∑ᵢ Πᵢ = I_N ⊗ I_ι = I), and V compresses it to {Eᵢ}.

• V : Matrix (Fin N × ι) (Fin N) ℂ

  The dilation isometry, as a matrix ℂ^N → ℂ^{N×ι}.

• isom : self.V.conjTranspose * self.V = 1

  V is an isometry: Vᴴ V = I.

• pullback (i : ι) : self.V.conjTranspose * blockProj N i * self.V = (P.E i).M

  Naimark pullback: each effect is the compression of an ancilla projector.

theorem CSD.LF4.NaimarkDilation.born_transfer {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (i : ι) : P.weight ψ i = RCLike.re (inner ℂ ((Matrix.toEuclideanLin D.V) ψ) ((Matrix.toEuclideanLin (blockProj N i)) ((Matrix.toEuclideanLin D.V) ψ)))

Born transfer. The POVM Born weight ⟨ψ, Eᵢ ψ⟩ equals the projective Born weight ⟨Vψ, Πᵢ (Vψ)⟩ of the dilated state Vψ against the ancilla block projector Πᵢ on ℂ^N ⊗ ℂ^ι. This is the bridge onto the projective-Born surface that fs_born_volume_ratio_N reads as a Fubini–Study volume (P.3).

Proof: the matrix↔operator adjoint bridge moves V across the inner product, toLpLin_mul_same folds Vᴴ · Πᵢ · V, and pullback collapses it to Eᵢ.