norm_phaseRotate
plain-language theorem explainer
Pointwise phase rotation of an 8-mode complex signal leaves each mode's modulus unchanged: multiplying ψ_k by e^{i θ_k} does not alter ‖ψ_k‖. Anyone proving phase invariance of the DFT-8 sector measure or preservation of normalisation under phase gates cites this. The proof is a one-line simp using the definition of phaseRotate and |e^{iθ}| = 1.
Claim. For every 8-mode complex signal $\psi$, every real phase assignment $\theta : \{0,\ldots,7\} \to \mathbb{R}$, and every mode index $k$, $\|e^{i\theta_k}\psi_k\| = \|\psi_k\|$.
background
The module forces the Born rule on DFT-8 sectors: the unique probability measure that is normalised, phase-invariant, additive on disjoint mode sets, and calibrated to the two-branch exp(−C) rule is $\mu(S)=\sum_{k\in S}|\psi_k|^2$. The setting rests on ComplexStructureForcing (Signal8, inner product, DFT-8, Parseval) and the two-outcome Born certificate.
A Signal8 is an 8-component complex amplitude vector indexed by Fin 8 (the eight-tick octave from T7). Pointwise phase rotation multiplies mode $k$ by $e^{i\theta_k}$; the definition is phaseRotate ψ θ := fun k => ψ k * exp(i·θ_k). Sector measure sums squared moduli over a Finset of modes, so any claim that the measure ignores arguments needs modulus preservation mode by mode.
Upstream, Phase is the 8-tick phase space Fin 8. The complex-norm identity |exp(iθ)| = 1 for real θ is the analytic engine behind the equality.
proof idea
Term-mode one-liner. Unfold phaseRotate to expose the factor Complex.exp (↑(θ k) * I), then apply Complex.norm_exp_ofReal_mul_I, which states that the complex modulus of $e^{i\theta}$ is 1 for real $\theta$. Multiplicativity of the norm then cancels the phase factor and leaves $|\psi k|$. No induction or case split; pure simp on the definition plus that standard complex lemma.
why it matters
This is the atomic modulus-preservation fact that makes phase invariance of the Born sector measure go through. Downstream, sectorMeasure_phase_invariant rewrites the sum of squared norms after phase rotation by calling this lemma at each index, and isNormalized_phaseRotate uses it to show that total mass $\sum_k |\psi_k|^2$ is unchanged under phase gates.
In the Recognition forcing chain the result sits under T7 (eight-tick octave) and the complex-structure forcing that supplies Signal8. It closes part of the Born-rule gap flagged in the module registry: without modulus invariance, the unique-measure theorem could not drop arguments and recover $\mu(S)=\sum|\psi_k|^2$. It is local bookkeeping, but every later uniqueness or calibration step that quotes phase invariance depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.