LF3 Singlet / Expectations: the headline 4×4 Pauli expectation calculation #
Category: 3-Local (LF3 left/right zero expectations and singlet_pauli_correlation = −a·b).
Paper §6.
Three theorems on the Bell singlet:
singlet_left_pauli_expectation_zero : ⟨ψ⁻ | σ·a ⊗ I | ψ⁻⟩ = 0singlet_right_pauli_expectation_zero : ⟨ψ⁻ | I ⊗ σ·b | ψ⁻⟩ = 0singlet_pauli_correlation : ⟨ψ⁻ | σ·a ⊗ σ·b | ψ⁻⟩ = -a·b
Strategy: a single helper lemma expectation_formula reduces the expectation
on any (Fin 2 × Fin 2)-indexed matrix to a (1/2) · (sum of 4 entries)
form. The three theorems then evaluate the entries of sigmaDotLeft / Right / Joint.
The proof of expectation_formula is a 4×4 inner-product unfolding: reduce
to a dot product via EuclideanSpace.inner_eq_star_dotProduct, expand both
sums over Fin 2 × Fin 2, push star past pointwise application with
Pi.star_apply, substitute the four singlet_apply_* values (12 of 16
terms vanish from factors of zero), and close with ring_nf + the
((√2)⁻¹)² = 1/2 helper.
Expectation formula. On the Bell singlet, the expectation of an
arbitrary (Fin 2 × Fin 2)-indexed matrix reduces to a half-sum over four
specific matrix entries. The 12 of 16 double-sum terms vanish (each has a
singlet (0,0) = 0 or singlet (1,1) = 0 factor); the surviving 4 factor
through ((√2)⁻¹)² = 1/2.
Pauli matrix entries (auxiliaries) #
pauliDot a 0 0 = a_z (as a complex number).
pauliDot a 1 1 = −a_z.
The three headline expectations (paper §6.7, §6.8) #
Singlet left-Pauli expectation vanishes. ⟨ψ⁻ | σ·a ⊗ I | ψ⁻⟩ = 0.
Singlet right-Pauli expectation vanishes. ⟨ψ⁻ | I ⊗ σ·b | ψ⁻⟩ = 0.