The CGLMP qudit Bell inequality and its local-hidden-variable bound

Category: Cat-1 (CSD-free general qudit Bell theory; a Mathlib-upstream-staging candidate). Natural namespace ProbabilityTheory.CGLMP, no CSD wrapper.

This file formalises the Collins-Gisin-Linden-Massar-Popescu (CGLMP 2002) Bell inequality for two parties, two settings per party, and d outcomes per setting. It is the d-outcome generalisation of the two-outcome CHSH/Bell bound (|S| <= 2).

The local-hidden-variable model

Two parties. Each has two measurement settings (indexed by Bool), each setting having d outcomes (in ZMod d). A deterministic local-hidden-variable (LHV) model is a probability space (Λ, μ) of hidden variables together with local response functions

A B : Bool → Λ → ZMod d,

with A s l Alice's outcome for setting s at hidden state l (Bob's B likewise). Setting-locality on the shared Λ is the factorisation assumption. The joint LHV probability of the mod-d outcome relation A_x - B_y = k is

lhvTable μ A B x y k = (μ {l | A x l - B y l = k}).toReal.

The CGLMP functional I_d

Following the standard expression (settings A_1 = A false, A_2 = A true, B_1 = B false, B_2 = B true, all outcome relations mod d):

I_d = ∑_{k=0}^{⌊d/2⌋-1} (1 - 2k/(d-1)) *
      ( [P(A_1=B_1+k) + P(B_1=A_2+k+1) + P(A_2=B_2+k) + P(B_2=A_1+k)]
      - [P(A_1=B_1-k-1) + P(B_1=A_2-k) + P(A_2=B_2-k-1) + P(B_2=A_1-k-1)] ).

Every term is rewritten in the single orientation P(A_x - B_y = m) using P(B_b = A_a + m) = P(A_a - B_b = -m); the result is cglmp applied to an abstract probability table p : Bool → Bool → ZMod d → K. cglmpLHV is cglmp on the LHV table. The classical (CGLMP) bound is I_d ≤ 2, and it is tight (achieved by a deterministic strategy; see scaledDetZ and the numeric facts).

Results

• cglmpLHV_eq_integral (general d): the CGLMP functional of an LHV model is the μ-average of its deterministic (per-hidden-state) CGLMP values. This is the linearity/reduction identity: an LHV model is a mixture of deterministic product strategies.
• cglmpLHV_le_of_det_le (general d, load-bearing): if every deterministic strategy has CGLMP value ≤ C, then every LHV model has cglmpLHV ≤ C. This reduces the continuous LHV bound to the finite optimisation over (ZMod d)^4 strategies.
• cglmpDet_le_two, cglmp_lhv_bound_two / _three / _four: the LHV bound I_d ≤ 2 for d = 2, 3, 4. The finite optimisation is discharged by decide on the division-cleared integer functional scaledDetZ over (ZMod d)^4.
• scaledDetZ_le_general, cglmp_lhv_bound (general d): the numeric bound scaledDetZ ≤ 2*(d-1) and hence I_d ≤ 2 for every d ≥ 2, proved by the CGLMP counting argument (the sawtooth reduction + the cyclic constraint), not by decide. This closes the numeric bound at full dimensional generality.
• scaledDetZ_tight_general, cglmp_detTable_tight_general (general d): the bound is tight — the all-zero local strategy attains scaledDetZ = 2(d-1), i.e. I_d = 2, for every d ≥ 2. So 2 is the EXACT local-hidden-variable optimum in every dimension (generalising the decide anchors scaledDetZ_three_tight / _four_tight).

Honest scope

