Documentation

CsdLean4.Empirical.CSD.MUB3Volume

Empirical/CSD: the d=3 mutually-unbiased-bases POVM and its Born weights as Kähler volumes #

Category: 3-Local (CSD-ontic layer; a second non-qubit (N = 3) symmetric entry in the volume-frequency series — the complete set of mutually unbiased bases in dimension 3).

In dimension d = 3 there are d + 1 = 4 mutually unbiased bases (MUBs): the computational basis together with three Fourier-type bases from the Heisenberg–Weyl / Alltop construction, v_{a,j}[l] = ω^{a l² + j l}/√3 (a, j ∈ Fin 3, ω = e^{2πi/3}). Any two vectors from different bases satisfy |⟨v, w⟩|² = 1/d = 1/3 — they are unbiased (mub3_unbiased). The 4 · 3 = 12 vectors form a tight frame, so the effects Eₖ = (1/4)|ψₖ⟩⟨ψₖ| give a genuine (non-projective) POVM with ∑ Eₖ = I₃: pooling a measurement in each of the 4 bases with prior 1/4.

This file:

builds mub3POVM : POVM 3 (Fin 4 × Fin 3) (a scaledRankOneEffect (1/4) helper + the tight-frame completeness ∑|ψₖ⟩⟨ψₖ| = 4 I₃);
proves the defining unbiasedness |⟨v, w⟩|² = 1/3 across distinct bases;
gives the closed-form Born weights p_{b,j}(ψ) = (1/4)‖⟨v_{b,j}, ψ⟩‖²;
runs it through the POVM tranche: canonicalNaimark mub3POVM is the dilation, and mub3_born_frequency_volume lands the twelve outcome frequencies as Fubini–Study volumes on the dilated ontic Σ' = ℂℙ³⁵ — carving-free, Gleason-free.

The dilation lives on ℂℙ^{N·|ι|−1} = ℂℙ³⁵ (N = 3, |ι| = 12). 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) — notably, MUB vectors themselves (which zero the other two outcomes of their own basis) are covered.

Source #

Wootters, Fields 1989, Ann. Phys. 191, 363 (MUBs from finite fields); Ivonovic 1981. The d=3 MUB POVM is the canonical complete-MUB measurement.

Constants and square-root facts #

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

1/√3.

Equations

CSD.Empirical.CSDBridge.MUB3Volume.cc = ↑(√3 / 3)

Instances For

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

theorem CSD.Empirical.CSDBridge.MUB3Volume.om2_def :

om2 = ↑(-1 / 2) - ↑(√3 / 2) * Complex.I

The conjugate cube root of unity, as its defining formula (interface lemma, §9.1).

theorem CSD.Empirical.CSDBridge.MUB3Volume.r3 :

√3 ^ 2 = 3

theorem CSD.Empirical.CSDBridge.MUB3Volume.r3_4 :

√3 ^ 4 = 9

theorem CSD.Empirical.CSDBridge.MUB3Volume.normSq_coord (z : ℂ) :

‖z‖ ^ 2 = z.re * z.re + z.im * z.im

The 12 MUB vectors #

noncomputable def CSD.Empirical.CSDBridge.MUB3Volume.mubAmp :

Fin 4 → Fin 3 → Fin 3 → ℂ

The amplitudes of the twelve MUB vectors v_{b,j} (basis b ∈ Fin 4, vector j ∈ Fin 3) on the computational basis. Basis 0 is computational; bases 1,2,3 are the Fourier-type bases a = b−1, v_{a,j}[l] = ω^{a l² + j l}/√3.

Equations

Instances For

noncomputable def CSD.Empirical.CSDBridge.MUB3Volume.mubVec (b : Fin 4) (j : Fin 3) :

EuclideanSpace ℂ (Fin 3)

The twelve MUB vectors as unit vectors in ℂ³.

Equations

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

Instances For

theorem CSD.Empirical.CSDBridge.MUB3Volume.mubVec_ofLp (b : Fin 4) (j l : Fin 3) :

