isNormalized_phaseRotate
plain-language theorem explainer
Phase rotation of a unit-norm 8-mode signal stays unit-norm. Anyone proving phase invariance of the DFT-8 sector measure (Born-rule forcing) cites this. The proof reduces normalisation to the pointwise identity that multiplying by e^{iθ_k} does not change modulus.
Claim. Let $\psi$ be an 8-mode complex signal with $\sum_{k}\|\psi_k\|^2=1$, and let $\theta:\mathrm{Fin}\,8\to\mathbb{R}$ assign a real phase to each mode. Then the pointwise rotated signal $k\mapsto\psi_k\,e^{i\theta_k}$ also satisfies $\sum_{k}\|\psi_k e^{i\theta_k}\|^2=1$.
background
The module forces the Born rule on the eight-tick register: the unique probability on mode-sets that is normalised, phase-invariant, additive on disjoint sectors, and calibrated to the two-branch exp(−C) rule is $\mu(S)=\sum_{k\in S}|\psi_k|^2$ (equivalently the DFT-8 Parseval form).
A signal $\psi:\mathrm{Fin},8\to\mathbb{C}$ is normalised when $\sum_k|\psi_k|^2=1$. Pointwise phase rotation multiplies mode $k$ by $e^{i\theta_k}$. The sibling lemma norm_phaseRotate records that this leaves each modulus unchanged, which is the only analytic input needed here. The setting sits on ComplexStructureForcing (Signal8, inner product, DFT-8) and the two-outcome Born certificate.
proof idea
Unfold the target normalisation as $\sum_k|\mathrm{phaseRotate},\psi,\theta,k|^2=1$. Simplify with the pointwise identity $|\mathrm{phaseRotate},\psi,\theta,k|=|\psi_k|$, so the sum collapses to the original normalisation hypothesis. No further algebra.
why it matters
This is the normalisation half of phase invariance for the sector measure that the module identifies with Born probability. The next sibling, sector-measure phase invariance, needs exactly that rotated states remain normalised so the measure stays a probability. The module doc places the whole development as closing the Born-rule gap (replacing trivial placeholders), depending on T5 (J-uniqueness), T7 (eight-tick octave), T8 ($D=3$), and the measurement mechanism F-009. No downstream edges are recorded yet; the lemma is local scaffolding for the uniqueness theorem stated in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.