Empirical/QM/KCBS: the Klyachko–Can–Binicioğlu–Shumovsky pentagon (state-dependent contextuality)

The KCBS inequality is the simplest state-dependent contextuality test — the qutrit analogue of Bell/CHSH, on the pentagon graph C₅. Five rank-1 projectors Π₀,…,Π₄ on ℂ³ are arranged so that consecutive ones (cyclically) are orthogonal (mutually exclusive outcomes). Any noncontextual hidden-variable model assigns each Πᵢ a definite value in {0,1} respecting the exclusivity, and then

K₅ := ∑ᵢ ⟨Πᵢ⟩ ≤ 2

— because the independence number of the 5-cycle C₅ is 2 (no three of five cyclically-arranged vertices are pairwise non-adjacent). Quantum mechanics reaches √5 ≈ 2.236 > 2 on the pentagon "apex" state, violating noncontextuality.

This module proves the noncontextual bound over a genuine measure-theoretic model (five {0,1} observables with cyclic exclusivity on a probability space), mirroring the CHSH-LHV / Leggett–Garg pattern:

• kcbs_pointwise — the C₅ combinatorial core: ∑ xᵢ ≤ 2 for xᵢ ∈ {0,1} with xᵢ·xᵢ₊₁ = 0.
• kcbs_noncontextual_bound — ∑ᵢ ∫ Xᵢ ≤ 2 for any such model.

The quantum √5 violation (the pentagon ℂ³ vectors + golden-ratio orthogonality) is a separate, heavier construction and is not in this module.

Experimental verification: Lapkiewicz et al. 2011 (single photons, three-level). CSD note: KCBS is state-dependent contextuality — Gleason/KS-style noncontextuality is exactly the assumption CSD's contextual (apparatus-fixed) outcome regions deny, so CSD is unconstrained by it.

References

Empirical/QM/Crypto/E91.lean (the LHV-bound measure-theoretic pattern); Empirical/QM/LeggettGarg.lean (the pointwise-inequality + integral_mono pattern); Empirical/CSD/Contextuality/KS18.lean (state-independent contextuality, for contrast).

theorem CSD.Empirical.QM.KCBS.kcbs_pointwise {x₀ x₁ x₂ x₃ x₄ : ℝ} (h₀ : x₀ = 0 ∨ x₀ = 1) (h₁ : x₁ = 0 ∨ x₁ = 1) (h₂ : x₂ = 0 ∨ x₂ = 1) (h₃ : x₃ = 0 ∨ x₃ = 1) (h₄ : x₄ = 0 ∨ x₄ = 1) (e₀ : x₀ * x₁ = 0) (e₁ : x₁ * x₂ = 0) (e₂ : x₂ * x₃ = 0) (e₃ : x₃ * x₄ = 0) (e₄ : x₄ * x₀ = 0) : x₀ + x₁ + x₂ + x₃ + x₄ ≤ 2

The pentagon (C₅) combinatorial core. For five {0,1} values with cyclic consecutive-exclusivity xᵢ·xᵢ₊₁ = 0, at most two can be 1: ∑ xᵢ ≤ 2 (the independence number of C₅).

theorem CSD.Empirical.QM.KCBS.kcbs_noncontextual_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X₀ X₁ X₂ X₃ X₄ : Ω → ℝ) (h₀ : ∀ (ω : Ω), X₀ ω = 0 ∨ X₀ ω = 1) (h₁ : ∀ (ω : Ω), X₁ ω = 0 ∨ X₁ ω = 1) (h₂ : ∀ (ω : Ω), X₂ ω = 0 ∨ X₂ ω = 1) (h₃ : ∀ (ω : Ω), X₃ ω = 0 ∨ X₃ ω = 1) (h₄ : ∀ (ω : Ω), X₄ ω = 0 ∨ X₄ ω = 1) (e₀ : ∀ (ω : Ω), X₀ ω * X₁ ω = 0) (e₁ : ∀ (ω : Ω), X₁ ω * X₂ ω = 0) (e₂ : ∀ (ω : Ω), X₂ ω * X₃ ω = 0) (e₃ : ∀ (ω : Ω), X₃ ω * X₄ ω = 0) (e₄ : ∀ (ω : Ω), X₄ ω * X₀ ω = 0) (i₀ : MeasureTheory.Integrable X₀ μ) (i₁ : MeasureTheory.Integrable X₁ μ) (i₂ : MeasureTheory.Integrable X₂ μ) (i₃ : MeasureTheory.Integrable X₃ μ) (i₄ : MeasureTheory.Integrable X₄ μ) : ∫ (ω : Ω), X₀ ω ∂μ + ∫ (ω : Ω), X₁ ω ∂μ + ∫ (ω : Ω), X₂ ω ∂μ + ∫ (ω : Ω), X₃ ω ∂μ + ∫ (ω : Ω), X₄ ω ∂μ ≤ 2

The KCBS noncontextual bound K₅ ≤ 2. For any noncontextual model — a probability space with five {0,1}-valued observables X₀,…,X₄ obeying cyclic exclusivity Xᵢ·Xᵢ₊₁ = 0 — the pentagon sum ∑ᵢ ⟨Xᵢ⟩ ≤ 2. Proved from the C₅ pointwise bound by integral monotonicity.

