LF6-6: Gisin's theorem — every entangled pure two-qubit state violates CHSH

Category: 6-Local (closes the LF6-6 non-factorisation witness beyond maximal entanglement).

LF6/PartialSchmidtCorrelation.lean computes, from the Hilbert space, the Pauli correlation of the general real-Schmidt two-qubit state Ψ(c,s) = c|00⟩ + s|11⟩:

⟨Ψ(c,s) | σ·a ⊗ σ·b | Ψ(c,s)⟩ = a_z b_z + 2cs·(a_x b_x − a_y b_y)      (`psQubit_pauli_correlation`)

and there named the remaining cost of LF6-6: forcing non-factorisation for unequal Schmidt coefficients needs a CHSH violation for a non-maximally-entangled state — Gisin's theorem. The LF6-D Φ⁺ reduction and the CGLMP Dirichlet kernel are both specific to equal weights and do not port. This module supplies that witness.

The result

gisin_chsh_violation : for every entangled state (0 < c, 0 < s, c² + s² = 1) there are detector settings a, a', b, b' with 2 < psCHSH c s a a' b b' — the CHSH combination of the partial-Schmidt correlation exceeds the Bell-1964 classical bound 2. So every pure entangled two-qubit state is Bell-nonlocal (Gisin 1991).

The witness is trig-free and c,s-dependent (as it must be — the optimal Bob angle depends on the concurrence). With t = 2cs (the concurrence) and r = 1/√(1+t²):

• Alice: a = x̂ = (1,0,0), a' = ẑ = (0,0,1);
• Bob: b = (t·r, 0, r), b' = (−t·r, 0, r) — unit vectors in the x–z plane tilted toward x̂ by exactly the concurrence.

gisin_chsh_value computes the CHSH combination in closed form, psCHSH = 2√(1 + 4c²s²) (the Horodecki optimum for T = diag(2cs, −2cs, 1)), which exceeds 2 precisely because the concurrence 2cs > 0; the maximally-entangled c = s = 1/√2 recovers the Tsirelson value 2√2.

Grounding

psCorr is not a free real function: psExpectation_eq_psCorr identifies it with the genuine Hilbert-space expectation ⟨Ψ(c,s)|σ·a⊗σ·b|Ψ(c,s)⟩ (via psQubit_pauli_correlation), so psCHSH is the CHSH combination of physical two-qubit Pauli correlations, matching the singlet chshOperator convention E(a,b) − E(a,b') + E(a',b) + E(a',b') (Empirical/QM/Bell.lean).

References: LF6/PartialSchmidtCorrelation.lean (psQubit, psQubit_pauli_correlation — the correlation this violates); Empirical/QM/Bell.lean (chshOperator, chsh_singlet_tsirelson_bound — the maximally-entangled special case); specs/future-work.md (LF6-6); specs/BACKLOG.md.

noncomputable def CSD.LF6.detector3 (x y z : ℝ) (h_norm : x ^ 2 + y ^ 2 + z ^ 2 = 1) : LF3.DetectorSetting

Build a DetectorSetting from three real components with the unit-norm side condition (the local analogue of Empirical/QM/Bell.detector3, which is private).

Equations

• CSD.LF6.detector3 x y z h_norm = { vec := !₂[x, y, z], unit := ⋯ }

@[simp]

theorem CSD.LF6.detector3_vec (x y z : ℝ) (h_norm : x ^ 2 + y ^ 2 + z ^ 2 = 1) (i : Fin 3) : (detector3 x y z h_norm).vec.ofLp i = ![x, y, z] i

noncomputable def CSD.LF6.psCorr (c s : ℝ) (a b : LF3.DetectorSetting) : ℝ

The real partial-Schmidt correlation in closed form, E(a,b) = a_z b_z + 2cs·(a_x b_x − a_y b_y). Identified with the Hilbert-space expectation of σ·a ⊗ σ·b on Ψ(c,s) by psExpectation_eq_psCorr.

Equations

• CSD.LF6.psCorr c s a b = a.vec.ofLp 2 * b.vec.ofLp 2 + 2 * c * s * (a.vec.ofLp 0 * b.vec.ofLp 0 - a.vec.ofLp 1 * b.vec.ofLp 1)

theorem CSD.LF6.psExpectation_eq_psCorr (c s : ℝ) (hcs : c ^ 2 + s ^ 2 = 1) (a b : LF3.DetectorSetting) : psExpectation c s (LF3.sigmaDotJoint a b) = ↑(psCorr c s a b)

psCorr is the physical correlation. For a normalised Schmidt state the closed-form real psCorr equals the Hilbert-space Pauli expectation ⟨Ψ(c,s)|σ·a⊗σ·b|Ψ(c,s)⟩.

noncomputable def CSD.LF6.psCHSH (c s : ℝ) (a a' b b' : LF3.DetectorSetting) : ℝ

The CHSH combination of the partial-Schmidt correlation, S = E(a,b) − E(a,b') + E(a',b) + E(a',b') — the same sign convention as the singlet chshOperator.

Equations

• CSD.LF6.psCHSH c s a a' b b' = CSD.LF6.psCorr c s a b - CSD.LF6.psCorr c s a b' + CSD.LF6.psCorr c s a' b + CSD.LF6.psCorr c s a' b'