(mubVec b j).ofLp l = mubAmp b j l

theorem CSD.Empirical.CSDBridge.MUB3Volume.mubVec_apply (b : Fin 4) (j l : Fin 3) :

(mubVec b j).ofLp l = mubAmp b j l

theorem CSD.Empirical.CSDBridge.MUB3Volume.mubVec_norm (b : Fin 4) (j : Fin 3) :

‖mubVec b j‖ = 1

The tight-frame relation and the POVM #

theorem CSD.Empirical.CSDBridge.MUB3Volume.mub3_outer_sum :

∑ b : Fin 4, ∑ j : Fin 3, LF2.outerProduct (mubVec b j) = 4 • 1

∑_{b,j} |v_{b,j}⟩⟨v_{b,j}| = 4 I₃ — the MUB tight-frame relation (4 bases, each a resolution of the identity).

noncomputable def CSD.Empirical.CSDBridge.MUB3Volume.mubEffect (i : Fin 4 × Fin 3) :

The (b,j)-th MUB effect E_{b,j} = (1/4)|v_{b,j}⟩⟨v_{b,j}|.

Equations

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

Instances For

theorem CSD.Empirical.CSDBridge.MUB3Volume.mub3_complete :

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

Completeness: ∑_{b,j} E_{b,j} = (1/4)(4 I₃) = I₃. The MUB pooling is a POVM.

noncomputable def CSD.Empirical.CSDBridge.MUB3Volume.mub3POVM :

LF2.POVM 3 (Fin 4 × Fin 3)

The d=3 complete-MUB POVM {E_{b,j} = (1/4)|v_{b,j}⟩⟨v_{b,j}|} — pooling a measurement in each of the four mutually unbiased bases with prior 1/4.

Equations

CSD.Empirical.CSDBridge.MUB3Volume.mub3POVM = { E := CSD.Empirical.CSDBridge.MUB3Volume.mubEffect, complete := CSD.Empirical.CSDBridge.MUB3Volume.mub3_complete }

Instances For

The unbiasedness property #

theorem CSD.Empirical.CSDBridge.MUB3Volume.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.MUB3Volume.mub3_unbiased (b b' : Fin 4) (j j' : Fin 3) (h : b ≠ b') :

‖inner ℂ (mubVec b j) (mubVec b' j')‖ ^ 2 = 1 / 3

Mutual unbiasedness: any two vectors from different bases overlap with |⟨v_{b,j}, v_{b',j'}⟩|² = 1/d = 1/3. The defining MUB property.

The Born weights as Kähler volumes #

theorem CSD.Empirical.CSDBridge.MUB3Volume.mub3_weight_eq (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) (i : Fin 4 × Fin 3) :

mub3POVM.weight ψ i = 1 / 4 * ‖inner ℂ ψ (mubVec i.1 i.2)‖ ^ 2

Closed-form MUB Born weights: for a unit preparation ψ, p_{b,j}(ψ) = (1/4)‖⟨v_{b,j}, ψ⟩‖².

noncomputable def CSD.Empirical.CSDBridge.MUB3Volume.mub3Naimark :

LF4.NaimarkDilation mub3POVM

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

Equations

CSD.Empirical.CSDBridge.MUB3Volume.mub3Naimark = CSD.LF4.canonicalNaimark CSD.Empirical.CSDBridge.MUB3Volume.mub3POVM

Instances For

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

The d=3 MUB POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_volume_uncond at the complete-MUB measurement: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ³⁵ have each of the twelve outcome frequencies converge, on a single almost-sure event, to the Born weight p_{b,j}(ψ) = (1/4)‖⟨v_{b,j},ψ⟩‖² — realised as a sum of Fubini–Study volumes of the dilated barycentric cells. A second non-qubit symmetric entry; carving-free, Gleason-free, and (since the 2026-06-11 hpos migration) with no genericity hypothesis on the dilated state.