• The reduction (cglmpLHV_eq_integral, cglmpLHV_le_of_det_le) is general d: the LHV-to-finite-optimisation bridge holds for every d ≥ 2.
• The numeric bound I_d ≤ 2 is proved for d = 2, 3, 4 by decide on the 81 (d = 3) / 256 (d = 4) deterministic strategies (concrete anchors) AND for every d ≥ 2 by the CGLMP counting argument (scaledDetZ_le_general, cglmp_lhv_bound). The general-d bound is the sawtooth reduction scaledDetZ = -2 - 2·d·t (t ≥ -1 integer) forced by the cyclic constraint on the four outcome differences; it is a genuine proof, not decide (which only reduces at fixed d) and not axiomatised. d = 3 is the genuine first qudit Bell inequality beyond CHSH.
• d = 2 reduces to the CHSH bound: ⌊2/2⌋ = 1, coefficient 1, and the eight terms are the CHSH probabilities. This is a sanity anchor, not the deliverable; the two-outcome CHSH |S| ≤ 2 already lives elsewhere.

Reference: Collins, Gisin, Linden, Massar, Popescu, Phys. Rev. Lett. 88, 040404 (2002).

The CGLMP functional on an abstract probability table

def ProbabilityTheory.CGLMP.cglmpBracket {K : Type u_1} [Field K] (d : ℕ) (p : Bool → Bool → ZMod d → K) (k : ℕ) : K

The CGLMP bracket at index k: the eight-term signed combination of joint outcome-relation probabilities. p x y m reads P(A_x - B_y = m). The four "positive" terms and four "negative" terms are the standard CGLMP grouping, rewritten into the single orientation A_x - B_y.

Equations

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

def ProbabilityTheory.CGLMP.cglmp {K : Type u_1} [Field K] (d : ℕ) (p : Bool → Bool → ZMod d → K) : K

The CGLMP functional I_d on an abstract probability table p: ∑_{k<⌊d/2⌋} (1 - 2k/(d-1)) * cglmpBracket d p k.

Equations

• ProbabilityTheory.CGLMP.cglmp d p = ∑ k ∈ Finset.range (d / 2), (1 - 2 * ↑k / (↑d - 1)) * ProbabilityTheory.CGLMP.cglmpBracket d p k

def ProbabilityTheory.CGLMP.detTable {K : Type u_1} [Field K] {d : ℕ} (a1 a2 b1 b2 : ZMod d) : Bool → Bool → ZMod d → K

The deterministic probability table for a fixed local strategy (a1, a2, b1, b2) (Alice's outcomes for settings false, true, then Bob's): P(A_x - B_y = k) is 1 if the strategy realises the relation, else 0.

Equations

• ProbabilityTheory.CGLMP.detTable a1 a2 b1 b2 x y k = if ((bif x then a2 else a1) - bif y then b2 else b1) = k then 1 else 0

The division-cleared integer functional (for the finite optimisation)

decide cannot reduce the rational/real functional (Rat/Real arithmetic does not compute in the kernel). Multiplying the inequality I_d ≤ 2 through by (d - 1) > 0 clears the denominators, giving an integer-valued functional scaledDetZ that decide can evaluate over the finite strategy space.

def ProbabilityTheory.CGLMP.detIndZ {d : ℕ} (a b k : ZMod d) : ℤ

The integer indicator ⟦a - b = k⟧ ∈ {0, 1}.

Equations

• ProbabilityTheory.CGLMP.detIndZ a b k = if a - b = k then 1 else 0

def ProbabilityTheory.CGLMP.bracketZ {d : ℕ} (a1 a2 b1 b2 : ZMod d) (k : ℕ) : ℤ

The integer CGLMP bracket (same eight-term structure as cglmpBracket, over ℤ).

Equations

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

def ProbabilityTheory.CGLMP.scaledDetZ {d : ℕ} (a1 a2 b1 b2 : ZMod d) : ℤ

The division-cleared integer CGLMP value of a deterministic strategy: (d - 1) * I_d^det = ∑_{k<⌊d/2⌋} (d - 1 - 2k) * bracketZ. Kernel-decide-able over (ZMod d)^4.

Equations

• ProbabilityTheory.CGLMP.scaledDetZ a1 a2 b1 b2 = ∑ k ∈ Finset.range (d / 2), (↑d - 1 - 2 * ↑k) * ProbabilityTheory.CGLMP.bracketZ a1 a2 b1 b2 k