The quantum √5 violation — the pentagon on ℝ³

noncomputable def CSD.Empirical.QM.KCBS.cc : ℝ

cos θ for the pentagon apex angle, with cos²θ = 1/√5.

Equations

• CSD.Empirical.QM.KCBS.cc = √(1 / √5)

noncomputable def CSD.Empirical.QM.KCBS.ss : ℝ

sin θ, with sin²θ = 1 − 1/√5.

Equations

• CSD.Empirical.QM.KCBS.ss = √(1 - 1 / √5)

theorem CSD.Empirical.QM.KCBS.sqrt5_pos : 0 < √5

theorem CSD.Empirical.QM.KCBS.sqrt5_sq : √5 ^ 2 = 5

theorem CSD.Empirical.QM.KCBS.one_le_sqrt5 : 1 ≤ √5

theorem CSD.Empirical.QM.KCBS.cc_sq : cc ^ 2 = 1 / √5

theorem CSD.Empirical.QM.KCBS.ss_sq : ss ^ 2 = 1 - 1 / √5

noncomputable def CSD.Empirical.QM.KCBS.kvA (a : ℝ) : Fin 3 → ℝ

A pentagon unit vector at azimuthal angle a: (sinθ·cos a, sinθ·sin a, cosθ).

Equations

• CSD.Empirical.QM.KCBS.kvA a = ![CSD.Empirical.QM.KCBS.ss * Real.cos a, CSD.Empirical.QM.KCBS.ss * Real.sin a, CSD.Empirical.QM.KCBS.cc]

def CSD.Empirical.QM.KCBS.apex : Fin 3 → ℝ

The apex state |ψ⟩ = (0,0,1).

Equations

• CSD.Empirical.QM.KCBS.apex = ![0, 0, 1]

def CSD.Empirical.QM.KCBS.dot3 (u v : Fin 3 → ℝ) : ℝ

Real 3-vector dot product.

Equations

• CSD.Empirical.QM.KCBS.dot3 u v = u 0 * v 0 + u 1 * v 1 + u 2 * v 2

noncomputable def CSD.Empirical.QM.KCBS.ang : Fin 5 → ℝ

The five pentagon azimuths 4πk/5.

Equations

• CSD.Empirical.QM.KCBS.ang = ![0, 4 * Real.pi / 5, 8 * Real.pi / 5, 12 * Real.pi / 5, 16 * Real.pi / 5]

noncomputable def CSD.Empirical.QM.KCBS.kv (k : Fin 5) : Fin 3 → ℝ

The five KCBS pentagon vectors.

Equations

• CSD.Empirical.QM.KCBS.kv k = CSD.Empirical.QM.KCBS.kvA (CSD.Empirical.QM.KCBS.ang k)

theorem CSD.Empirical.QM.KCBS.dot_kvA (a b : ℝ) : dot3 (kvA a) (kvA b) = ss ^ 2 * Real.cos (a - b) + cc ^ 2

The dot product of two pentagon vectors folds to sin²θ·cos(a−b) + cos²θ.

theorem CSD.Empirical.QM.KCBS.cos_4pi5 : Real.cos (4 * Real.pi / 5) = -(1 + √5) / 4

cos(4π/5) = −(1+√5)/4.

theorem CSD.Empirical.QM.KCBS.orth_of_cos {a b : ℝ} (h : Real.cos (a - b) = -(1 + √5) / 4) : dot3 (kvA a) (kvA b) = 0

Orthogonality from the folded dot product: if cos(a−b) = cos(4π/5) then the vectors are orthogonal (the pentagon overlap identity, using √5² = 5).

theorem CSD.Empirical.QM.KCBS.kv_orth (k : Fin 5) : dot3 (kv k) (kv (k + 1)) = 0

Consecutive pentagon vectors are orthogonal (the exclusivity structure). Each cyclic azimuth gap reduces to cos(4π/5).

theorem CSD.Empirical.QM.KCBS.kv_unit (k : Fin 5) : dot3 (kv k) (kv k) = 1

Each pentagon vector is a unit vector.

theorem CSD.Empirical.QM.KCBS.kv_apex_born (k : Fin 5) : dot3 apex (kv k) ^ 2 = 1 / √5

The apex overlap Born weight ⟨ψ|Πₖ|ψ⟩ = cos²θ = 1/√5.

theorem CSD.Empirical.QM.KCBS.kcbs_qm_value : ∑ k : Fin 5, dot3 apex (kv k) ^ 2 = √5

The quantum KCBS value is √5. ∑ₖ ⟨ψ|Πₖ|ψ⟩ = 5·(1/√5) = √5.

theorem CSD.Empirical.QM.KCBS.kcbs_quantum_violation : 2 < ∑ k : Fin 5, dot3 apex (kv k) ^ 2

The quantum violation K₅ = √5 > 2. The pentagon apex state exceeds the noncontextual bound 2, so quantum mechanics violates KCBS noncontextuality.