jcost_modulus_only
plain-language theorem explainer
J-cost is invariant under multiplying a positive real amplitude by a unit-modulus complex phase e^{iθ}. Anyone deriving Born-rule phase independence or unitarity from cost axioms in the complex-structure forcing chain would cite this. The proof is a short algebraic reduction: the complex modulus factors, |e^{iθ}|=1, and the positive real is recovered.
Claim. For every real $r>0$ and every real angle $\theta$, the recognition cost satisfies $J(r)=J\bigl(\lVert r\,e^{i\theta}\rVert\bigr)$, where $J(x)=(x+x^{-1})/2-1$ on positive reals.
background
The module Complex Structure Forcing argues that the eight-tick cyclic shift (T7) cannot be diagonalized over the reals: its spectrum includes the eighth roots of unity, and $\omega^2=i$ has no real representative because $x^2+1>0$ for all real $x$. Complexification is therefore forced, and the DFT-8 supplies the canonical unitary diagonalization.
The recognition cost on positive ratios is $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness). In the complex setting one evaluates cost on moduli of mode amplitudes. The module's step 7 records that $J$ depends only on $|c_k|$, not on $\arg(c_k)$; that phase invariance is the content of the present theorem.
Upstream, Jcost is the same closed form used throughout the cost layer. The complex-norm identities applied here are standard Mathlib facts: multiplicativity of $\lVert\cdot\rVert$ and $\lVert e^{i\theta}\rVert=1$.
proof idea
Term/tactic hybrid, three steps. First rewrite the right-hand modulus by multiplicativity (norm_mul), cancel the phase via Complex.norm_exp_ofReal_mul_I (which yields $1$), and simplify by mul_one, leaving $J(r)=J(\lVert(r:\mathbb{C})\rVert)$. Then congr 1 reduces the claim to equality of the two positive real arguments. Finally simp with Complex.norm_real and abs_of_pos hr recovers $r$ from the real embedding, using positivity of $r$.
why it matters
This is the explicit phase-invariance lemma in the module's forcing chain from cost axioms to complex Hilbert structure. The module doc lists it as step 7: after forcing $\mathbb{C}$ via the non-real eigenvalue $i$ of the eight-tick shift, and after Parseval for DFT-8, one still needs that $J$ sees only moduli. That fact is why probability can depend on $|\psi|^2$ rather than $\arg(\psi)$, and it feeds the next block (Part 6): cost conservation plus balanced ledger ($\sigma=0$) implies the evolution operator preserves norm and is therefore unitary.
Framework landmarks: T5 (J uniqueness), T7 (eight-tick octave), and the registry item "Complex Hilbert space from cost". No downstream uses are recorded yet in the graph; the immediate consumer is the unitarity-from-cost-conservation development in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.