The Gisin witness settings

noncomputable def CSD.LF6.gisinA : LF3.DetectorSetting

Alice's first setting a = x̂ = (1,0,0).

Equations

• CSD.LF6.gisinA = CSD.LF6.detector3 1 0 0 CSD.LF6.gisinA._proof_1

noncomputable def CSD.LF6.gisinA' : LF3.DetectorSetting

Alice's second setting a' = ẑ = (0,0,1).

Equations

• CSD.LF6.gisinA' = CSD.LF6.detector3 0 0 1 CSD.LF6.gisinA'._proof_1

theorem CSD.LF6.gisin_r_sq (c s : ℝ) : (√(1 + (2 * c * s) ^ 2))⁻¹ ^ 2 = (1 + (2 * c * s) ^ 2)⁻¹

r = 1/√(1+t²) with t = 2cs, squared: r² = (1+(2cs)²)⁻¹.

theorem CSD.LF6.gisin_B_norm (c s : ℝ) : (2 * c * s * (√(1 + (2 * c * s) ^ 2))⁻¹) ^ 2 + 0 ^ 2 + (√(1 + (2 * c * s) ^ 2))⁻¹ ^ 2 = 1

The unit-norm condition for Bob's b = (t·r, 0, r): (t·r)² + 0² + r² = 1.

theorem CSD.LF6.gisin_B'_norm (c s : ℝ) : (-(2 * c * s * (√(1 + (2 * c * s) ^ 2))⁻¹)) ^ 2 + 0 ^ 2 + (√(1 + (2 * c * s) ^ 2))⁻¹ ^ 2 = 1

The unit-norm condition for Bob's b' = (−t·r, 0, r).

noncomputable def CSD.LF6.gisinB (c s : ℝ) : LF3.DetectorSetting

Bob's first setting b = (t·r, 0, r), t = 2cs, r = 1/√(1+t²) — a unit vector in the x–z plane tilted toward x̂ by the concurrence.

Equations

• CSD.LF6.gisinB c s = CSD.LF6.detector3 (2 * c * s * (√(1 + (2 * c * s) ^ 2))⁻¹) 0 (√(1 + (2 * c * s) ^ 2))⁻¹ ⋯

noncomputable def CSD.LF6.gisinB' (c s : ℝ) : LF3.DetectorSetting

Bob's second setting b' = (−t·r, 0, r) (the x-reflection of b).

Equations

• CSD.LF6.gisinB' c s = CSD.LF6.detector3 (-(2 * c * s * (√(1 + (2 * c * s) ^ 2))⁻¹)) 0 (√(1 + (2 * c * s) ^ 2))⁻¹ ⋯

theorem CSD.LF6.gisin_chsh_value (c s : ℝ) : psCHSH c s gisinA gisinA' (gisinB c s) (gisinB' c s) = 2 * √(1 + (2 * c * s) ^ 2)

The CHSH value on the Gisin witness is 2√(1 + (2cs)²) — the Horodecki optimum for the correlation matrix T = diag(2cs, −2cs, 1). At maximal entanglement 2cs = 1 this is 2√2, the Tsirelson bound.

theorem CSD.LF6.gisin_psCHSH_gt_two (c s : ℝ) (hc : 0 < c) (hs : 0 < s) : 2 < psCHSH c s gisinA gisinA' (gisinB c s) (gisinB' c s)

The Gisin witness beats the classical bound: 2 < psCHSH for the closed-form correlation, since psCHSH = 2√(1 + (2cs)²) and the concurrence 2cs > 0. (Pure statement about the settings; the physical reading is gisin_chsh_violation below.)

theorem CSD.LF6.gisin_chsh_violation (c s : ℝ) (hc : 0 < c) (hs : 0 < s) (hcs : c ^ 2 + s ^ 2 = 1) : ∃ (a : LF3.DetectorSetting) (a' : LF3.DetectorSetting) (b : LF3.DetectorSetting) (b' : LF3.DetectorSetting), 2 < (psExpectation c s (LF3.sigmaDotJoint a b)).re - (psExpectation c s (LF3.sigmaDotJoint a b')).re + (psExpectation c s (LF3.sigmaDotJoint a' b)).re + (psExpectation c s (LF3.sigmaDotJoint a' b')).re

Gisin's theorem (two-qubit, real-Schmidt form). Every pure entangled two-qubit state Ψ(c,s) = c|00⟩ + s|11⟩ (with 0 < c, 0 < s, c² + s² = 1) violates the CHSH inequality: there are detector settings a, a', b, b' for which the CHSH combination of the genuine Hilbert-space Pauli expectations ⟨Ψ(c,s)|σ·a⊗σ·b|Ψ(c,s)⟩ exceeds the Bell-1964 classical bound 2. The witness is gisinA/gisinA'/gisinB/gisinB', giving 2√(1 + (2cs)²) > 2 since the concurrence 2cs > 0; every pure entangled two-qubit state is thus Bell-nonlocal (Gisin 1991). The normalisation c² + s² = 1 is what identifies the closed-form psCorr with the physical expectation (psExpectation_eq_psCorr).