LF3 Singlet / JointProjector: joint spin projector algebra + the Born expectation identity

Category: 3-Local (LF4 §3 discharge groundwork — the reusable physics behind MeasurementJointEig.born_eq_P_st).

This module supplies the matrix-level facts about the joint two-qubit spin projector jointSpinProj s t a b = Πˢ(a) ⊗ Πᵗ(b) that LF4 needs to construct genuine joint spin eigenstates (rather than the closed-form cAmp = √P_st placeholder of Kernel.lean):

• jointSpinProj_isHermitian — Hermitian (Kronecker of Hermitian projectors).
• jointSpinProj_idem — idempotent (mixed-product property + spinProj_idem).
• spinProj_mul_orthogonal / jointSpinProj_mul_orthogonal — distinct sectors multiply to zero (mutual orthogonality of the four joint projectors).
• singlet_jointSpinProj_expectation — the Born identity at the projector level: ⟨ψ⁻ | Πˢ(a)⊗Πᵗ(b) | ψ⁻⟩ = P_st a b s t = (1 − st·a·b)/4. Proved by the same entry-evaluation technique as singlet_pauli_correlation.

The LF4 eigenstate eig s t := (√P_st)⁻¹ • (jointSpinProj s t · ψ⁻) is the normalised projection of the singlet onto the sector; combined with the expectation identity and Hermitian-idempotence it yields ‖⟨ψ⁻, eig s t⟩‖² = P_st and ‖eig s t‖ = 1. That construction (and the Fin 2 × Fin 2 → Fin N re-indexing) lives in the LF4 layer; this module is the context-independent physics it consumes.

Joint spin projector as a Kronecker product

theorem CSD.LF3.jointSpinProj_eq_kronecker (s t : Sign) (a b : DetectorSetting) : jointSpinProj s t a b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (spinProj s a) (spinProj t b)

jointSpinProj is the Kronecker product of the two one-qubit spin projectors. (Definitional; restated for ⊗ₖ-rewriting.)

theorem CSD.LF3.jointSpinProj_isHermitian (s t : Sign) (a b : DetectorSetting) : (jointSpinProj s t a b).IsHermitian

The joint spin projector is Hermitian.

theorem CSD.LF3.jointSpinProj_idem (s t : Sign) (a b : DetectorSetting) : jointSpinProj s t a b * jointSpinProj s t a b = jointSpinProj s t a b

The joint spin projector is idempotent: (Πˢ⊗Πᵗ)² = Πˢ⊗Πᵗ.

theorem CSD.LF3.spinProj_mul_orthogonal {s s' : Sign} (a : DetectorSetting) (h : s ≠ s') : spinProj s a * spinProj s' a = 0

One-qubit spin projectors at distinct signs are mutually orthogonal: Πˢ(a) · Πˢ'(a) = 0 when s ≠ s'. Expand (1/4)(1 + sσ)(1 + s'σ) = (1/4)(1 + (s+s')σ + ss'·σ²); for s ≠ s', s + s' = 0 and ss' = -1, so it collapses to (1/4)(1 - 1) = 0.

theorem CSD.LF3.jointSpinProj_mul_orthogonal {s t s' t' : Sign} (a b : DetectorSetting) (h : (s, t) ≠ (s', t')) : jointSpinProj s t a b * jointSpinProj s' t' a b = 0

The four joint spin projectors are mutually orthogonal: for distinct sectors (s, t) ≠ (s', t'), (Πˢ(a)⊗Πᵗ(b))·(Πˢ'(a)⊗Πᵗ'(b)) = 0.

One-qubit spin projector entries

theorem CSD.LF3.spinProj_apply_00 (s : Sign) (a : DetectorSetting) : spinProj s a 0 0 = 1 / 2 * (1 + ↑s.val * ↑(a.vec.ofLp 2))

Πˢ(a) 0 0 = (1 + s·a_z)/2.

theorem CSD.LF3.spinProj_apply_01 (s : Sign) (a : DetectorSetting) : spinProj s a 0 1 = 1 / 2 * (↑s.val * (↑(a.vec.ofLp 0) - Complex.I * ↑(a.vec.ofLp 1)))

Πˢ(a) 0 1 = s·(a_x − i a_y)/2.

theorem CSD.LF3.spinProj_apply_10 (s : Sign) (a : DetectorSetting) : spinProj s a 1 0 = 1 / 2 * (↑s.val * (↑(a.vec.ofLp 0) + Complex.I * ↑(a.vec.ofLp 1)))

Πˢ(a) 1 0 = s·(a_x + i a_y)/2.

theorem CSD.LF3.spinProj_apply_11 (s : Sign) (a : DetectorSetting) : spinProj s a 1 1 = 1 / 2 * (1 - ↑s.val * ↑(a.vec.ofLp 2))

Πˢ(a) 1 1 = (1 − s·a_z)/2.

The Born expectation identity

theorem CSD.LF3.singlet_jointSpinProj_expectation (s t : Sign) (a b : DetectorSetting) : expectation (jointSpinProj s t a b) = ↑(P_st a b s t)

Born identity at the projector level. ⟨ψ⁻ | Πˢ(a) ⊗ Πᵗ(b) | ψ⁻⟩ = P_st a b s t = (1 − st·a·b)/4.

This is the genuine spin computation underlying MeasurementJointEig's born_eq_P_st field: it expresses the singlet expectation of the joint spin projector as the closed-form kernel P_st. Proved by reducing the expectation to the four-entry half-sum (expectation_formula), evaluating the joint-projector entries as products of one-qubit-projector entries (Matrix.kroneckerMap_apply + spinProj_apply_*), and simplifying with Complex.I_sq exactly as in singlet_pauli_correlation.