jcost_phase_invariant
plain-language theorem explainer
Phase multiplication leaves the complex J-cost unchanged: the cost of a complex amplitude equals the cost after any pure phase factor. Anyone deriving Born-rule uniqueness or admissible unitary evolution from recognition cost cites this. The OperatorCore entry is a re-export abbrev of the Foundation theorem, which reduces to the unit-modulus identity for complex exponentials.
Claim. For every $z \in \mathbb{C}$ and every real phase $\theta$, the complex J-cost satisfies $J_{\mathbb{C}}(z) = J_{\mathbb{C}}(z \, e^{i\theta})$. Equivalently, $J$ depends only on the modulus $\|z\|$, not on $\arg(z)$.
background
In the complex-structure forcing module, the recognition cost is lifted from positive reals to complex amplitudes by evaluating the real J-cost on the modulus: $J_{\mathbb{C}}(z) := J(|z|)$. The real cost $J$ is the unique continuous solution forced at T5, $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), subject to the Recognition Composition Law.
The local setting is the passage from that real cost to operators on eight-tick mode data (DFT-8, cyclic shift, total mode cost). Phase invariance is the statement that multiplying an amplitude by a pure phase $e^{i\theta}$ does not change recognition cost. Upstream, the theorem is proved by reducing to $|e^{i\theta}| = 1$ under the complex norm, so the modulus is unchanged.
This is the cost-side dual of ordinary U(1) gauge freedom: only the radial degree of freedom is costly.
proof idea
The OperatorCore declaration is a one-line abbrev re-export; it carries no independent proof. The underlying theorem unfolds $J_{\mathbb{C}}$, applies congruence on the modulus argument, rewrites $|z \cdot e^{i\theta}| = |z| , |e^{i\theta}|$ by multiplicativity of the complex norm, and discharges $|e^{i\theta}| = 1$ by the standard identity for the complex exponential on the imaginary axis. The two sides therefore present the same real argument to $J$.
why it matters
Phase invariance is the stated root cause of the Born rule in this stack: the unique probability weight compatible with cost-phase invariance is $P = |\psi|^2$. Downstream, gleason_from_rs uses that forcing to obtain a Gleason-style uniqueness theorem (weight $r \mapsto r^2$ on the unit interval).
It also feeds admissible evolution: UnitaryEvolution requires inner-product preservation together with non-increase of total mode cost; phase freedom without cost change is what lets unitary (norm-preserving) maps stay cost-admissible. In the unified forcing chain, the T5+T7 canonical-Hamiltonian bridge packages cost-phase duality alongside the small-deviation quadratic $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ that supplies kinetic energy, so this fact sits on the T5 side of the bridge from J-uniqueness and the eight-tick octave to Hamiltonian structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.