LF6-D (QM side): the maximally-entangled qutrit violates the CGLMP inequality

Category: 6-Local (the d = 3-intrinsic Bell violation for Ψ_3, the QM-side payoff of the CGLMP infrastructure Mathlib/Probability/CGLMP.lean).

The LF6-D non-factorisation of the general d × d maximally-entangled state Ψ_d (no_product_partition_realises_maxEntangled) was, up to this file, forced through the CHSH-violating 2 × 2 Schmidt (Φ⁺) sector: a genuinely derived violation, but a two-outcome (CHSH) one, so not d-intrinsic. This module discharges the genuinely d = 3 CGLMP violation for the maximally-entangled qutrit, closing that gap for d = 3.

What is proved

Under the standard CGLMP phase-basis measurements on Ψ_3 (Alice offsets α₁ = 0, α₂ = 1/2; Bob offsets β₁ = -1/4, β₂ = 1/4), the joint outcome-difference Born probabilities pQM x y c = P(A_x − B_y = c) are computed from the Hilbert space (pQM is the marginal sum of the genuine squared overlaps bornPair x y k l = ‖⟨outcome_{k,l}, Ψ_3⟩‖², bornPair_value its closed form via the roots-of-unity geometric sum). The four CGLMP-positive entries are (4 + 2√3)/9, the four negative entries 1/9, giving the exact CGLMP value

I_3 = cglmp 3 pQM = (12 + 8√3)/9 ≈ 2.8729                    (cglmp_maxEntangled_qutrit_eq)

which exceeds the local-hidden-variable bound 2 (cglmp_maxEntangled_qutrit_gt_two), contradicting ProbabilityTheory.CGLMP.cglmp_lhv_bound_three (I_3 ≤ 2 for every deterministic LHV model). Hence no local-hidden-variable model reproduces Ψ_3's actual CGLMP outcome-difference statistics (no_lhv_realises_maxEntangled_cglmp): a genuinely d = 3-intrinsic Bell force, not the 2 × 2 Φ⁺ CHSH sector.

Honest scope

• The violation is a genuine computation from Ψ_3's actual Born probabilities under real qutrit measurements: bornPair is a squared inner product with maxEntangled 3, the outcome vectors are the CGLMP phase-basis measurement vectors (aVec_unit, bVec_unit: unit vectors), and pQM x y c is the genuine outcome-difference marginal (pQM, pQM_eq_pair: Born depends only on k − l by bornPair_periodic). The value (12 + 8√3)/9 is not asserted; every step is derived, the √3 irrational (no rational analogue violates — half-integer offsets give exactly 2).
• The LHV bound I_3 ≤ 2 is imported from cglmp_lhv_bound_three (the d = 3 finite optimisation, decide over the 81 strategies). This file supplies the QM side.
• d = 3 only. The general-d (d ≥ 4) CGLMP violation for Ψ_d remains the residual.
• Foundational-triple-only (no busch_effect_gleason; the geometric sums and the finite LHV optimisation are both Gleason-free).

Reference: Collins, Gisin, Linden, Massar, Popescu, Phys. Rev. Lett. 88, 040404 (2002). specs/lf6-plan.md (LF6-D).

The CGLMP qutrit measurement settings

noncomputable def CSD.LF6.CGLMPQutrit.alphaOff (x : Bool) : ℝ

Alice's phase offset α_x: setting false (A₁) → 0, true (A₂) → 1/2.

Equations

• CSD.LF6.CGLMPQutrit.alphaOff x = if x = true then 1 / 2 else 0

noncomputable def CSD.LF6.CGLMPQutrit.betaOff (y : Bool) : ℝ

Bob's phase offset β_y: setting false (B₁) → -1/4, true (B₂) → 1/4.

Equations

• CSD.LF6.CGLMPQutrit.betaOff y = if y = true then 1 / 4 else -1 / 4

