LF3/Spinor: the detector-axis spinors

Category: 3-Local (the local eigenbasis of σ·a).

Why this exists

SingletDeisolationFlow.nudgedSinglet was documented as the singlet "transformed by local basis rotations". That description is false, and the repository's own proof shows why: inside singletJointEig_born,

inner ℂ singlet (singletJointEig s t a b) = (Real.sqrt (P_st a b s t) : ℂ)

so nudgedSinglet a b is the vector (√P_st)_{s,t} — all real, all non-negative, every phase stripped. Local unitaries preserve Schmidt spectra and ψ⁻ is maximally entangled, so a local-unitary image of ψ⁻ is maximally entangled; but at a ⊥ b all four P_st = ¼, making nudgedSinglet = ½(1,1,1,1) a product state. No local unitary does that.

The defect is in singletJointEig := (√P_st)⁻¹ • (Πˢ(a) ⊗ Πᵗ(b)) ψ⁻, which fixes each basis vector's phase by projecting ψ⁻ itself: four independent phases, where a product unitary supplies only separable ones (αₛ + βₜ).

This module builds the local eigenbasis that a genuine nudge-locality statement needs. It sits in LF3 because every object here (DetectorSetting, spinProj, pauliDot) is LF3's; the nudge theorem that consumes it belongs in LF6. Nothing here depends on the old definition, and nothing here is claimed of it.

Contents

• spinor s a — the unit s-eigenvector of σ·a, defined by an explicit formula with a single case split at the pole 1 + s·a_z = 0 (where the eigenvector collapses to a basis vector).
• spinor_normSq — the spinor is a unit vector.
• ★★ spinProj_eq_outer — the projector is its outer product. This is what carries the Born identity downstream: it gives Πˢ(a) ⊗ Πᵗ(b) = (u ⊗ w)(u ⊗ w)ᴴ, hence ⟨ψ⁻, (Πˢ ⊗ Πᵗ) ψ⁻⟩ = |⟨u ⊗ w, ψ⁻⟩|².

References

LF3/Setup.lean (spinProj, pauliDot, DetectorSetting); LF6/SingletDeisolationFlow.lean (the object this replaces); specs/c1-correction-plan.md §3b.

Preliminaries

theorem CSD.LF3.sign_sq (s : Sign) : s.val ^ 2 = 1

theorem CSD.LF3.sign_ne_zero (s : Sign) : s.val ≠ 0

theorem CSD.LF3.abs_vec_two_le_one (a : DetectorSetting) : |a.vec.ofLp 2| ≤ 1

The z-component is bounded by one, from ‖a‖ = 1.

theorem CSD.LF3.transverse_eq_zero_of_pole (s : Sign) (a : DetectorSetting) (h : 1 + s.val * a.vec.ofLp 2 = 0) : a.vec.ofLp 0 = 0 ∧ a.vec.ofLp 1 = 0

At the pole the transverse components vanish.

The detector-axis spinor

noncomputable def CSD.LF3.spinorRaw (s : Sign) (a : DetectorSetting) : Fin 2 → ℂ

The unnormalised s-eigenvector of σ·a: the first column of Πˢ(a) scaled by 2. Its squared norm is 2(1 + s·a_z), so it is nonzero exactly away from the pole.

Equations

• CSD.LF3.spinorRaw s a = ![↑(1 + s.val * a.vec.ofLp 2), ↑s.val * (↑(a.vec.ofLp 0) + Complex.I * ↑(a.vec.ofLp 1))]

@[simp]

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

@[simp]

theorem CSD.LF3.spinorRaw_one (s : Sign) (a : DetectorSetting) : spinorRaw s a 1 = ↑s.val * (↑(a.vec.ofLp 0) + Complex.I * ↑(a.vec.ofLp 1))

@[simp]

theorem CSD.LF3.star_spinorRaw_zero (s : Sign) (a : DetectorSetting) : star (spinorRaw s a 0) = ↑(1 + s.val * a.vec.ofLp 2)

@[simp]

theorem CSD.LF3.star_spinorRaw_one (s : Sign) (a : DetectorSetting) : star (spinorRaw s a 1) = ↑s.val * (↑(a.vec.ofLp 0) - Complex.I * ↑(a.vec.ofLp 1))

theorem CSD.LF3.sum_sq_components_eq_one_C (a : DetectorSetting) : ↑(a.vec.ofLp 0) ^ 2 + ↑(a.vec.ofLp 1) ^ 2 + ↑(a.vec.ofLp 2) ^ 2 = 1

The unit-vector relation, as a complex identity.

theorem CSD.LF3.sign_sq_C (s : Sign) : ↑s.val ^ 2 = 1

theorem CSD.LF3.two_mul_spinProj_eq_raw_outer (s : Sign) (a : DetectorSetting) (i j : Fin 2) : ↑(2 * (1 + s.val * a.vec.ofLp 2)) * spinProj s a i j = spinorRaw s a i * star (spinorRaw s a j)

★ The division-free outer-product identity. 2(1 + s·a_z) · Πˢ(a)ᵢⱼ = rawᵢ · conj(rawⱼ). Away from the pole, dividing by the positive scalar gives Πˢ(a) = u uᴴ.

