phaseRotate
plain-language theorem explainer
Pointwise phase rotation on an 8-mode complex signal: each mode k is multiplied by e^{i θ_k}. Anyone proving phase invariance of the DFT-8 sector measure (Born-rule forcing) cites this map. The body is a one-line pointwise definition via Complex.exp.
Claim. For an 8-mode signal $\psi:\mathrm{Fin}\,8\to\mathbb{C}$ and a real phase assignment $\theta:\mathrm{Fin}\,8\to\mathbb{R}$, define $(\mathrm{phaseRotate}\,\psi\,\theta)(k)=\psi(k)\,e^{i\theta_k}$.
background
The module forces the Born rule on 8-mode 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$. By Parseval the same holds in the DFT-8 frequency basis.
Signal8 is the 8-tick complex mode space coming from ComplexStructureForcing (tied to the T7 eight-tick octave). A state is normalised when $\sum_k|\psi_k|^2=1$. The sector measure sums squared moduli over a Finset of modes. Phase invariance means the measure depends only on moduli, not arguments; that property is stated by applying this rotation and showing the measure is unchanged.
Downstream lemmas immediately record that rotation preserves Euclidean norm modewise and therefore preserves normalisation and sector measures.
proof idea
Pure definition: the rotated signal is the pointwise product of $\psi(k)$ with $\mathrm{Complex.exp}(i,\theta(k))$. No proof obligations. Downstream norm_phaseRotate discharges the key identity $|e^{i\theta_k}|=1$ via Complex.norm_exp_ofReal_mul_I, which then feeds phase-invariance and normalisation preservation by simp.
why it matters
Phase invariance is axiom (2) in the module's uniqueness theorem for the sector measure. This map is the concrete group action used to state that axiom: every theorem that says $\mu$ is phase-invariant quantifies over $\theta$ and applies phaseRotate.
It is used by norm_phaseRotate, sectorMeasure_phase_invariant, isNormalized_phaseRotate, and both dft8_sector_forcing and dft8_sector_forcing_freq. The quantum-side wrapper born_rule_from_jcost reuses the same pattern. Together those results close the Born-rule gap in the registry (replacing trivial placeholders) under T5/T7/T8 and the two-outcome calibration from TwoOutcomeBornCert.
Without an explicit rotation operator, phase invariance would be an informal slogan rather than a Lean-checkable equality of sector measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.