The Born rule \(P(\psi ) = |\langle \phi |\psi \rangle |^2\) arises as the unique probability measure on \(L^2(K^1)\) induced by Haar measure and Gleason’s theorem.

Proved clean: Haar measure gives a probability measure on \(K^1\); \(\| f\| ^2 = \int |f|^2 d\mu \) normalizes to \(1\). Axioms: K1_haar_probability, born_from_haar, gleason_uniqueness (Gleason 1957, not in Mathlib).