theorem ProbabilityTheory.CGLMP.cglmpBracket_detTable_eq {d : ℕ} (a1 a2 b1 b2 : ZMod d) (k : ℕ) : cglmpBracket d (detTable a1 a2 b1 b2) k = ↑(bracketZ a1 a2 b1 b2 k)

The real deterministic bracket equals the integer bracket cast to ℝ.

theorem ProbabilityTheory.CGLMP.cglmp_detTable_eq {d : ℕ} (hd : 2 ≤ d) (a1 a2 b1 b2 : ZMod d) : cglmp d (detTable a1 a2 b1 b2) = ↑(scaledDetZ a1 a2 b1 b2) / (↑d - 1)

The real deterministic CGLMP value equals scaledDetZ / (d - 1) (for d ≥ 2).

The LHV model and the CGLMP functional on it

noncomputable def ProbabilityTheory.CGLMP.lhvTable {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} (μ : MeasureTheory.Measure Λ) (A B : Bool → Λ → ZMod d) : Bool → Bool → ZMod d → ℝ

The joint LHV probability table: P(A_x - B_y = k) = μ {l | A x l - B y l = k} (as a real number).

Equations

• ProbabilityTheory.CGLMP.lhvTable μ A B x y k = (μ {l : Λ | A x l - B y l = k}).toReal

noncomputable def ProbabilityTheory.CGLMP.cglmpLHV {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} (μ : MeasureTheory.Measure Λ) (A B : Bool → Λ → ZMod d) : ℝ

The CGLMP functional of an LHV model.

Equations

• ProbabilityTheory.CGLMP.cglmpLHV μ A B = ProbabilityTheory.CGLMP.cglmp d (ProbabilityTheory.CGLMP.lhvTable μ A B)

theorem ProbabilityTheory.CGLMP.lhvTable_eq_integral {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} [NeZero d] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) (x y : Bool) (k : ZMod d) : lhvTable μ A B x y k = ∫ (l : Λ), detTable (A false l) (A true l) (B false l) (B true l) x y k ∂μ

Each LHV probability is the integral of the deterministic indicator over the hidden variable: P(A_x - B_y = k) = ∫ ⟦A x l - B y l = k⟧ dμ.

theorem ProbabilityTheory.CGLMP.detTable_integrable {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} [NeZero d] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) (x y : Bool) (k : ZMod d) : MeasureTheory.Integrable (fun (l : Λ) => detTable (A false l) (A true l) (B false l) (B true l) x y k) μ

The deterministic indicator is integrable (bounded by 1, measurable).

The deterministic reduction (general d)

theorem ProbabilityTheory.CGLMP.cglmpLHV_eq_integral {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} [NeZero d] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) : cglmpLHV μ A B = ∫ (l : Λ), cglmp d (detTable (A false l) (A true l) (B false l) (B true l)) ∂μ

The CGLMP reduction identity (general d). The CGLMP functional of an LHV model is the μ-average of the deterministic (per-hidden-state) CGLMP values. An LHV model is a mixture of the deterministic product strategies (A false l, A true l, B false l, B true l); cglmp is linear in the probability table, and the integral commutes with the finite linear combination.

theorem ProbabilityTheory.CGLMP.cglmpDet_integrable {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} [NeZero d] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) : MeasureTheory.Integrable (fun (l : Λ) => cglmp d (detTable (A false l) (A true l) (B false l) (B true l))) μ

The pointwise deterministic CGLMP value is integrable over the hidden variable (finite linear combination of integrable indicators).

theorem ProbabilityTheory.CGLMP.cglmpLHV_le_of_det_le {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} [NeZero d] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) (C : ℝ) (hdet : ∀ (a1 a2 b1 b2 : ZMod d), cglmp d (detTable a1 a2 b1 b2) ≤ C) : cglmpLHV μ A B ≤ C

The LHV-to-finite-optimisation bound (general d, load-bearing). If every deterministic strategy (a1, a2, b1, b2) ∈ (ZMod d)^4 has CGLMP value ≤ C, then every LHV model has cglmpLHV ≤ C. This is the convexity/averaging step: it reduces the continuous LHV bound to a finite optimisation over the deterministic strategies.

