LF3 Singlet / JointEig: genuine joint spin eigenstates of the singlet (LF4 §3)

Category: 3-Local (LF4 §3 discharge — genuine joint spin eigenvectors).

Constructs the actual joint spin eigenstate at sector (s, t) as the normalised projection of the singlet onto that sector, singletJointEig s t := (√P_st)⁻¹ • (Πˢ(a)⊗Πᵗ(b)) ψ⁻, and proves the facts a MeasurementJointEig bundle needs as theorems rather than carried hypotheses:

• singletJointEig_norm — unit norm (uses jointSpinProj Hermitian + idempotent + the Born expectation identity);
• singletJointEig_born — ‖⟨ψ⁻, singletJointEig s t⟩‖² = P_st a b s t (the LF4-todo §3 target);
• singletJointEig_orthogonal — distinct sectors give orthogonal eigenstates.

All over EuclideanSpace ℂ (Fin 2 × Fin 2); the LF4 bundle re-indexes to Fin N via a LinearIsometryEquiv (inner products / norms transport).

Generic-context restriction. The (√P_st)⁻¹ normalisation requires P_st a b s t ≠ 0, i.e. s·t·(a·b) ≠ 1. For a generic context (|a·b| < 1 — the generic non-collinear contexts, which include the four canonical CHSH-optimal pairs, but NOT the collinear ones) every sector has P_st > 0, so the construction covers all four sectors.

⚠️ Corrected 2026-08-11. The previous wording said collinear settings have "one vanishing sector" and "no Born information"; both halves were wrong. At a·b = ±1 two of the four sectors have probability zero and the other two carry 1/2 each — perfect (anti)correlation, which is among the most informative Bell data, not an absence of Born content. They are excluded here only because the legacy singletJointEig normalisation divides by √P_st and so needs all four P_st > 0. LF6.localNudgeVec has no such division and covers them (localDeisolation_pointer_volume_local).

noncomputable def CSD.LF3.singletJointEig (s t : Sign) (a b : DetectorSetting) : EuclideanSpace ℂ (Fin 2 × Fin 2)

The genuine joint spin eigenstate at sector (s, t): the normalised projection of the singlet onto the range of Πˢ(a)⊗Πᵗ(b).

Equations

• CSD.LF3.singletJointEig s t a b = (↑√(CSD.LF3.P_st a b s t))⁻¹ • (Matrix.toEuclideanLin (CSD.LF3.jointSpinProj s t a b)) CSD.LF3.singlet

theorem CSD.LF3.toEuclideanLin_mul_apply (M N : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (v : EuclideanSpace ℂ (Fin 2 × Fin 2)) : (Matrix.toEuclideanLin (M * N)) v = (Matrix.toEuclideanLin M) ((Matrix.toEuclideanLin N) v)

toEuclideanLin turns matrix multiplication into composition.

theorem CSD.LF3.toEuclideanLin_jointSpinProj_idem (s t : Sign) (a b : DetectorSetting) (v : EuclideanSpace ℂ (Fin 2 × Fin 2)) : (Matrix.toEuclideanLin (jointSpinProj s t a b)) ((Matrix.toEuclideanLin (jointSpinProj s t a b)) v) = (Matrix.toEuclideanLin (jointSpinProj s t a b)) v

The joint projector acts idempotently on vectors.

theorem CSD.LF3.toEuclideanLin_jointSpinProj_isSymmetric (s t : Sign) (a b : DetectorSetting) : (Matrix.toEuclideanLin (jointSpinProj s t a b)).IsSymmetric

T_P is symmetric (self-adjoint), from jointSpinProj Hermitian.

theorem CSD.LF3.norm_sq_jointSpinProj_singlet (s t : Sign) (a b : DetectorSetting) : ‖(Matrix.toEuclideanLin (jointSpinProj s t a b)) singlet‖ ^ 2 = P_st a b s t

The squared norm of the singlet's projection onto the sector is P_st.

theorem CSD.LF3.singletJointEig_norm (s t : Sign) (a b : DetectorSetting) (hP : 0 < P_st a b s t) : ‖singletJointEig s t a b‖ = 1

Unit norm of the joint spin eigenstate (generic context).

theorem CSD.LF3.singletJointEig_born (s t : Sign) (a b : DetectorSetting) (hP : 0 < P_st a b s t) : ‖inner ℂ singlet (singletJointEig s t a b)‖ ^ 2 = P_st a b s t

The Born identity for the genuine joint spin eigenstate (LF4-todo §3): ‖⟨ψ⁻, singletJointEig s t⟩‖² = P_st a b s t.

theorem CSD.LF3.singletJointEig_orthogonal {s t s' t' : Sign} (a b : DetectorSetting) (h : (s, t) ≠ (s', t')) : inner ℂ (singletJointEig s t a b) (singletJointEig s' t' a b) = 0

Distinct sectors give orthogonal joint spin eigenstates.