noncomputable def CSD.LF6.CGLMPQutrit.deltaOff (x y : Bool) : ℝ

The combined offset δ = α_x − β_y.

Equations

• CSD.LF6.CGLMPQutrit.deltaOff x y = CSD.LF6.CGLMPQutrit.alphaOff x - CSD.LF6.CGLMPQutrit.betaOff y

noncomputable def CSD.LF6.CGLMPQutrit.aAngle (x : Bool) (k : ZMod 3) (j : Fin 3) : ℝ

Alice's phase-basis angle 2π·j·(k + α_x)/3 for outcome k, component j.

Equations

• CSD.LF6.CGLMPQutrit.aAngle x k j = 2 * Real.pi * ↑↑j * (↑k.val + CSD.LF6.CGLMPQutrit.alphaOff x) / 3

noncomputable def CSD.LF6.CGLMPQutrit.bAngle (y : Bool) (l : ZMod 3) (j : Fin 3) : ℝ

Bob's phase-basis angle −2π·j·(l + β_y)/3 for outcome l, component j.

Equations

• CSD.LF6.CGLMPQutrit.bAngle y l j = -(2 * Real.pi * ↑↑j * (↑l.val + CSD.LF6.CGLMPQutrit.betaOff y) / 3)

noncomputable def CSD.LF6.CGLMPQutrit.aVec (x : Bool) (k : ZMod 3) : EuclideanSpace ℂ (Fin 3)

Alice's CGLMP phase-basis measurement vector |k⟩_{A,x} = (1/√3) ∑_j ω^{j(k+α_x)} |j⟩ (ω = e^{2πi/3}), a unit vector (aVec_unit).

Equations

• CSD.LF6.CGLMPQutrit.aVec x k = WithLp.toLp 2 fun (j : Fin 3) => (↑√3)⁻¹ * Complex.exp (↑(CSD.LF6.CGLMPQutrit.aAngle x k j) * Complex.I)

noncomputable def CSD.LF6.CGLMPQutrit.bVec (y : Bool) (l : ZMod 3) : EuclideanSpace ℂ (Fin 3)

Bob's CGLMP phase-basis measurement vector |l⟩_{B,y} = (1/√3) ∑_j ω^{-j(l+β_y)} |j⟩, a unit vector (bVec_unit).

Equations

• CSD.LF6.CGLMPQutrit.bVec y l = WithLp.toLp 2 fun (j : Fin 3) => (↑√3)⁻¹ * Complex.exp (↑(CSD.LF6.CGLMPQutrit.bAngle y l j) * Complex.I)

noncomputable def CSD.LF6.CGLMPQutrit.outcome (x y : Bool) (k l : ZMod 3) : EuclideanSpace ℂ (Fin 3 × Fin 3)

The joint measurement outcome vector |k⟩_{A,x} ⊗ |l⟩_{B,y} on EuclideanSpace ℂ (Fin 3 × Fin 3).

Equations

• CSD.LF6.CGLMPQutrit.outcome x y k l = WithLp.toLp 2 fun (p : Fin 3 × Fin 3) => (CSD.LF6.CGLMPQutrit.aVec x k).ofLp p.1 * (CSD.LF6.CGLMPQutrit.bVec y l).ofLp p.2

noncomputable def CSD.LF6.CGLMPQutrit.bornPair (x y : Bool) (k l : ZMod 3) : ℝ

The joint Born probability P(A_x = k, B_y = l) = ‖⟨outcome_{k,l}, Ψ_3⟩‖²: the genuine squared overlap of the outcome vector with the maximally-entangled qutrit maxEntangled 3.

Equations

• CSD.LF6.CGLMPQutrit.bornPair x y k l = ‖inner ℂ (CSD.LF6.CGLMPQutrit.outcome x y k l) (CSD.LF6.maxEntangled 3)‖ ^ 2

noncomputable def CSD.LF6.CGLMPQutrit.baseAngle (x y : Bool) (k l : ZMod 3) : ℝ