The finite optimisation, discharged for d = 2, 3, 4

theorem ProbabilityTheory.CGLMP.scaledDetZ_le_two (a1 a2 b1 b2 : ZMod 2) : scaledDetZ a1 a2 b1 b2 ≤ 2 * (2 - 1)

Finite check d = 2 (16 strategies): the division-cleared integer functional is ≤ 2*(d-1).

theorem ProbabilityTheory.CGLMP.scaledDetZ_le_three (a1 a2 b1 b2 : ZMod 3) : scaledDetZ a1 a2 b1 b2 ≤ 2 * (3 - 1)

Finite check d = 3 (81 strategies): the first qudit Bell inequality beyond CHSH.

theorem ProbabilityTheory.CGLMP.scaledDetZ_le_four (a1 a2 b1 b2 : ZMod 4) : scaledDetZ a1 a2 b1 b2 ≤ 2 * (4 - 1)

Finite check d = 4 (256 strategies), genuinely rational coefficient.

theorem ProbabilityTheory.CGLMP.cglmpDet_le_two {d : ℕ} (hd : 2 ≤ d) (hb : ∀ (a1 a2 b1 b2 : ZMod d), scaledDetZ a1 a2 b1 b2 ≤ 2 * (↑d - 1)) (a1 a2 b1 b2 : ZMod d) : cglmp d (detTable a1 a2 b1 b2) ≤ 2

The deterministic CGLMP bound I_d^det ≤ 2, given the integer optimisation scaledDetZ ≤ 2*(d-1). Bridges the decide-friendly integer bound to the real functional via cglmp_detTable_eq.

theorem ProbabilityTheory.CGLMP.cglmp_lhv_bound_two {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod 2) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) : cglmpLHV μ A B ≤ 2

CGLMP LHV bound, d = 2. Reduces to CHSH; sanity anchor.

theorem ProbabilityTheory.CGLMP.cglmp_lhv_bound_three {Λ : 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)) : cglmpLHV μ A B ≤ 2

CGLMP LHV bound, d = 3. The first genuine qudit Bell inequality beyond CHSH: every deterministic local-hidden-variable model of two qutrits obeys I_3 ≤ 2.

theorem ProbabilityTheory.CGLMP.cglmp_lhv_bound_four {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (A B : Bool → Λ → ZMod 4) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) : cglmpLHV μ A B ≤ 2

CGLMP LHV bound, d = 4. I_4 ≤ 2 (genuinely rational coefficient 1 - 2/3).

Tightness (the bound 2 is achieved)

theorem ProbabilityTheory.CGLMP.scaledDetZ_three_tight : ∃ (a1 : ZMod 3) (a2 : ZMod 3) (b1 : ZMod 3) (b2 : ZMod 3), scaledDetZ a1 a2 b1 b2 = 2 * (3 - 1)

The d = 3 bound is tight. Some deterministic strategy attains scaledDetZ = 2*(d-1), i.e. I_3^det = 2. Together with scaledDetZ_le_three this certifies the CGLMP classical bound is exactly 2 (achieved), not a loose over-estimate. Hence the functional is the genuine CGLMP inequality, not a relabelled trivial bound.

theorem ProbabilityTheory.CGLMP.scaledDetZ_four_tight : ∃ (a1 : ZMod 4) (a2 : ZMod 4) (b1 : ZMod 4) (b2 : ZMod 4), scaledDetZ a1 a2 b1 b2 = 2 * (4 - 1)

The d = 4 bound is tight.

The general-d LHV bound (the CGLMP counting argument)

The numeric optimisation scaledDetZ ≤ 2*(d-1) is discharged for all d (not merely d = 2, 3, 4 via decide) by the CGLMP counting argument. The core is the sawtooth reduction: the division-cleared functional collapses to four values of the single linear-on-representatives sawtooth S(r) = d - 1 - 2·val(r), evaluated at the four outcome differences a₁−b₁, a₂−b₁, a₂−b₂, (a₁−b₂)−1. The cyclic constraint (a₁−b₁) − (a₂−b₁) + (a₂−b₂) − ((a₁−b₂)−1) = 1 (mod d) then forces scaledDetZ = -2 - 2·d·t with t ≥ -1 (integer), whence scaledDetZ ≤ 2(d-1), tight at t = -1. No decide, no dimension restriction.

