Empirical/CSD: the d=2 SIC-POVM and its Born weights as Kähler volumes

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

The SIC-POVM (symmetric informationally-complete POVM) in dimension 2 is the tetrahedral qubit measurement: four fiducial states |ψₖ⟩ whose Bloch vectors form a regular tetrahedron, with effects Eₖ = (1/2)|ψₖ⟩⟨ψₖ|. It is symmetric in the strong sense that the pairwise overlaps are all equal, |⟨ψⱼ,ψₖ⟩|² = 1/3 for j ≠ k (sic_inner_normSq below) — the defining SIC property — and informationally complete (four outcomes span the operator space of a qubit). It is a genuine POVM: ∑ₖ Eₖ = I holds because ∑ₖ |ψₖ⟩⟨ψₖ| = 2 I (the tetrahedral tight-frame relation).

The explicit fiducial set used here: ψ₀ = |0⟩, ψₖ = (1/√3)|0⟩ + √(2/3)·ω^{k-1}|1⟩ (k = 1,2,3), ω = e^{2πi/3}, i.e. the second components are √6/3, −√6/6 ± i√2/2.

This file:

• builds sicPOVM : POVM 2 (Fin 4) (a scaledRankOneEffect (1/2) helper + completeness);
• proves the equiangular SIC property |⟨ψⱼ,ψₖ⟩|² = 1/3;
• gives the closed-form Born weights pₖ(ψ) = (1/2)‖⟨ψ, ψₖ⟩‖²;
• runs the POVM through the tranche: canonicalNaimark sicPOVM is the dilation, and sic_born_frequency_volume lands the four SIC outcome frequencies as Fubini–Study volumes on the dilated Σ' = ℂℙ⁷ — carving-free, Gleason-free.

The capstone 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).

Square-root facts

theorem CSD.Empirical.CSDBridge.SICVolume.r2 : √2 ^ 2 = 2

theorem CSD.Empirical.CSDBridge.SICVolume.r3 : √3 ^ 2 = 3

theorem CSD.Empirical.CSDBridge.SICVolume.r6 : √6 ^ 2 = 6

The SIC fiducial states

noncomputable def CSD.Empirical.CSDBridge.SICVolume.sicAmp : Fin 4 → Fin 2 → ℂ

The complex amplitudes of the four tetrahedral SIC states on the computational basis. ω = e^{2πi/3} enters as ω = −1/2 + i√3/2, so √(2/3)·ω = −√6/6 + i√2/2 and √(2/3)·ω² = −√6/6 − i√2/2.

Equations

• CSD.Empirical.CSDBridge.SICVolume.sicAmp 0 0 = 1
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 0 1 = 0
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 1 0 = ↑(√3 / 3)
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 1 1 = ↑(√6 / 3)
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 2 0 = ↑(√3 / 3)
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 2 1 = ↑(-√6 / 6) + ↑(√2 / 2) * Complex.I
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 3 0 = ↑(√3 / 3)
• CSD.Empirical.CSDBridge.SICVolume.sicAmp 3 1 = ↑(-√6 / 6) - ↑(√2 / 2) * Complex.I

noncomputable def CSD.Empirical.CSDBridge.SICVolume.sicState (k : Fin 4) : EuclideanSpace ℂ (Fin 2)

The four SIC states as unit vectors in ℂ².

Equations

• CSD.Empirical.CSDBridge.SICVolume.sicState k = EuclideanSpace.single 0 (CSD.Empirical.CSDBridge.SICVolume.sicAmp k 0) + EuclideanSpace.single 1 (CSD.Empirical.CSDBridge.SICVolume.sicAmp k 1)

theorem CSD.Empirical.CSDBridge.SICVolume.sicState_ofLp (k : Fin 4) (i : Fin 2) : (sicState k).ofLp i = sicAmp k i

theorem CSD.Empirical.CSDBridge.SICVolume.sicState_apply (k : Fin 4) (i : Fin 2) : (sicState k).ofLp i = sicAmp k i

theorem CSD.Empirical.CSDBridge.SICVolume.normSq_coord (z : ℂ) : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im

‖z‖² = z.re·z.re + z.im·z.im, the bridge to real coordinates.

