sectorMeasure_phase_invariant
plain-language theorem explainer
Phase rotation of an 8-mode signal leaves every sector measure unchanged: the Born weight of a mode set depends only on moduli, not arguments. Anyone proving uniqueness of the DFT-8 sector probability cites this invariance axiom. The proof reduces the sum to pointwise equality of complex norms under multiplication by unit-modulus phases.
Claim. For any 8-mode complex signal $\psi$, any real phase assignment $\theta$ on the eight modes, and any finite mode set $S\subseteq\{0,\ldots,7\}$, the sector measure is unchanged by pointwise phase rotation: $\sum_{k\in S}\|e^{i\theta_k}\psi_k\|^2 = \sum_{k\in S}\|\psi_k\|^2$.
background
The module forces the Born rule on the eight-tick (DFT-8) mode space: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and calibrated to the two-branch exp(−C) rule is $\mu(S)=\sum_{k\in S}|\psi_k|^2$ (and the same in the frequency basis by Parseval).
A Signal8 is an 8-component complex amplitude. The sector measure of a mode set $S$ is the sum of squared moduli over $S$. Pointwise phase rotation multiplies mode $k$ by $e^{i\theta_k}$. The supporting lemma states that this rotation preserves each mode norm: $|e^{i\theta_k}\psi_k|=|\psi_k|$, via the standard identity $|e^{i\alpha}|=1$.
Phase invariance is one of the four axioms in the module theorem statement; without it the measure could depend on absolute phases and would not match Born probabilities.
proof idea
Term-mode, three steps. Unfold the sector-measure definition on both sides (sum of squared norms). Congruence reduces equality of sums to equality of summands. Pointwise, rewrite each summand by the lemma that phase rotation preserves the complex norm of mode $k$. No induction or measure theory is required: the claim is pure pointwise algebra on $\mathbb{C}$.
why it matters
This lemma discharges the phase-invariance conjunct inside dft8_sector_forcing and its frequency-domain twin dft8_sector_forcing_freq. Those parent theorems are the module's main result: the unique sector probability meeting normalisation, phase invariance, disjoint additivity, and two-branch calibration is the Born sum of squared moduli (and the same after DFT-8).
In the Recognition chain this sits on T7 (eight-tick octave, period $2^3$) and the complex-structure forcing that supplies Signal8, inner products, and Parseval. It helps close the Born-rule registry gap that previously held trivial placeholders, tying measurement weights to the eight-mode ledger rather than an external postulate.
Downstream uniqueness arguments quote the $\forall\theta$ form of this equality directly; without it the forcing package would not pin $\mu$ to moduli alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.