Documentation

CsdLean4.Empirical.CSD.SIC3Volume

Empirical/CSD: the d=3 SIC-POVM (Hesse) and its Born weights as Kähler volumes #

Category: 3-Local (CSD-ontic layer; the first symmetric non-qubit (N = 3) entry in the volume-frequency series — the genuine dimension-3 SIC).

The d=3 SIC-POVM (symmetric informationally-complete POVM in dimension three) is the Hesse configuration: the 9 = d² Weyl–Heisenberg orbit states of the fiducial f = (0, 1, −1)/√2, ψ_{a,b} = Xᵃ Zᵇ f with X the cyclic shift |j⟩ ↦ |j+1⟩, Z the clock |j⟩ ↦ ωʲ|j⟩, ω = e^{2πi/3}. Concretely

ψ_{0,b} ∝ (0, ωᵇ, −ω²ᵇ),   ψ_{1,b} ∝ (−ω²ᵇ, 0, ωᵇ),   ψ_{2,b} ∝ (ωᵇ, −ω²ᵇ, 0)

(each × 1/√2). The effects are E_{a,b} = (1/3)|ψ_{a,b}⟩⟨ψ_{a,b}|; it is a genuine POVM because the orbit is a tight frame, ∑_{a,b}|ψ_{a,b}⟩⟨ψ_{a,b}| = 3 I₃, so ∑ E_{a,b} = I₃. It is symmetric in the strong (SIC) sense |⟨ψⱼ,ψₖ⟩|² = 1/4 for j ≠ k (sic3_inner_normSq), the dimension-3 analogue of the qubit tetrahedron.

This file:

builds sic3POVM : POVM 3 (Fin 3 × Fin 3) (a scaledRankOneEffect (1/3) helper + the Weyl–Heisenberg tight-frame completeness);
proves the equiangular SIC property |⟨ψⱼ,ψₖ⟩|² = 1/4;
gives the closed-form Born weights p_{a,b}(ψ) = (1/3)‖⟨ψ_{a,b}, ψ⟩‖²;
runs it through the POVM tranche: canonicalNaimark sic3POVM is the dilation, and sic3_born_frequency_volume lands the nine outcome frequencies as Fubini–Study volumes on the dilated ontic Σ' = ℂℙ²⁶ — carving-free, Gleason-free.

The first symmetric qutrit entry; the dilation lives on ℂℙ^{N·|ι|−1} = ℂℙ²⁶ (N = 3, |ι| = 9). 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).

Source #

Zauner 1999 (thesis); Renes, Blume-Kohout, Scott, Caves 2004, J. Math. Phys. 45, 2171 (the d=3 SIC / Hesse configuration).

Constants and square-root facts #

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.cc :

1/√2.

Equations

CSD.Empirical.CSDBridge.SIC3Volume.cc = ↑(√2 / 2)

Instances For

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.om :

ω = e^{2πi/3} = −1/2 + i√3/2.

Equations

CSD.Empirical.CSDBridge.SIC3Volume.om = ↑(-1 / 2) + ↑(√3 / 2) * Complex.I

Instances For

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.om2 :

ω² = e^{−2πi/3} = −1/2 − i√3/2.

Equations

CSD.Empirical.CSDBridge.SIC3Volume.om2 = ↑(-1 / 2) - ↑(√3 / 2) * Complex.I

Instances For

theorem CSD.Empirical.CSDBridge.SIC3Volume.r2 :

√2 ^ 2 = 2

theorem CSD.Empirical.CSDBridge.SIC3Volume.r3 :

√3 ^ 2 = 3

theorem CSD.Empirical.CSDBridge.SIC3Volume.r6 :

√6 ^ 2 = 6

theorem CSD.Empirical.CSDBridge.SIC3Volume.r2_4 :

√2 ^ 4 = 4

theorem CSD.Empirical.CSDBridge.SIC3Volume.r3_4 :

√3 ^ 4 = 9

theorem CSD.Empirical.CSDBridge.SIC3Volume.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.

The 9 SIC fiducial states (Weyl–Heisenberg orbit) #

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.sicAmp :

Fin 3 → Fin 3 → Fin 3 → ℂ

The amplitudes of the nine SIC states ψ_{a,b} (a, b ∈ Fin 3) on the computational basis. ψ_{a,b}[j] = ω^{(j−a)b}·f_{j−a} with f = (0, 1, −1)/√2.

Equations

Instances For

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.sicState (a b : Fin 3) :

EuclideanSpace ℂ (Fin 3)

The nine SIC states as unit vectors in ℂ³.

Equations

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

Instances For

theorem CSD.Empirical.CSDBridge.SIC3Volume.sicState_ofLp (a b j : Fin 3) :