The base phase φ = −2π·((k − l) + δ)/3 of the amplitude geometric sum.

Equations

• CSD.LF6.CGLMPQutrit.baseAngle x y k l = -(2 * Real.pi * (↑k.val - ↑l.val + CSD.LF6.CGLMPQutrit.deltaOff x y) / 3)

The outcome vectors are unit vectors (genuine measurements)

theorem CSD.LF6.CGLMPQutrit.aVec_unit (x : Bool) (k : ZMod 3) : ‖aVec x k‖ = 1

Alice's outcome vectors are unit vectors: ‖·‖² = ∑_j 1/3 = 1.

theorem CSD.LF6.CGLMPQutrit.bVec_unit (y : Bool) (l : ZMod 3) : ‖bVec y l‖ = 1

Bob's outcome vectors are unit vectors.

The Born probability closed form (roots-of-unity geometric sum)

theorem CSD.LF6.CGLMPQutrit.inner_outcome_collapse (x y : Bool) (k l : ZMod 3) : inner ℂ (outcome x y k l) (maxEntangled 3) = (↑√3)⁻¹ * ∑ i : Fin 3, (starRingEnd ℂ) ((outcome x y k l).ofLp (i, i))

The inner product with Ψ_3 collapses onto the diagonal: only the (i,i) amplitudes survive the maximally-entangled contraction.

theorem CSD.LF6.CGLMPQutrit.normSq_geom (θ : ℝ) : Complex.normSq (1 + Complex.exp (↑θ * Complex.I) + Complex.exp (↑θ * Complex.I) ^ 2) = 3 + 4 * Real.cos θ + 2 * Real.cos (2 * θ)

‖1 + e^{iθ} + e^{2iθ}‖² = 3 + 4cos θ + 2cos 2θ (the d = 3 geometric-sum modulus).

theorem CSD.LF6.CGLMPQutrit.bornPair_value (x y : Bool) (k l : ZMod 3) : bornPair x y k l = 1 / 27 * (3 + 4 * Real.cos (baseAngle x y k l) + 2 * Real.cos (2 * baseAngle x y k l))

The joint Born probability closed form. From the diagonal collapse, the conjugated amplitudes are (1/3)·(e^{iφ})^i, φ = baseAngle; the geometric sum and normSq_geom give bornPair = (1/27)(3 + 4cos φ + 2cos 2φ).

theorem CSD.LF6.CGLMPQutrit.bornPair_periodic (x y : Bool) (k l : ZMod 3) : bornPair x y k l = bornPair x y (k - l) 0

The joint Born probability depends only on the outcome difference k − l (mod 3): the geometric-sum phase is periodic in the integer difference. This is the genuine "outcome-difference" structure of the CGLMP measurement.

The CGLMP Born table pQM

noncomputable def CSD.LF6.CGLMPQutrit.pQM (x y : Bool) (c : ZMod 3) : ℝ

The genuine CGLMP outcome-difference Born table for Ψ_3: pQM x y c = P(A_x − B_y = c), the sum over outcome pairs (k, l) with k − l = c of the joint Born probabilities bornPair x y k l.

Equations

• CSD.LF6.CGLMPQutrit.pQM x y c = ∑ l : ZMod 3, CSD.LF6.CGLMPQutrit.bornPair x y (c + l) l

theorem CSD.LF6.CGLMPQutrit.pQM_eq (x y : Bool) (c : ZMod 3) : pQM x y c = 3 * bornPair x y c 0

The outcome-difference marginal collapses (via periodicity) to three copies of a single representative Born probability.

theorem CSD.LF6.CGLMPQutrit.pQM_eq_pair (x y : Bool) (k l : ZMod 3) : pQM x y (k - l) = 3 * bornPair x y k l

pQM x y (k − l) = 3 · bornPair x y k l for any representative pair.

