JcostC
plain-language theorem explainer
Extends the real recognition cost J to complex amplitudes by evaluating J on the complex modulus. Anyone proving cost-phase invariance, Born-rule uniqueness from phase blindness, or the T5–T7 canonical Hamiltonian bridge cites this. The body is a one-line composition of the real J-cost with the complex norm.
Claim. For $z \in \mathbb{C}$, define $J_{\mathbb{C}}(z) := J(\|z\|)$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost on positive reals (extended by the usual norm convention at $0$).
background
The module Complex Structure Forcing shows that the 8-tick cyclic shift (T7) cannot be diagonalized over the reals: its spectrum includes the 8th roots of unity, and $\omega^2 = i$ has no real representative because $x^2 + 1 > 0$ for all real $x$. Complexification is therefore algebraically forced, and the DFT-8 supplies the canonical unitary diagonalization.
The real recognition cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by T5. It measures the cost of a positive ratio away from $1$. Once amplitudes live in $\mathbb{C}$, the natural lift is to feed the modulus into that same $J$.
Phase factors $e^{i\theta}$ have unit modulus, so any functional built only from $|z|$ is automatically phase-blind. That is the local setting this definition occupies: the cost side of the bridge from T5+T7 to a complex Hilbert structure with genuine unitarity.
proof idea
Definition, not a proof. The body is the one-line composition Cost.Jcost ‖z‖: apply the real J-cost to the complex absolute value. No lemmas are invoked at the definition site; downstream theorems (phase invariance) unfold this and use norm_mul together with ‖exp(iθ)‖ = 1.
why it matters
This is the cost-side hinge of the module's registry claim: close the gap from cost axioms to complex Hilbert structure. Downstream, jcost_phase_invariant proves $J_{\mathbb{C}}(z) = J_{\mathbb{C}}(z e^{i\theta})$ for every real phase, and the doc-comment there names the physical payoff: phase blindness of cost is the root cause of the Born rule, with $P = |\psi|^2$ the unique probability compatible with cost-phase invariance.
The same definition is re-exported in OperatorCore and is named inside the UnifiedForcingChain bridge certificate T5_T7_To_CanonicalHamiltonian_Bridge, which packages cost-phase duality, the small-deviation quadratic (Hamiltonian) limit of $J$, and the DFT-8 eigenvalue structure forced by the cyclic shift. Framework landmarks in play: T5 (J-uniqueness), T7 (eight-tick octave), and the forced complex structure that makes unitarity available on the 8-tick register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.