def ProbabilityTheory.CGLMP.sawtooth (d : ℕ) (r : ZMod d) : ℤ

The CGLMP sawtooth S(r) = d - 1 - 2·val(r): the single coefficient function to which the division-cleared functional collapses. Linear in the standard representative val r; its antisymmetric arm structure (the low arm k and the high arm d-1-k) is exactly the CGLMP weight pattern d - 1 - 2k.

Equations

• ProbabilityTheory.CGLMP.sawtooth d r = ↑d - 1 - 2 * ↑r.val

theorem ProbabilityTheory.CGLMP.val_neg_sub_one {d : ℕ} [NeZero d] (r : ZMod d) : (-r - 1).val = d - 1 - r.val

val (-r - 1) = d - 1 - val r: the reflection carrying the low arm to the high arm.

theorem ProbabilityTheory.CGLMP.sawtooth_sum_pos {d : ℕ} [NeZero d] (r : ZMod d) : (∑ k ∈ Finset.range (d / 2), (↑d - 1 - 2 * ↑k) * if r = ↑k then 1 else 0) = if r.val < d / 2 then ↑d - 1 - 2 * ↑r.val else 0

The positive-arm collector: ∑_k (d-1-2k)·⟦r = k⟧ picks out the single term k = val r when val r < ⌊d/2⌋.

theorem ProbabilityTheory.CGLMP.sawtooth_sum_neg {d : ℕ} [NeZero d] (r : ZMod d) : (∑ k ∈ Finset.range (d / 2), (↑d - 1 - 2 * ↑k) * if r = -↑k - 1 then 1 else 0) = if d - 1 - r.val < d / 2 then ↑d - 1 - 2 * ↑(d - 1 - r.val) else 0

The negative-arm collector: ∑_k (d-1-2k)·⟦r = -k-1⟧ picks out the reflected term k = d-1-val r.

theorem ProbabilityTheory.CGLMP.sawtooth_weighted_sum {d : ℕ} [NeZero d] (r : ZMod d) : ∑ k ∈ Finset.range (d / 2), (↑d - 1 - 2 * ↑k) * ((if r = ↑k then 1 else 0) - if r = -↑k - 1 then 1 else 0) = sawtooth d r

The sawtooth collapse. The weighted difference of the two arm collectors equals the sawtooth S(r) for every r (both arms and the middle fixed point covered by the same linear formula d - 1 - 2·val r).

theorem ProbabilityTheory.CGLMP.bracketZ_eq_sawtooth_summand {d : ℕ} (a1 a2 b1 b2 : ZMod d) (k : ℕ) : bracketZ a1 a2 b1 b2 k = ((if a1 - b1 = ↑k then 1 else 0) - if a1 - b1 = -↑k - 1 then 1 else 0) - ((if a2 - b1 = ↑k then 1 else 0) - if a2 - b1 = -↑k - 1 then 1 else 0) + ((if a2 - b2 = ↑k then 1 else 0) - if a2 - b2 = -↑k - 1 then 1 else 0) - ((if a1 - b2 - 1 = ↑k then 1 else 0) - if a1 - b2 - 1 = -↑k - 1 then 1 else 0)

The per-index bracket identity. The integer CGLMP bracket at index k equals the signed combination of the four differences' arm summands. This is the purely combinatorial rewrite of bracketZ into the sawtooth arms; the a₁−b₂ difference carries the -1 shift (via (a₁−b₂)−1).

theorem ProbabilityTheory.CGLMP.scaledDetZ_eq_sawtooth {d : ℕ} [NeZero d] (a1 a2 b1 b2 : ZMod d) : scaledDetZ a1 a2 b1 b2 = sawtooth d (a1 - b1) - sawtooth d (a2 - b1) + sawtooth d (a2 - b2) - sawtooth d (a1 - b2 - 1)

