Move continuously between the two states
On this page · Permalink · Source line 182
Changing only relative phase moves the selected probability from zero to one. Let \(v_+\) contain the positive entries of \(c_{12}/\sqrt{48}\) and \(v_-\) contain the absolute values of its negative entries. Their supports are disjoint and each has squared norm \(1/2\). Define
\[
\chi_\theta=v_++e^{i\theta}v_-,\qquad
\chi_0=\chi,\quad\chi_\pi=\psi.
\]
Indeed, \(\chi_\theta=\tfrac{1+e^{i\theta}}2\chi+\tfrac{1-e^{i\theta}}2\psi\). Since \(P\chi=0\) and \(P\psi=\psi\), we get \(\|P\chi_\theta\|^2=|1-e^{i\theta}|^2/4=\sin^2(\theta/2)\). The endpoint statements are covered by the inherited Lean development. This continuous family is an elementary prose derivation and a checked illustration, not an additional inherited Lean theorem.