theorem CSD.Empirical.CSDBridge.SICVolume.sicState_norm (k : Fin 4) : ‖sicState k‖ = 1

The tetrahedral tight-frame relation and the POVM

theorem CSD.Empirical.CSDBridge.SICVolume.sic_outer_sum : ∑ k : Fin 4, LF2.outerProduct (sicState k) = 2 • 1

∑ₖ |ψₖ⟩⟨ψₖ| = 2 I — the tetrahedral tight-frame relation that makes the SIC a valid POVM.

noncomputable def CSD.Empirical.CSDBridge.SICVolume.sicEffect (k : Fin 4) : LF2.Effect 2

The k-th SIC effect Eₖ = (1/2)|ψₖ⟩⟨ψₖ|.

Equations

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

theorem CSD.Empirical.CSDBridge.SICVolume.sic_complete : ∑ k : Fin 4, (sicEffect k).M = 1

Completeness: ∑ₖ Eₖ = (1/2)·(2 I) = I. The SIC is a genuine POVM.

noncomputable def CSD.Empirical.CSDBridge.SICVolume.sicPOVM : LF2.POVM 2 (Fin 4)

The d=2 SIC-POVM {Eₖ = (1/2)|ψₖ⟩⟨ψₖ|}ₖ — the tetrahedral symmetric informationally-complete (non-projective) qubit measurement.

Equations

• CSD.Empirical.CSDBridge.SICVolume.sicPOVM = { E := CSD.Empirical.CSDBridge.SICVolume.sicEffect, complete := CSD.Empirical.CSDBridge.SICVolume.sic_complete }

The equiangular SIC property

theorem CSD.Empirical.CSDBridge.SICVolume.inner_two (x y : EuclideanSpace ℂ (Fin 2)) : inner ℂ x y = star (x.ofLp 0) * y.ofLp 0 + star (x.ofLp 1) * y.ofLp 1

⟨x, y⟩ = star(x₀)·y₀ + star(x₁)·y₁ on ℂ².

theorem CSD.Empirical.CSDBridge.SICVolume.sic_inner_normSq (j k : Fin 4) (hjk : j ≠ k) : ‖inner ℂ (sicState j) (sicState k)‖ ^ 2 = 1 / 3

The defining SIC symmetry: all pairwise overlaps are equal, |⟨ψⱼ, ψₖ⟩|² = 1/3 for j ≠ k. The four states are equiangular — a regular tetrahedron in the Bloch ball.

The SIC Born weights as Kähler volumes

theorem CSD.Empirical.CSDBridge.SICVolume.sic_weight_eq (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) (k : Fin 4) : sicPOVM.weight ψ k = 1 / 2 * ‖inner ℂ ψ (sicState k)‖ ^ 2

Closed-form SIC Born weights: for a unit preparation ψ, pₖ(ψ) = (1/2)‖⟨ψ, ψₖ⟩‖².

noncomputable def CSD.Empirical.CSDBridge.SICVolume.sicNaimark : LF4.NaimarkDilation sicPOVM

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

Equations

• CSD.Empirical.CSDBridge.SICVolume.sicNaimark = CSD.LF4.canonicalNaimark CSD.Empirical.CSDBridge.SICVolume.sicPOVM

theorem CSD.Empirical.CSDBridge.SICVolume.sic_born_frequency_volume (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 4 ≃ Fin 8) (ψ' : EuclideanSpace ℂ (Fin 8)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin sicNaimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 8) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 8) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin 8), 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 4), 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 (sicPOVM.weight ψ k))

The SIC POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_volume_uncond at the tetrahedral SIC POVM: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ⁷ have the k-th SIC outcome's empirical frequency converge, on a single almost-sure event, to the SIC Born weight pₖ(ψ) = ⟨ψ, Eₖ ψ⟩ = (1/2)‖⟨ψₖ,ψ⟩‖² — realised as a sum of Fubini–Study volumes of the dilated barycentric cells. The third non-projective (POVM) entry in the volume-frequency series, after the trine and USD; carving-free, Gleason-free, and (since the 2026-06-11 hpos migration) with no genericity hypothesis on the dilated state.