Empirical: Malus's law (spin-1/2 Born probability)

Category: 3-Local. QM-validity layer (pure inner-product geometry, no CSD ontology). The QM-side companion to Empirical/CSD/MalusVolume.lean: the same cos²(θ/2) value, here as a textbook Born identity rather than a derived Fubini-Study volume.

What this file proves

For a spin-1/2 prepared in the +-eigenstate of spin along the polar angle θ, ψ_θ = cos(θ/2)|0⟩ + sin(θ/2)|1⟩, and measured along +z:

P(+_z | θ) = |⟨0|ψ_θ⟩|² = cos²(θ/2)        (Malus's law)
P(−_z | θ) = |⟨1|ψ_θ⟩|² = sin²(θ/2)

plus the basis-completeness identity cos²(θ/2) + sin²(θ/2) = 1.

Malus's law subsumes the two Stern-Gerlach values:

• θ = 0 ⟹ cos²(0) = 1 (P(+_z | +_z) = 1, born_zPlus_zPlus);
• θ = π/2 ⟹ cos²(π/4) = 1/2 (the canonical 50/50 split, born_xPlus_zPlus).

The angular law cos²(θ/2) is the spin-1/2 analogue of the classical optical Malus law I = I₀ cos²θ (Malus 1809); the half-angle reflects the spin-1/2 double cover. It reuses the Stern-Gerlach bornProb (the doubly-normalised |⟨state|prep⟩|²), so the result is invariant under (un)normalisation.

Source

• Malus 1809 (optical, classical analogue).
• The spin-1/2 cos²(θ/2) form: standard QM (Sakurai, Modern QM; the rotated-spin projection probability).

The θ-rotated spin state

noncomputable def CSD.Empirical.Malus.malus (θ : ℝ) : Fin 2 → ℂ

The spin-θ +-eigenstate ψ_θ = cos(θ/2)|0⟩ + sin(θ/2)|1⟩ (in the unnormalised Fin 2 → ℂ convention; it is in fact a unit vector).

Equations

• CSD.Empirical.Malus.malus θ = ![↑(Real.cos (θ / 2)), ↑(Real.sin (θ / 2))]

@[simp]

theorem CSD.Empirical.Malus.normSq_malus (θ : ℝ) : SternGerlach.normSq (malus θ) = 1

Malus's law

theorem CSD.Empirical.Malus.malus_law (θ : ℝ) : SternGerlach.bornProb SternGerlach.zPlus (malus θ) = Real.cos (θ / 2) ^ 2

Malus's law P(+_z | θ) = cos²(θ/2). The Born probability that a spin prepared at polar angle θ is measured + along z.

theorem CSD.Empirical.Malus.malus_law_complement (θ : ℝ) : SternGerlach.bornProb SternGerlach.zMinus (malus θ) = Real.sin (θ / 2) ^ 2

Complementary outcome P(−_z | θ) = sin²(θ/2).

theorem CSD.Empirical.Malus.malus_basis_complete (θ : ℝ) : SternGerlach.bornProb SternGerlach.zPlus (malus θ) + SternGerlach.bornProb SternGerlach.zMinus (malus θ) = 1

Basis completeness: the two z-outcome probabilities sum to 1.

Recovery of the Stern-Gerlach values

theorem CSD.Empirical.Malus.malus_zero : SternGerlach.bornProb SternGerlach.zPlus (malus 0) = 1

θ = 0 recovers P(+_z | +_z) = 1: at zero angle the prep is |0⟩.

theorem CSD.Empirical.Malus.malus_pi_div_two : SternGerlach.bornProb SternGerlach.zPlus (malus (Real.pi / 2)) = 1 / 2

θ = π/2 recovers the canonical 50/50 split P = 1/2.