(sicState a b).ofLp j = sicAmp a b j

theorem CSD.Empirical.CSDBridge.SIC3Volume.sicState_apply (a b j : Fin 3) :

(sicState a b).ofLp j = sicAmp a b j

theorem CSD.Empirical.CSDBridge.SIC3Volume.sicState_norm (a b : Fin 3) :

‖sicState a b‖ = 1

The Weyl–Heisenberg tight-frame relation and the POVM #

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_outer_sum :

∑ a : Fin 3, ∑ b : Fin 3, LF2.outerProduct (sicState a b) = 3 • 1

∑_{a,b} |ψ_{a,b}⟩⟨ψ_{a,b}| = 3 I₃ — the tight-frame relation making the SIC a POVM.

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.sicEffect (i : Fin 3 × Fin 3) :

The (a,b)-th SIC effect E_{a,b} = (1/3)|ψ_{a,b}⟩⟨ψ_{a,b}|.

Equations

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

Instances For

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_complete :

∑ i : Fin 3 × Fin 3, (sicEffect i).M = 1

Completeness: ∑_{a,b} E_{a,b} = (1/3)(3 I₃) = I₃. The d=3 SIC is a genuine POVM.

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.sic3POVM :

LF2.POVM 3 (Fin 3 × Fin 3)

The d=3 SIC-POVM {E_{a,b} = (1/3)|ψ_{a,b}⟩⟨ψ_{a,b}|} — the Hesse symmetric informationally-complete qutrit measurement.

Equations

CSD.Empirical.CSDBridge.SIC3Volume.sic3POVM = { E := CSD.Empirical.CSDBridge.SIC3Volume.sicEffect, complete := CSD.Empirical.CSDBridge.SIC3Volume.sic3_complete }

Instances For

The equiangular SIC property #

theorem CSD.Empirical.CSDBridge.SIC3Volume.inner_three (x y : EuclideanSpace ℂ (Fin 3)) :

inner ℂ x y = star (x.ofLp 0) * y.ofLp 0 + star (x.ofLp 1) * y.ofLp 1 + star (x.ofLp 2) * y.ofLp 2

⟨x, y⟩ = ∑ⱼ star(xⱼ)·yⱼ on ℂ³.

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_inner_normSq (a b c d : Fin 3) (h : (a, b) ≠ (c, d)) :

‖inner ℂ (sicState a b) (sicState c d)‖ ^ 2 = 1 / 4

The defining SIC symmetry: all pairwise overlaps are equal, |⟨ψⱼ, ψₖ⟩|² = 1/4 for j ≠ k. The nine states are equiangular — the dimension-3 analogue of the Bloch tetrahedron (1/(d+1) = 1/4).

The Born weights as Kähler volumes #

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_weight_eq (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) (i : Fin 3 × Fin 3) :

sic3POVM.weight ψ i = 1 / 3 * ‖inner ℂ ψ (sicState i.1 i.2)‖ ^ 2

Closed-form SIC Born weights: for a unit preparation ψ, p_{a,b}(ψ) = (1/3)‖⟨ψ_{a,b}, ψ⟩‖².

noncomputable def CSD.Empirical.CSDBridge.SIC3Volume.sic3Naimark :

LF4.NaimarkDilation sic3POVM

The canonical Naimark dilation of the d=3 SIC POVM.

Equations

CSD.Empirical.CSDBridge.SIC3Volume.sic3Naimark = CSD.LF4.canonicalNaimark CSD.Empirical.CSDBridge.SIC3Volume.sic3POVM

Instances For

theorem CSD.Empirical.CSDBridge.SIC3Volume.sic3_born_frequency_volume (ψ : EuclideanSpace ℂ (Fin 3)) (e : Fin 3 × Fin 3 × Fin 3 ≃ Fin 27) (ψ' : EuclideanSpace ℂ (Fin 27)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin sic3Naimark.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 27) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 27) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin 27), 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, ∀ (i : Fin 3 × Fin 3), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 3, (∑ l ∈ Finset.range m, (X l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (sic3POVM.weight ψ i))

The d=3 SIC-POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_volume_uncond at the Hesse SIC: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ²⁶ have each SIC outcome's empirical frequency converge, on a single almost-sure event, to the SIC Born weight p_{a,b}(ψ) = ⟨ψ, E_{a,b} ψ⟩ = (1/3)‖⟨ψ_{a,b},ψ⟩‖² — realised as a sum of Fubini–Study volumes of the dilated barycentric cells. The first symmetric non-qubit entry in the volume-frequency series; carving-free, Gleason-free, and (since the 2026-06-11 hpos migration) with no genericity hypothesis on the dilated state — notably, ψ ⊥ ψ_{a,b} (a SIC outcome weight exactly zero) is covered.