theorem CSD.LF6.CGLMPQutrit.pQM_eval (x y : Bool) (k l : ZMod 3) (θ cθ c2θ : ℝ) (hθ : baseAngle x y k l = θ) (h1 : Real.cos θ = cθ) (h2 : Real.cos (2 * θ) = c2θ) : pQM x y (k - l) = 3 * (1 / 27 * (3 + 4 * cθ + 2 * c2θ))

Evaluation helper: pQM x y (k − l) from a computed base angle and its cosines.

The eight CGLMP-relevant Born values

Four positive entries (4 + 2√3)/9 (base angle ± π/6), four negative entries 1/9 (base angle ± π/2), evaluated at the small representatives k − l ∈ {-1, 0, 1}.

theorem CSD.LF6.CGLMPQutrit.pQM_ff_0 : pQM false false 0 = (4 + 2 * √3) / 9

theorem CSD.LF6.CGLMPQutrit.pQM_ff_2 : pQM false false 2 = 1 / 9

theorem CSD.LF6.CGLMPQutrit.pQM_tt_0 : pQM true true 0 = (4 + 2 * √3) / 9

theorem CSD.LF6.CGLMPQutrit.pQM_tt_2 : pQM true true 2 = 1 / 9

theorem CSD.LF6.CGLMPQutrit.pQM_tf_2 : pQM true false 2 = (4 + 2 * √3) / 9

theorem CSD.LF6.CGLMPQutrit.pQM_tf_0 : pQM true false 0 = 1 / 9

theorem CSD.LF6.CGLMPQutrit.pQM_ft_0 : pQM false true 0 = (4 + 2 * √3) / 9

theorem CSD.LF6.CGLMPQutrit.pQM_ft_1 : pQM false true 1 = 1 / 9

The CGLMP value and the violation

theorem CSD.LF6.CGLMPQutrit.bracket_val : ProbabilityTheory.CGLMP.cglmpBracket 3 pQM 0 = 4 * ((4 + 2 * √3) / 9) - 4 * (1 / 9)

The CGLMP bracket at k = 0 on the Ψ_3 Born table: 4·(4+2√3)/9 − 4·(1/9).

theorem CSD.LF6.CGLMPQutrit.cglmp_maxEntangled_qutrit_eq : ProbabilityTheory.CGLMP.cglmp 3 pQM = (12 + 8 * √3) / 9

The maximally-entangled qutrit CGLMP value. I_3 = (12 + 8√3)/9 ≈ 2.8729, computed from Ψ_3's actual Born probabilities under the CGLMP phase-basis measurements.

theorem CSD.LF6.CGLMPQutrit.cglmp_maxEntangled_qutrit_gt_two : ProbabilityTheory.CGLMP.cglmp 3 pQM > 2

The qutrit CGLMP violation (QM side). Ψ_3 violates the CGLMP inequality: its CGLMP value (12 + 8√3)/9 ≈ 2.8729 exceeds the local-hidden-variable bound 2. Genuinely d = 3-intrinsic (the √3 is irrational; no rational / half-integer setting choice violates).

theorem CSD.LF6.CGLMPQutrit.no_lhv_realises_maxEntangled_cglmp {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod 3) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) (hRep : ProbabilityTheory.CGLMP.lhvTable μ A B = pQM) : False

The d = 3-intrinsic no-go (LF6-D, CGLMP routing). No local-hidden-variable model (Λ, μ, A, B) reproduces Ψ_3's actual CGLMP outcome-difference Born statistics pQM: such a model would have CGLMP value cglmpLHV = cglmp 3 pQM = (12 + 8√3)/9 > 2, contradicting the LHV bound cglmp_lhv_bound_three (I_3 ≤ 2). This is the genuinely d = 3 Bell force for the maximally-entangled qutrit, superseding the 2 × 2 Φ⁺ CHSH sector of no_product_partition_realises_maxEntangled.