Empirical/CSD: the USD (unambiguous-discrimination) POVM and its Born weights as Kähler volumes

Category: 3-Local (CSD-ontic layer; the second non-projective (POVM) entry in the volume-frequency series, after the trine).

The unambiguous state discrimination POVM (Ivanovic–Dieks–Peres) is the canonical "why POVMs are needed" measurement: it distinguishes two non-orthogonal pure states ψ₁, ψ₂ (overlap s = ⟨ψ₁,ψ₂⟩ ∈ [0,1)) with zero error at the cost of an inconclusive outcome. The three effects are E₁ = a|ψ₂^⊥⟩⟨ψ₂^⊥|, E₂ = a|ψ₁^⊥⟩⟨ψ₁^⊥|, E? = |χ?⟩⟨χ?| with a = 1/(1+s); the full usdPOVM : POVM 2 (Fin 3) (states + unambiguity + success + completeness) is built in Empirical/QM/USD.lean.

This file:

• gives the closed-form conclusive Born weights p₁(ψ) = a‖⟨ψ, ψ₂^⊥⟩‖², p₂(ψ) = a‖⟨ψ, ψ₁^⊥⟩‖²;
• runs the POVM through the tranche: canonicalNaimark (usdPOVM …) is the dilation, and usd_born_frequency_volume lands the three USD outcome frequencies as Fubini–Study volumes on the dilated ontic Σ' = ℂℙ⁵ — carving-free, Gleason-free.

Like the trine, the volume reading is the general POVM capstone instantiated at a concrete non-projective measurement; it routes through the hpos-free engine (povm_born_frequency_volume_uncond, LF4/BornRegionUncond.lean), so no genericity hypothesis on the dilated state is carried (2026-06-11 migration).

The conclusive Born weights

theorem CSD.Empirical.CSDBridge.USDVolume.usd_weight_e1 (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : (QM.USD.usdPOVM s hs0 hs1).weight ψ 0 = QM.USD.usdA s * ‖inner ℂ ψ (QM.USD.psi2perp s)‖ ^ 2

Closed-form conclusive weight (outcome 1): p₁(ψ) = a‖⟨ψ, ψ₂^⊥⟩‖².

theorem CSD.Empirical.CSDBridge.USDVolume.usd_weight_e2 (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : (QM.USD.usdPOVM s hs0 hs1).weight ψ 1 = QM.USD.usdA s * ‖inner ℂ ψ QM.USD.psi1perp‖ ^ 2

Closed-form conclusive weight (outcome 2): p₂(ψ) = a‖⟨ψ, ψ₁^⊥⟩‖².

The USD POVM Born weights as Kähler volumes

noncomputable def CSD.Empirical.CSDBridge.USDVolume.usdNaimark (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : LF4.NaimarkDilation (QM.USD.usdPOVM s hs0 hs1)

The canonical Naimark dilation of the USD POVM (it exists, like every POVM's).

Equations

• CSD.Empirical.CSDBridge.USDVolume.usdNaimark s hs0 hs1 = CSD.LF4.canonicalNaimark (CSD.Empirical.QM.USD.usdPOVM s hs0 hs1)

theorem CSD.Empirical.CSDBridge.USDVolume.usd_born_frequency_volume (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 3 ≃ Fin 6) (ψ' : EuclideanSpace ℂ (Fin 6)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (usdNaimark s hs0 hs1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 6) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 6) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin 6), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (k : Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (X l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, k))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds ((QM.USD.usdPOVM s hs0 hs1).weight ψ k))

The USD POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_volume_uncond at the unambiguous-discrimination POVM: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ⁵ have the k-th USD outcome's empirical frequency converge, on a single almost-sure event, to the USD Born weight pₖ(ψ) = ⟨ψ, Eₖ ψ⟩ (the two conclusive weights a‖⟨ψₖ^⊥, ψ⟩‖² and the inconclusive weight) — realised as a sum of Fubini–Study volumes of the dilated barycentric cells. The second non-projective (POVM) entry in the volume-frequency series, after the trine; carving-free, Gleason-free, and (since the 2026-06-11 hpos migration) with no genericity hypothesis on the dilated state — notably, ψ = ψ₁ or ψ₂ (a conclusive weight exactly zero, the unambiguity case itself) is covered.