1.14 A continuous phase family with a fixed initial histogram
On this page · Permalink · Source line 1300
The two endpoint states are especially simple, but the mechanism is continuous. Define the nonnegative vectors \(v_+\) and \(v_-\) by placing \(|c(n)|/\sqrt{48}\) respectively on the positive and negative entries of \(c\), with zero elsewhere. Thus
Their supports are disjoint, and each has squared norm \(1/2\). For real \(\theta\), define
It is a normalized state with the same original-basis probabilities for every \(\theta\). The endpoints are \(\chi_0=\chi\) and \(\chi_\pi=\psi\).
Theorem QA19: Relative-phase response
For this family,
Proof
Disjoint support gives \(\|\chi_\theta\|^2=\|v_+\|^2+\|v_-\|^2=1\) and unchanged entrywise squared magnitudes. Solving for \(v_+\) and \(v_-\) in terms of \(\chi\) and \(\psi\) gives
Since \(P\chi=0\) and \(P\psi=\psi\),
Its squared norm is
Finally, \(P=FDF^\dagger\) and unitarity imply \(\|P\chi_\theta\|^2=\|DF^\dagger\chi_\theta\|^2\), exactly the sum of the selected Fourier-basis probabilities. \(\square\)
This is a proved prose extension for the visual guide. It is not presented as an inherited Lean theorem. It shows that a probability histogram can stay fixed while an interference-based observation varies from zero to one.