Empirical/CSD: the unsharp qutrit POVM and its Born weights as Kähler volumes

Category: 3-Local (CSD-ontic layer; the first non-qubit (N = 3) entry in the volume-frequency series, and the first genuinely non-projective qutrit POVM).

The unsharp (white-noise) measurement is the textbook model of a noisy detector and the canonical reason POVMs are needed beyond the projective formalism: a sharp basis measurement {|k⟩⟨k|} degraded by depolarising noise of strength ε,

Eₖ = (1 − ε)|k⟩⟨k| + (ε/3) I₃        (k ∈ Fin 3,  0 ≤ ε ≤ 1).

For ε ∈ (0, 1) each Eₖ is a genuine (rank-3, non-projector) effect, so this is a real POVM requiring a Naimark dilation rather than a projective measurement. Completeness is immediate: ∑ₖ Eₖ = (1 − ε) ∑ₖ|k⟩⟨k| + ε I₃ = (1 − ε) I₃ + ε I₃ = I₃.

This file:

• builds noisyPOVM ε : POVM 3 (Fin 3) (a direct Effect construction + completeness);
• gives the closed-form Born weights pₖ(ψ) = (1 − ε)‖⟨k, ψ⟩‖² + ε/3;
• runs it through the POVM tranche: canonicalNaimark (noisyPOVM ε) is the dilation, and noisy_born_frequency_volume lands the three outcome frequencies as Fubini–Study volumes on the dilated ontic Σ' = ℂℙ⁸ — carving-free, Gleason-free.

This is the first entry exercising the general-N Naimark→volume machinery past the qubit: the dilation lives on ℂℙ^{N·|ι|−1} = ℂℙ⁸ for N = 3, |ι| = 3. The capstone routes through the hpos-free engine (povm_born_frequency_basin, LF4/BornRegionUncond.lean), so no genericity hypothesis on the dilated state is carried (2026-06-11 migration).

Source

Unsharp / POVM measurements: Busch, Lahti, Mittelstaedt, The Quantum Theory of Measurement (1996); depolarising noise is the standard detector-noise model.

The computational basis of ℂ³

noncomputable def CSD.Empirical.CSDBridge.QutritPOVMVolume.basisVec (k : Fin 3) : EuclideanSpace ℂ (Fin 3)

The k-th computational basis vector |k⟩ of ℂ³.

Equations

• CSD.Empirical.CSDBridge.QutritPOVMVolume.basisVec k = EuclideanSpace.single k 1

@[simp]

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.basisVec_norm (k : Fin 3) : ‖basisVec k‖ = 1

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.basis_outer_sum : ∑ k : Fin 3, LF2.outerProduct (basisVec k) = 1

∑ₖ |k⟩⟨k| = I₃ — completeness of the computational basis.

The unsharp effects and POVM

noncomputable def CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyEffect (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (k : Fin 3) : LF2.Effect 3

The unsharp effect Eₖ = (1 − ε)|k⟩⟨k| + (ε/3) I₃. A genuine (rank-3) effect for ε ∈ (0, 1); ε = 0 is the sharp projector, ε = 1 the trivial I₃/3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyEffect_M (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (k : Fin 3) : (noisyEffect ε hε0 hε1 k).M = ↑(1 - ε) • LF2.outerProduct (basisVec k) + ↑(ε / 3) • 1

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.noisy_complete (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : ∑ k : Fin 3, (noisyEffect ε hε0 hε1 k).M = 1

Completeness: ∑ₖ Eₖ = (1 − ε) I₃ + ε I₃ = I₃.

noncomputable def CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyPOVM (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : LF2.POVM 3 (Fin 3)

The unsharp qutrit POVM {Eₖ = (1−ε)|k⟩⟨k| + (ε/3)I₃}ₖ — a genuine non-projective qutrit measurement.

Equations

• CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyPOVM ε hε0 hε1 = { E := CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyEffect ε hε0 hε1, complete := ⋯ }

The Born weights as Kähler volumes

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.noisy_weight_eq (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) (k : Fin 3) : (noisyPOVM ε hε0 hε1).weight ψ k = (1 - ε) * ‖inner ℂ ψ (basisVec k)‖ ^ 2 + ε / 3

Closed-form unsharp Born weights: for a unit preparation ψ, pₖ(ψ) = (1 − ε)‖⟨k, ψ⟩‖² + ε/3. The signal term (1−ε)‖⟨k,ψ⟩‖² plus the uniform noise floor ε/3.

noncomputable def CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyNaimark (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : LF4.NaimarkDilation (noisyPOVM ε hε0 hε1)

The canonical Naimark dilation of the unsharp qutrit POVM.

Equations

• CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyNaimark ε hε0 hε1 = CSD.LF4.canonicalNaimark (CSD.Empirical.CSDBridge.QutritPOVMVolume.noisyPOVM ε hε0 hε1)

theorem CSD.Empirical.CSDBridge.QutritPOVMVolume.noisy_born_frequency_volume (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (ψ : EuclideanSpace ℂ (Fin 3)) (e : Fin 3 × Fin 3 ≃ Fin 9) (ψ' : EuclideanSpace ℂ (Fin 9)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (noisyNaimark ε hε0 hε1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.KSigma 9) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)) (hindep : ∀ (j : Fin 9), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 9) j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (X l ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 9) (e (n, k))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds ((noisyPOVM ε hε0 hε1).weight ψ k))

The unsharp qutrit POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_basin at the unsharp qutrit measurement: i.i.d. trials over the fibred epistemic law on the dilated ontic Σ' = ℂℙ⁸ have the k-th outcome's empirical frequency converge, on a single almost-sure event, to the Born weight pₖ(ψ) = ⟨ψ, Eₖ ψ⟩ = (1 − ε)‖⟨k,ψ⟩‖² + ε/3 — realised as a sum of the epistemic typicality measures of the dilated global basins. The first non-qubit (N = 3) entry in the volume-frequency series, and the first non-projective qutrit POVM; carving-free, Gleason-free, and (since the 2026-06-11 hpos migration) with no genericity hypothesis on the dilated state — the sharp limit ε = 0 at a basis state is covered.