mode_cost_phase_invariant
plain-language theorem explainer
Independent phase rotations of the eight DFT modes leave the total J-cost unchanged, so the cost landscape carries a U(1)^8 gauge symmetry in the mode basis. Anyone deriving unitarity of cost- and norm-preserving linear maps on ℂ^8 cites this fact. The argument is a short algebraic reduction: modulus is multiplicative and pure phases have unit modulus, so each summand J(‖c_k‖) is fixed.
Claim. For every signal $f:\{0,\ldots,7\}\to\mathbb{C}$ and every real phase assignment $\theta:\{0,\ldots,7\}\to\mathbb{R}$, the total mode cost is unchanged under modewise phase rotation: $\sum_{k=0}^{7} J(\|f(k)\|)=\sum_{k=0}^{7} J(\|f(k)\,e^{i\theta_k}\|)$, where $J$ is the Recognition cost on moduli.
background
The module Complex Structure Forcing shows that the eight-tick cyclic shift on the ledger cannot be diagonalized over the reals, so complexification is algebraically forced rather than optional. A signal on the eight-tick cycle is a map $f:\mathrm{Fin},8\to\mathbb{C}$. Its total mode cost is the sum $\sum_k J(|f(k)|)$ of the unique J-cost (T5) evaluated on each mode modulus.
The module argument runs: T7 forces a shift $T$ with $T^8=I$; eigenvalues are eighth roots of unity; $\omega^2=i$ has no real representative; the DFT-8 is the canonical unitary diagonalization; Parseval preserves the inner product. The present claim is step 7 of that chain: J depends only on modulus, not argument, so the cost landscape is phase-blind in the mode basis.
Upstream, totalModeCost is exactly that sum of $J(|c_k|)$. The proof also uses multiplicativity of the complex modulus and the elementary identity $|e^{i\theta}|=1$.
proof idea
Term-mode proof by unfolding and congruence. Unfold the total mode cost to an eight-term sum of $J(|\cdot|)$. Congruence on the sum, then pointwise on each index $k$, reduces the claim to equality of the two moduli. Rewrite $|f(k)\cdot e^{i\theta_k}|$ via multiplicativity of the complex norm, apply $|\exp(i\theta)|=1$ for real $\theta$, and cancel the unit factor with mul_one. No induction and no analysis beyond the norm identities.
why it matters
This is the phase-invariance half of the bridge from cost axioms to genuine unitarity on ℂ^8. Combined with the norm constraint, any cost-preserving, norm-preserving linear map must be unitary (module claim 8). It is packaged directly into complex_structure_certificate as the cost_phase_invariant field, alongside shift periodicity, the imaginary eigenvalue $i$, the absence of a real root of $x^2+1$, and DFT-8 unitarity.
Downstream it feeds the Unified Forcing Chain bridges from T5+T7 to the canonical Hamiltonian and from T7 to the canonical carrier: cost-phase duality and the DFT-8 eigenvalue structure sit next to the small-deviation expansion $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$. Framework landmarks: T5 (J-uniqueness), T7 (eight-tick octave), and the registry gap "Complex Hilbert space from cost". Closes that gap rather than leaving it as scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.