Empirical/CSD: the qubit trine POVM and its Born weights as Kähler volumes

Category: 3-Local (CSD-ontic layer; the first non-projective (POVM) entry in the volume-frequency series — SG, Malus, Bell, GHZ, Hardy were all projective).

The trine is the canonical minimal symmetric qubit POVM: three states |ψₖ⟩ whose Bloch vectors sit at 120° in a great circle, with effects Eₖ = (2/3)|ψₖ⟩⟨ψₖ|. It is a genuine POVM — ∑ₖ Eₖ = I holds only because the three projectors sum to (3/2)I — and cannot be realised projectively (three outcomes on a 2-dimensional space).

This file:

• builds trinePOVM : POVM 2 (Fin 3) (a scaledRankOneEffect helper + completeness);
• gives the closed-form Born weights pₖ(ψ) = (2/3)‖⟨ψₖ, ψ⟩‖²;
• runs it through the POVM tranche: canonicalNaimark trinePOVM is the dilation, and trine_born_frequency_volume lands the trine outcome frequencies as Fubini–Study volumes on the dilated Σ' = ℂℙ⁵ — carving-free, Gleason-free.

The trine has no structural zeros (for generic ψ all three weights are nonzero). The capstone is unconditional: 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); vanishing dilated amplitudes give FS-null cells.

The trine states and POVM

noncomputable def CSD.Empirical.CSDBridge.TrineVolume.trineAmp : Fin 3 → Fin 2 → ℝ

The (real) amplitudes of the three trine states on the computational basis: Bloch vectors at 120° in the x–z great circle. ψ₀ = |0⟩, ψ₁ = (1/2)|0⟩ + (√3/2)|1⟩, ψ₂ = (1/2)|0⟩ − (√3/2)|1⟩.

Equations

• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 0 0 = 1
• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 0 1 = 0
• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 1 0 = 1 / 2
• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 1 1 = √3 / 2
• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 2 0 = 1 / 2
• CSD.Empirical.CSDBridge.TrineVolume.trineAmp 2 1 = -(√3 / 2)

noncomputable def CSD.Empirical.CSDBridge.TrineVolume.trineState (k : Fin 3) : EuclideanSpace ℂ (Fin 2)

The three trine states as unit vectors in ℂ².

Equations

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

theorem CSD.Empirical.CSDBridge.TrineVolume.trineState_ofLp (k : Fin 3) (i : Fin 2) : (trineState k).ofLp i = ↑(trineAmp k i)

theorem CSD.Empirical.CSDBridge.TrineVolume.trineAmp_sq_sum (k : Fin 3) : trineAmp k 0 ^ 2 + trineAmp k 1 ^ 2 = 1

theorem CSD.Empirical.CSDBridge.TrineVolume.trineState_norm (k : Fin 3) : ‖trineState k‖ = 1

theorem CSD.Empirical.CSDBridge.TrineVolume.trineState_apply (k : Fin 3) (i : Fin 2) : (trineState k).ofLp i = ↑(trineAmp k i)

theorem CSD.Empirical.CSDBridge.TrineVolume.trine_outer_sum : ∑ k : Fin 3, LF2.outerProduct (trineState k) = ↑(3 / 2) • 1

∑ₖ |ψₖ⟩⟨ψₖ| = (3/2) I — the Gram relation that makes the trine a valid POVM.

The trine POVM

noncomputable def CSD.Empirical.CSDBridge.TrineVolume.trineEffect (k : Fin 3) : LF2.Effect 2

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

Equations

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

theorem CSD.Empirical.CSDBridge.TrineVolume.trine_complete : ∑ k : Fin 3, (trineEffect k).M = 1

Completeness: ∑ₖ Eₖ = (2/3)(3/2) I = I. The trine is a genuine POVM.

noncomputable def CSD.Empirical.CSDBridge.TrineVolume.trinePOVM : LF2.POVM 2 (Fin 3)

The qubit trine POVM {Eₖ = (2/3)|ψₖ⟩⟨ψₖ|}ₖ — the canonical minimal symmetric (non-projective) qubit measurement.

Equations

• CSD.Empirical.CSDBridge.TrineVolume.trinePOVM = { E := CSD.Empirical.CSDBridge.TrineVolume.trineEffect, complete := CSD.Empirical.CSDBridge.TrineVolume.trine_complete }

The trine Born weights as Kähler volumes

theorem CSD.Empirical.CSDBridge.TrineVolume.trine_weight_eq (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) (k : Fin 3) : trinePOVM.weight ψ k = 2 / 3 * ‖inner ℂ ψ (trineState k)‖ ^ 2

Closed-form trine Born weights: for a unit preparation ψ, pₖ(ψ) = (2/3)‖⟨ψ, ψₖ⟩‖² — the symmetric 120°-measurement outcome probabilities.

noncomputable def CSD.Empirical.CSDBridge.TrineVolume.trineNaimark : LF4.NaimarkDilation trinePOVM

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

Equations

• CSD.Empirical.CSDBridge.TrineVolume.trineNaimark = CSD.LF4.canonicalNaimark CSD.Empirical.CSDBridge.TrineVolume.trinePOVM

theorem CSD.Empirical.CSDBridge.TrineVolume.trine_born_frequency_volume (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 3 ≃ Fin 6) (ψ' : EuclideanSpace ℂ (Fin 6)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin trineNaimark.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 (trinePOVM.weight ψ k))

The trine POVM Born weights as Kähler volumes (the capstone). Instantiating povm_born_frequency_volume_uncond at the trine: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ⁵ have the k-th trine outcome's empirical frequency converge, on a single almost-sure event, to the trine Born weight pₖ(ψ) = ⟨ψ, Eₖ ψ⟩ (the symmetric 120°-measurement outcome probability (2/3)‖⟨ψₖ,ψ⟩‖²) — realised as a sum of Fubini–Study volumes of the dilated barycentric cells. The first non-projective (POVM) 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.