The sawtooth reduction (general d). The division-cleared functional equals the signed sum of the four sawtooth values at the outcome differences. This is the structural half of the counting argument: scaledDetZ is fully determined by the four differences and the single sawtooth S.

theorem ProbabilityTheory.CGLMP.scaledDetZ_le_general {d : ℕ} [NeZero d] (hd : 2 ≤ d) (a1 a2 b1 b2 : ZMod d) : scaledDetZ a1 a2 b1 b2 ≤ 2 * (↑d - 1)

The general-d CGLMP numeric bound (the counting argument). For every deterministic strategy (a₁, a₂, b₁, b₂) ∈ (ZMod d)^4 and every d ≥ 2, scaledDetZ ≤ 2*(d-1). This discharges the named residual cglmpDet_le_two's hypothesis for all d: the sawtooth reduction gives scaledDetZ = -2 - 2·d·t where t is the integer witnessing the cyclic constraint ∑(differences) ≡ 1 (mod d), and the outcome-difference bounds 0 ≤ val < d force t ≥ -1, hence scaledDetZ ≤ 2(d-1) (tight at t = -1; cf. scaledDetZ_three_tight, scaledDetZ_four_tight).

theorem ProbabilityTheory.CGLMP.cglmp_lhv_bound {Λ : Type u_1} [MeasurableSpace Λ] {d : ℕ} (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (hd : 2 ≤ d) (A B : Bool → Λ → ZMod d) (hA : ∀ (x : Bool), Measurable (A x)) (hB : ∀ (y : Bool), Measurable (B y)) : cglmpLHV μ A B ≤ 2

The CGLMP LHV bound, general d. For every d ≥ 2 and every deterministic local-hidden-variable model of two d-outcome parties, the CGLMP functional obeys I_d ≤ 2. Composes the LHV-to-finite-optimisation reduction (cglmpLHV_le_of_det_le) with the general-d counting argument (scaledDetZ_le_general) through the integer-to-real bridge (cglmpDet_le_two). This closes the numeric bound at full dimensional generality; the d = 2, 3, 4 decide variants (cglmp_lhv_bound_two/_three/_four) are the concrete anchors.

Tightness of the general-d bound

The general bound cglmp_lhv_bound (I_d ≤ 2) is not merely an upper estimate — it is saturated at every d by an explicit local strategy. The all-zero deterministic strategy (a₁,a₂,b₁,b₂) = 0 achieves the maximum: three sawtooth arms sit at S(0) = d-1 and the shifted arm at the reflected minimum S(-1) = -(d-1), summing to scaledDetZ = 2(d-1), i.e. I_d = 2. This generalises the decide-proved anchors scaledDetZ_three_tight / scaledDetZ_four_tight to all d.

theorem ProbabilityTheory.CGLMP.scaledDetZ_tight_general {d : ℕ} [NeZero d] : scaledDetZ 0 0 0 0 = 2 * (↑d - 1)

The integer functional is tight at every d. The all-zero strategy gives scaledDetZ 0 0 0 0 = 2(d-1) — the maximum permitted by scaledDetZ_le_general (attained at t = -1). Three arms at S(0) = d-1, the shifted arm at S(-1) = -(d-1).

theorem ProbabilityTheory.CGLMP.cglmp_detTable_tight_general {d : ℕ} (hd : 2 ≤ d) : cglmp d (detTable 0 0 0 0) = 2

The CGLMP LHV bound I_d ≤ 2 is TIGHT at every d. The local deterministic strategy (0,0,0,0) (the LHV table detTable 0 0 0 0) achieves I_d = 2 exactly, for every d ≥ 2: cglmp d (detTable 0 0 0 0) = 2. Together with cglmp_lhv_bound (I_d ≤ 2), this shows 2 is the EXACT local-hidden-variable optimum in every dimension — the CGLMP bound is saturated, not merely an upper estimate.