LF6-6: the partial-Schmidt (non-maximally-entangled) two-qubit correlation

Category: 6-Local (extends the LF6-D entangled tier beyond the maximally-entangled family).

LF6-D's non-factorisation runs on the maximally-entangled state Ψ_d (equal Schmidt coefficients), whose two-qubit sector is the Bell Φ⁺. This module takes the first step beyond maximal entanglement: the general real-Schmidt two-qubit state Ψ(c,s) = c|00⟩ + s|11⟩ (c² + s² = 1), and derives its Hilbert-space Pauli correlation in closed form:

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

The coefficient's magnitude 2|cs| is the concurrence (the entanglement measure; = 2cs in the canonical Schmidt form c, s ≥ 0): it is 1 at the maximally-entangled point c = s = 1/√2, where the correlation collapses to Φ⁺'s a_x b_x − a_y b_y + a_z b_z (psQubit_pauli_correlation_maximal), and 0 for a product state (c or s = 0). So this makes explicit where maximal entanglement enters the LF6-D correlation.

Honest scope

• Delivered (the correlation, general partial-Schmidt): the Hilbert-space Pauli correlation of an arbitrary real-Schmidt two-qubit state, psQubit_pauli_correlation, computed from the Hilbert space (psExpectation_formula + the pauliDot entries), with the maximal-entanglement reduction to Φ⁺ (psQubit_pauli_correlation_maximal). This extends the LF6 correlation content past equal Schmidt coefficients.
• The non-factorisation witness (now discharged in LF6/GisinTheorem.lean): forcing non-factorisation for unequal Schmidt coefficients (c ≠ s) needs a Bell violation for a non-maximally-entangled state. The LF6-D reflectXZ → singlet CHSH reduction is specific to Φ⁺ (equal weights) and the CGLMP Dirichlet-kernel closed form to the equal diagonal amplitudes (√d)⁻¹; neither ports. The general witness is Gisin's theorem — GisinTheorem.gisin_chsh_violation builds it directly on the psQubit_pauli_correlation computed here: from the state-dependence, the concurrence 2cs > 0 yields explicit detector settings with CHSH value 2√(1+(2cs)²) > 2.

Reference: specs/future-work.md (LF6-6); LF6/GisinTheorem.lean (gisin_chsh_violation, the witness).

noncomputable def CSD.LF6.psQubit (c s : ℝ) : EuclideanSpace ℂ (Fin 2 × Fin 2)

The partial-Schmidt two-qubit state Ψ(c,s) = c|00⟩ + s|11⟩ (real Schmidt coefficients) on EuclideanSpace ℂ (Fin 2 × Fin 2). Maximally entangled at c = s = 1/√2 (= Φ⁺), a product state at c = 0 or s = 0.

Equations

• CSD.LF6.psQubit c s = WithLp.toLp 2 fun (w : Fin 2 × Fin 2) => if w = (0, 0) then ↑c else if w = (1, 1) then ↑s else 0

theorem CSD.LF6.psQubit_apply (c s : ℝ) (w : Fin 2 × Fin 2) : (psQubit c s).ofLp w = if w = (0, 0) then ↑c else if w = (1, 1) then ↑s else 0

theorem CSD.LF6.psQubit_apply_00 (c s : ℝ) : (psQubit c s).ofLp (0, 0) = ↑c

theorem CSD.LF6.psQubit_apply_01 (c s : ℝ) : (psQubit c s).ofLp (0, 1) = 0

theorem CSD.LF6.psQubit_apply_10 (c s : ℝ) : (psQubit c s).ofLp (1, 0) = 0

theorem CSD.LF6.psQubit_apply_11 (c s : ℝ) : (psQubit c s).ofLp (1, 1) = ↑s

noncomputable def CSD.LF6.psExpectation (c s : ℝ) (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : ℂ

Expectation ⟨Ψ(c,s) | M | Ψ(c,s)⟩ for a (Fin 2 × Fin 2)-indexed matrix M.

Equations

• CSD.LF6.psExpectation c s M = inner ℂ (CSD.LF6.psQubit c s) ((Matrix.toEuclideanLin M) (CSD.LF6.psQubit c s))

theorem CSD.LF6.psExpectation_formula (c s : ℝ) (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : psExpectation c s M = ↑c ^ 2 * M (0, 0) (0, 0) + ↑c * ↑s * M (0, 0) (1, 1) + ↑s * ↑c * M (1, 1) (0, 0) + ↑s ^ 2 * M (1, 1) (1, 1)

The partial-Schmidt expectation formula. On Ψ(c,s) the expectation of an arbitrary (Fin 2 × Fin 2)-indexed matrix reduces to the four diagonal-support entries weighted by the Schmidt products c², cs, sc, s². The 12 of 16 double-sum terms vanish (each has a Ψ(0,1) = 0 or Ψ(1,0) = 0 factor); the c, s are real, so star acts trivially. Mirrors phiPlus_expectation_formula with the two unequal amplitudes c, s.

theorem CSD.LF6.psExpectation_sigmaDotJoint (c s : ℝ) (a b : LF3.DetectorSetting) : psExpectation c s (LF3.sigmaDotJoint a b) = ↑(c ^ 2 + s ^ 2) * (↑(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))

The raw (pre-normalisation) partial-Schmidt Pauli correlation: ⟨Ψ(c,s)|σ·a ⊗ σ·b|Ψ(c,s)⟩ = (c²+s²)·a_z b_z + 2cs·(a_x b_x − a_y b_y).

theorem CSD.LF6.psQubit_pauli_correlation (c s : ℝ) (hcs : c ^ 2 + s ^ 2 = 1) (a b : LF3.DetectorSetting) : psExpectation c s (LF3.sigmaDotJoint 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))

The partial-Schmidt two-qubit Pauli correlation (the genuine Hilbert-space computation, generalising phiPlus_pauli_correlation beyond maximal entanglement). For c² + s² = 1:

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

The coefficient's magnitude 2|cs| is the concurrence (= 2cs in the canonical Schmidt form c, s ≥ 0): 1 at maximal entanglement (c = s = 1/√2), 0 at a product state. This makes explicit where the Schmidt spectrum enters the LF6-D Φ⁺ correlation.

theorem CSD.LF6.psQubit_pauli_correlation_maximal (a b : LF3.DetectorSetting) : psExpectation (√2)⁻¹ (√2)⁻¹ (LF3.sigmaDotJoint a b) = ↑(a.vec.ofLp 0 * b.vec.ofLp 0 - a.vec.ofLp 1 * b.vec.ofLp 1 + a.vec.ofLp 2 * b.vec.ofLp 2)

Maximal-entanglement reduction: Ψ(1/√2, 1/√2) = Φ⁺. At the maximally-entangled point the partial-Schmidt correlation collapses to Φ⁺'s a_x b_x − a_y b_y + a_z b_z (concurrence 2cs = 1), recovering phiPlus_pauli_correlation. So Φ⁺ is the equal-Schmidt-coefficient special case.