theorem CSD.LF3.spinorRaw_normSq (s : Sign) (a : DetectorSetting) : ‖spinorRaw s a 0‖ ^ 2 + ‖spinorRaw s a 1‖ ^ 2 = 2 * (1 + s.val * a.vec.ofLp 2)

The unnormalised spinor's squared norm.

noncomputable def CSD.LF3.spinor (s : Sign) (a : DetectorSetting) : Fin 2 → ℂ

The unit s-eigenvector of σ·a. Away from the pole it is spinorRaw normalised; at the pole (1 + s·a_z = 0, forcing a = -s·ẑ) that vector vanishes and Πˢ(a) = diag(0,1), so the eigenvector is e₁.

Equations

• CSD.LF3.spinor s a = if 0 < 1 + s.val * a.vec.ofLp 2 then (↑√(2 * (1 + s.val * a.vec.ofLp 2)))⁻¹ • CSD.LF3.spinorRaw s a else ![0, 1]

theorem CSD.LF3.pole_facts (s : Sign) (a : DetectorSetting) (hpos : ¬0 < 1 + s.val * a.vec.ofLp 2) : a.vec.ofLp 0 = 0 ∧ a.vec.ofLp 1 = 0 ∧ s.val * a.vec.ofLp 2 = -1

At the pole, the transverse components vanish and s·a_z = -1.

The spinor is a unit vector, and the projector is its outer product

theorem CSD.LF3.spinor_normSq (s : Sign) (a : DetectorSetting) : ‖spinor s a 0‖ ^ 2 + ‖spinor s a 1‖ ^ 2 = 1

The spinor has unit norm, in both branches.

theorem CSD.LF3.spinProj_eq_outer (s : Sign) (a : DetectorSetting) (i j : Fin 2) : spinProj s a i j = spinor s a i * star (spinor s a j)

★★ The projector is the spinor's outer product: Πˢ(a) = u uᴴ.

This is the lemma that carries the Born identity downstream: it gives Πˢ(a) ⊗ Πᵗ(b) = (u ⊗ w)(u ⊗ w)ᴴ, hence ⟨ψ⁻, (Πˢ ⊗ Πᵗ) ψ⁻⟩ = |⟨u ⊗ w, ψ⁻⟩|².

The wing basis unitary

The two spinors are the columns of a unitary. Completeness of the spin projectors gives U Uᴴ = 1 in one step, with no orthogonality argument: (U Uᴴ)ᵢⱼ = Σₛ (u_s)ᵢ conj((u_s)ⱼ) = Σₛ Πˢ(a)ᵢⱼ = δᵢⱼ.

def CSD.LF3.signOfFin : Fin 2 → Sign

The two signs, indexed by Fin 2.

Equations

• CSD.LF3.signOfFin = ![CSD.LF3.Sign.plus, CSD.LF3.Sign.minus]

@[simp]

theorem CSD.LF3.signOfFin_zero : signOfFin 0 = Sign.plus

@[simp]

theorem CSD.LF3.signOfFin_one : signOfFin 1 = Sign.minus

theorem CSD.LF3.spinProj_add_eq_one (a : DetectorSetting) : spinProj Sign.plus a + spinProj Sign.minus a = 1

Completeness of the spin projectors: Π⁺(a) + Π⁻(a) = 1.

theorem CSD.LF3.sum_spinProj (a : DetectorSetting) (i j : Fin 2) : ∑ k : Fin 2, spinProj (signOfFin k) a i j = 1 i j

Summing the projectors over both signs.

noncomputable def CSD.LF3.wingBasisUnitary (a : DetectorSetting) : Matrix (Fin 2) (Fin 2) ℂ

The wing basis unitary. Columns are the two detector-axis spinors, so conjugating by it is the change of basis into the σ·a eigenbasis.

Equations

• CSD.LF3.wingBasisUnitary a = Matrix.of fun (i k : Fin 2) => CSD.LF3.spinor (CSD.LF3.signOfFin k) a i

theorem CSD.LF3.wingBasisUnitary_mem_unitaryGroup (a : DetectorSetting) : wingBasisUnitary a ∈ Matrix.unitaryGroup (Fin 2) ℂ

★★ The wing basis matrix is unitary.

noncomputable def CSD.LF3.wingBasisU (a : DetectorSetting) : ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The wing basis unitary, as an element of the unitary group.

Equations

• CSD.LF3.wingBasisU a = ⟨CSD.LF3.wingBasisUnitary a, ⋯⟩

@[simp]

theorem CSD.LF3.wingBasisU_val (a : DetectorSetting) : ↑(wingBasisU a) = wingBasisUnitary a

The two-qubit product spinor

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

The product spinor u_s(a) ⊗ w_t(b) on the two-qubit space.

Equations

• CSD.LF3.spinorPair s t a b p = CSD.LF3.spinor s a p.1 * CSD.LF3.spinor t b p.2

theorem CSD.LF3.jointSpinProj_eq_outer (s t : Sign) (a b : DetectorSetting) (I J : Fin 2 × Fin 2) : jointSpinProj s t a b I J = spinorPair s t a b I * star (spinorPair s t a b J)

★★ The joint projector is the outer product of the product spinor: Πˢ(a) ⊗ Πᵗ(b) = (u ⊗ w)(u ⊗ w)ᴴ.