LF6-D (QM side, general `d`): `Ψ_d` violates the CGLMP inequality for every `d ≥ 2` #

Category: 3-Local (the general-d-intrinsic Bell violation for Ψ_d, the QM-side payoff of the CGLMP infrastructure Mathlib/Probability/CGLMP.lean, extending the d = 3 qutrit violation CGLMPQutrit.cglmp_maxEntangled_qutrit_gt_two to ALL d ≥ 2).

What is proved (general `d`, no dimension restriction) #

Under the standard CGLMP phase-basis measurements on Ψ_d = maxEntangled d (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 for arbitrary d:

pQM_closed : pQM x y c = 1 / (2 d² sin²(π(c.val + δ_xy)/d)), the standard maximally-entangled CGLMP closed form, DERIVED via the d-th-roots-of-unity Dirichlet / Fejér kernel dirichlet_kernel (‖∑_{j<d} e^{ijφ}‖² = sin²(dφ/2)/sin²(φ/2)), the quarter-integer numerator sin²(π(m+δ)) = 1/2 (sin_sq_pi_delta), and the diagonal contraction with Ψ_d (inner_outcome_collapse, hconj_term). No value asserted.
cglmpBracket_closed : the CGLMP bracket at index k in closed form (2/d²)(csc²(π(k+1/4)/d) − csc²(π(k+3/4)/d)) (bracketClosed); hence cglmp_maxEntangled_qudit_closed gives the full general-d CGLMP value as ∑_{k<⌊d/2⌋} (1 − 2k/(d−1)) · bracketClosed d k.
cglmp_maxEntangled_qudit_gt_two (hd : 2 ≤ d) : the general-d violation cglmp d pQM > 2. This is a genuine analytic inequality on the d-dependent trig sum, proved for EVERY d ≥ 2: every bracket term is nonnegative (bracketClosed_nonneg, via sin monotonicity on (0, π/2]) and every coefficient is nonnegative (coeff_nonneg), so the sum dominates its k = 0 term (Finset.single_le_sum), and the k = 0 term alone exceeds 2 (bracket_zero_gt_two) via sin x ≤ x on the π/(4d) arm and Jordan's inequality sin x ≥ 2x/π (jordan_sin, from strictConcaveOn_sin_Icc) on the 3π/(4d) arm, giving the uniform bound bracketClosed d 0 ≥ 32/π² − 8/9 > 2 (π < 3.15). No monotonicity in d needed; the single k = 0 term suffices for all d.
no_lhv_realises_maxEntangled_cglmp_d (hd : 2 ≤ d) : the general-d Bell force. No local-hidden-variable model reproducing Ψ_d's CGLMP statistics pQM exists: it would have cglmpLHV = cglmp d pQM > 2, contradicting cglmp_lhv_bound (I_d ≤ 2). Together with the general-d LHV bound this closes the statistical non-locality axis at FULL dimensional generality (matching the GHZ_n deterministic axis).

Honest scope #

Genuine computation from Ψ_d's actual Born probabilities: bornPair is a squared inner product with maxEntangled d, the outcome vectors are unit CGLMP phase-basis vectors, and pQM is the genuine outcome-difference marginal. The closed form is derived, not asserted.
The > 2 bound is a REAL analytic proof valid for every d ≥ 2 (not decide over a finite dimension range, not axiomatised). It uses only the k = 0 bracket term plus nonnegativity of the tail; the CGLMP value increases towards ≈ 2.9696 as d → ∞, but only the uniform lower bound 32/π² − 8/9 ≈ 2.35 is needed.
Foundational-triple-only (no busch_effect_gleason; the roots-of-unity sums, the trig inequalities, and the finite LHV optimisation are all Gleason-free).

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

LF6-D (QM side, general d): Ψ_d violates the CGLMP inequality for every d ≥ 2 #

What is proved (general d, no dimension restriction) #

Honest scope #

Jordan + reduction infra #

pQM and its closed form #

The bracket closed form #

Nonnegativity of coefficients and bracket terms #

The k=0 bracket exceeds 2 (the analytic lower bound) #

The general-d CGLMP violation and the Bell force #

LF6-D (QM side, general `d`): `Ψ_d` violates the CGLMP inequality for every `d ≥ 2` #

What is proved (general `d`, no dimension restriction) #