jcost_phase_invariant
plain-language theorem explainer
The complex J-cost of an amplitude is unchanged under multiplication by any unit-modulus phase e^{iθ}. Anyone deriving Born-rule uniqueness or unitary mode evolution from Recognition cost axioms cites this. The proof reduces to ‖e^{iθ}‖ = 1 and multiplicativity of the complex norm, so only the modulus enters J.
Claim. For every complex amplitude $z \in \mathbb{C}$ and every real phase $\theta \in \mathbb{R}$, $$J_{\mathbb{C}}(z) = J_{\mathbb{C}}\bigl(z \, e^{i\theta}\bigr),$$ where $J_{\mathbb{C}}(z) := J(\lVert z\rVert)$ is the Recognition J-cost evaluated on the modulus.
background
The module Complex Structure Forcing closes the gap from the eight-tick ledger shift to complex Hilbert structure. T7 forces a cyclic operator $T$ with $T^8 = I$; its eigenvalues are eighth roots of unity, and $\omega^2 = i$ has no real square root, so diagonalization over $\mathbb{R}$ is impossible and complexification is forced. The DFT-8 is the canonical unitary diagonalization.
The real cost $J$ (unique by T5, $J(x) = (x+x^{-1})/2 - 1$) extends to complex amplitudes by $J_{\mathbb{C}}(z) := J(\lVert z\rVert)$. Phase factors $e^{i\theta}$ arise as eigenvalues of the eight-tick shift and as free arguments of mode coefficients. The claim is that cost sees only modulus, never argument.
Upstream, the complex norm is multiplicative and $\lVert e^{i\theta}\rVert = 1$ for real $\theta$. That is all the analytic input needed.
proof idea
Unfold $J_{\mathbb{C}}$ to $J(\lVert\cdot\rVert)$. Congruence reduces the goal to equality of norms. Multiplicativity gives $\lVert z, e^{i\theta}\rVert = \lVert z\rVert , \lVert e^{i\theta}\rVert$. The standard identity $\lVert\exp(i\theta)\rVert = 1$ (Mathlib Complex.norm_exp_ofReal_mul_I) and right-multiplication by one finish the proof. Purely algebraic; no cost-functional properties beyond evaluation on the modulus are used.
why it matters
Phase invariance is the structural reason probability can depend only on $|\psi|^2$, not $\arg(\psi)$. Downstream, gleason_from_rs in the Born-rule module uses it (with additivity and two-branch Gibbs calibration) to force the weight $r \mapsto r^2$. The same fact feeds UnitaryEvolution: admissible evolutions preserve inner products and are J-cost non-increasing, hence unitary on the DFT-8 modes.
In the unified forcing chain it appears inside the T5+T7 → canonical Hamiltonian bridge certificate (cost-phase duality and quadratic emergence $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$). Together with T5 (J-uniqueness) and T7 (eight-tick octave) it closes the registry gap "complex Hilbert space from cost": complex structure is forced, and cost is blind to global phase, so the Born measure is the unique cost-respecting probability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.